El principio de Markov , que lleva el nombre de Andrey Markov Jr , es un enunciado de existencia condicional para el que existen muchas formulaciones equivalentes, como se analiza a continuación.
El principio es la validez lógica clásicamente, pero no en la matemática constructiva intuicionista . Sin embargo, muchos ejemplos particulares de ello también se pueden demostrar en un contexto constructivo.
Historia
El principio fue estudiado y adoptado por primera vez por la escuela rusa de constructivismo, junto con los principios de elección y, a menudo, con una perspectiva de realizabilidad sobre la noción de función matemática.
En teoría de la computabilidad
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 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 .
En lógica intuicionista
En la lógica de predicados , un predicado P sobre algún dominio se llama decidible si para cada x en el dominio, P ( x ) es verdadero o P ( x ) no es verdadero. Esto no es trivialmente cierto de manera constructiva.
Para un predicado decidible P sobre los números naturales , el principio de Markov dice:
Es decir, si P no puede ser falso para todos los números naturales n , entonces es verdadero para algunos n .
La regla de Markov
La regla de Markov es la formulación del principio de Markov como regla. Se afirma que es derivable tan pronto como es para Decidible. Formalmente,
Anne Troelstra [1] 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 toda la lógica intuicionista , la aritmética de Heyting y varias otras teorías intuicionistas, [2] utilizando la traducción de Friedman .
En aritmética de Heyting
Es equivalente en el lenguaje de la aritmética a:
por una función recursiva total sobre los números naturales.
Realizabilidad
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, 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 toma una comprensión de queno es en todas partes falso a la búsqueda ilimitada que comprueba sucesivamente sies verdad. Si no es falso en todas partes, entonces por -consistencia debe haber un término para el cual se mantiene, y cada término será verificado por la búsqueda eventualmente. Si acasono se mantiene 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 sostiene en forma vacía que la función es un realizador. Por la Ley del Medio Excluido (en nuestra metateoría clásica), debe retener en ninguna parte o no retener 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 clásica. Específicamente, un enunciado se puede demostrar en la aritmética de Heyting con la tesis de Extended Church si y solo si hay un número que de manera comprobable lo realiza en la aritmética de Heyting ; y es demostrable en la aritmética de Heyting con la tesis de Extended Church y el principio de Markov si y solo si hay un número que lo haga demostrablemente en la aritmética de Peano .
En análisis constructivo
Es equivalente, en el lenguaje del análisis real , a los siguientes principios:
- Para cada número real x , si es contradictorio que x sea igual a 0, entonces existe y ∈ Q tal que 0 < y <| x |, a menudo se expresa diciendo que x es , aparte de, o constructiva desigual a, 0.
- Para cada número real x , si es contradictorio que x sea igual a 0, entonces existe y ∈ R tal que xy = 1.
La realizabilidad modificada no justifica el principio de Markov, incluso si se usa la lógica clásica en la metateoría: no hay un realizador en el lenguaje del cálculo lambda simplemente tipado, ya que este lenguaje no es Turing completo y los bucles arbitrarios no se pueden definir en él.
Principio débil de Markov
El principio de Markov débil es una forma más débil del principio de Markov que puede enunciarse en el lenguaje del análisis como
Es una declaración condicional sobre la decidibilidad de la positividad de un número real.
Esta forma puede estar justificada por los principios de continuidad de Brouwer , mientras que la forma más fuerte los contradice. Así, puede derivarse del razonamiento intuicionista, de realizabilidad y clásico, en cada caso por diferentes razones, pero este principio no es válido en el sentido constructivo general de Bishop. [3]
Ver también
Referencias
- ^ Anne S. Troelstra. Investigación metamatemática de aritmética y análisis intuicionistas, Springer Verlag (1973), Teorema 4.2.4 de la 2ª edición.
- ^ Harvey Friedman. Funciones clásicas e intuicionistas probables recursivas. En Scott, DS y Muller, GH Editors, Higher Set Theory, Volumen 699 de Lecture Notes in Mathematics, Springer Verlag (1978), págs. 21-28.
- ^ Ulrich Kohlenbach , " Sobre el principio de Markov débil ". Mathematical Logic Quarterly (2002), vol 48, número S1, págs. 59–65.
enlaces externos
- Matemáticas constructivas (Enciclopedia de Filosofía de Stanford)