El principio de Markov (también conocido como principio de Leningrado [1] ), llamado así en honor a Andrey Markov Jr , es un enunciado de existencia condicional para el cual existen muchas formulaciones equivalentes, como se analiza a continuación. El principio es lógicamente válido en la forma clásica , pero no en la matemática constructiva intuicionista . Sin embargo, muchos casos concretos también se pueden demostrar en un contexto constructivo.
El principio fue estudiado y adoptado por primera vez por la escuela rusa de constructivismo, junto con principios de elección y, a menudo, con una perspectiva de realizabilidad de la noción de función matemática.
En el lenguaje de la teoría de la computabilidad , el principio de Markov es una expresión formal de la afirmación de que si es imposible que un algoritmo no termine, entonces para alguna entrada sí termina. Esto equivale a la afirmación de que si un conjunto y su complemento son ambos computablemente enumerables , entonces el conjunto es decidible . Estas afirmaciones son demostrables en la lógica clásica.
En lógica de predicados , un predicado P sobre algún dominio se llama decidible si para cada x en el dominio, se cumple P ( x ) o se cumple la negación de P ( x ). Esto no es trivialmente cierto desde el punto de vista constructivo.
El principio de Markov establece entonces: Para un predicado decidible P sobre los números naturales , si P no puede ser falso para todos los números naturales n , entonces es verdadero para algún n . Escrito usando cuantificadores :
La regla de Markov es la formulación del principio de Markov como regla. Afirma que es derivable en cuanto lo es, por decidible. Formalmente,
Anne Troelstra [2] demostró que es una regla admisible en la aritmética de Heyting . Posteriormente, el lógico Harvey Friedman demostró que la regla de Markov es una regla admisible en la lógica intuicionista de primer orden , la aritmética de Heyting y varias otras teorías intuicionistas, [3] utilizando la traducción de Friedman .
El principio de Markov es equivalente en el lenguaje de la aritmética a:
para una función recursiva total sobre los números naturales.
En presencia del principio de tesis de Church , el principio es equivalente a su forma para funciones recursivas primitivas . Usando el predicado T de Kleene , este último puede expresarse como
Si la aritmética constructiva se traduce utilizando la realizabilidad en una metateoría clásica que prueba la consistencia de la teoría clásica relevante (por ejemplo, la aritmética de Peano si estamos estudiando la aritmética de Heyting ), entonces el principio de Markov está justificado: un realizador es la función constante que lleva una comprensión que no es falsa en todas partes a la búsqueda ilimitada que comprueba sucesivamente si es verdadera. Si no es falso en todas partes, entonces, por coherencia, debe haber un término que sea válido y, eventualmente, la búsqueda comprobará cada término. Sin embargo, si no se cumple en ninguna parte, entonces el dominio de la función constante debe estar vacío, por lo que aunque la búsqueda no se detiene, todavía se mantiene vagamente que la función es una realizadora. Por la Ley del Medio Excluido (en nuestra metateoría clásica), no debe cumplirse en ninguna parte o no debe cumplirse en ninguna parte, por lo tanto, esta función constante es un realizador.
Si, en cambio, la interpretación de la realizabilidad se utiliza en una metateoría constructiva, entonces no está justificada. De hecho, para la aritmética de primer orden , el principio de Markov captura exactamente la diferencia entre una metateoría constructiva y una clásica. Específicamente, un enunciado es demostrable en la aritmética de Heyting con la tesis extendida de Church si y sólo si hay un número que de manera demostrable lo realiza en la aritmética de Heyting ; y es demostrable en aritmética de Heyting con la tesis de Church extendida y el principio de Markov si y sólo si hay un número que demostrablemente lo realiza en la aritmética de Peano .
El principio de Markov equivale, en el lenguaje del análisis real , a los siguientes principios:
La realizabilidad modificada no justifica el principio de Markov, incluso si se utiliza la lógica clásica en la metateoría: no hay ningún realizador en el lenguaje del cálculo lambda simplemente tipado, ya que este lenguaje no es completo de Turing y no se pueden definir bucles arbitrarios en él.
El principio de Markov débil es una forma más débil del principio. Puede expresarse en el lenguaje del análisis, como un enunciado condicional para la positividad de un número real:
Esta forma puede justificarse por los principios de continuidad de Brouwer , mientras que la forma más fuerte los contradice. Así, el principio débil de Markov puede derivarse del razonamiento intuicionista, de realizabilidad y clásico, en cada caso por diferentes razones, pero no es válido en el sentido constructivo general de Bishop , [4] ni demostrable en la teoría de conjuntos .
Para comprender de qué se trata el principio, es útil inspeccionar una declaración más contundente. Lo siguiente expresa que cualquier número real , tal que ningún no positivo no esté debajo de él, es positivo:
donde denota la negación de . Ésta es una implicación más fuerte porque el antecedente es más flexible. Tenga en cuenta que aquí se concluye una afirmación lógicamente positiva a partir de una afirmación lógicamente negativa. Está implícito en el principio débil de Markov al elevar la ley de De Morgan a una equivalencia.
Suponiendo la eliminación clásica de la doble negación, el principio débil de Markov se vuelve trivial y expresa que un número mayor que todos los números no positivos es positivo.
Una función entre espacios métricos se llama fuertemente extensional si implica , que clásicamente es simplemente la contraposición de la función que preserva la igualdad. Se puede demostrar que el principio de Markov es equivalente a la proposición de que todas las funciones entre espacios métricos arbitrarios son fuertemente extensionales, mientras que el principio de Markov débil es equivalente a la proposición de que todas las funciones desde espacios métricos completos hasta espacios métricos son fuertemente extensionales.
