El principio de Markov (también conocido como principio de Leningrado [1] ), llamado así por 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 de manera clásica , pero no en matemáticas constructivas intuicionistas . Sin embargo, muchos casos particulares de este principio son, no obstante, demostrables también 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, termina. Esto es equivalente 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 en términos constructivos.
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. Establece que es derivable en cuanto es, por tanto, decidible. Formalmente,
Anne Troelstra [2] demostró que es una regla admisible en la aritmética de Heyting . Más tarde, 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 . Utilizando 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 realización que no es falsa en todas partes a la búsqueda ilimitada que verifica sucesivamente si es verdadera. Si no es falsa en todas partes, entonces por -consistencia debe haber un término para el cual se cumple, y cada término será verificado por la búsqueda eventualmente. 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 detenga, todavía se cumple vacuamente que la función es un realizador. Por la Ley del Tercero Excluido (en nuestra metateoría clásica), debe o bien no cumplirse en ninguna parte o no cumplirse en ninguna parte, por lo tanto, esta función constante es un realizador.
Si, en cambio, se utiliza la interpretación de la realizabilidad 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 de Church extendida si y solo si hay un número que lo realiza demostrablemente en la aritmética de Heyting ; y es demostrable en la aritmética de Heyting con la tesis de Church extendida y el principio de Markov si y solo si hay un número que lo realiza demostrablemente en la aritmética de Peano .
El principio de Markov es equivalente, 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 realizador en el lenguaje del cálculo lambda simplemente tipado ya que este lenguaje no es Turing-completo y no se pueden definir bucles arbitrarios en él.
El principio débil de Markov es una forma más débil del principio. Puede enunciarse en el lenguaje del análisis como una afirmación condicional para la positividad de un número real:
Esta forma puede justificarse mediante 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 entender de qué se trata el principio, es útil examinar un enunciado más fuerte. El siguiente expresa que cualquier número real , tal que ningún número no positivo esté por debajo de él, es positivo:
donde denota la negación de . Esta es una implicación más fuerte porque el antecedente es más flexible. Nótese que aquí se concluye una afirmación lógicamente positiva a partir de una afirmación lógicamente negativa. Esto está implícito en el principio débil de Markov al elevar la ley de De Morgan para a una equivalencia.
Suponiendo la eliminación clásica de doble negación, el principio de Markov débil se vuelve trivial, expresando que un número mayor que todos los números no positivos es positivo.
Una función entre espacios métricos se denomina 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.
