Realizabilidad

En lógica matemática , la realizabilidad es un conjunto de métodos de la teoría de la demostración que se utilizan para estudiar demostraciones constructivas y extraer información adicional de ellas. ^{[ 1 ]} Las fórmulas de una teoría formal se "realizan" mediante objetos, conocidos como "realizadores", de manera que el conocimiento del realizador proporciona conocimiento sobre la verdad de la fórmula. Existen muchas variantes de la realizabilidad; la clase exacta de fórmulas que se estudia y los objetos que actúan como realizadores difieren de una variante a otra.

La realizabilidad puede considerarse una formalización de la interpretación de Brouwer-Heyting-Kolmogorov (BHK) de la lógica intuicionista . En la realizabilidad, la noción de "prueba" (que queda sin definir en la interpretación BHK) se reemplaza por una noción formal de "realizador". La mayoría de las variantes de la realizabilidad parten de un teorema que establece que cualquier enunciado demostrable en el sistema formal estudiado es realizable. Sin embargo, el realizador suele proporcionar más información sobre la fórmula que la que ofrecería directamente una prueba formal.

Además de brindar información sobre la demostrabilidad intuicionista, la realizabilidad puede aplicarse para probar las propiedades de disyunción y existencia de las teorías intuicionistas y para extraer programas de las demostraciones, como en la minería de pruebas . También está relacionada con la teoría de topos a través de la realizabilidad de topoi .

La versión original de realizabilidad de Kleene utiliza números naturales como realizadores para fórmulas en la aritmética de Heyting . Se requieren algunas notaciones: primero, un par ordenado ( n , m ) se trata como un solo número utilizando una función de emparejamiento recursiva primitiva fija ; segundo, para cada número natural n , φn es la función computable con índice n . Las siguientes cláusulas se utilizan para definir una relación " n realiza A " entre los números naturales n y las fórmulas _A en el lenguaje de la aritmética de Heyting, conocida como la relación de realizabilidad de Kleene de 1945: ^{[ 2 ]}

• Cualquier número n realiza una fórmula atómica s = t si y solo si s = t es verdadera. Por lo tanto, todo número realiza una ecuación verdadera, y ningún número realiza una ecuación falsa.
• Un par ( n , m ) realiza una fórmula A ∧ B si y solo si n realiza A y m realiza B. Por lo tanto, un realizador para una conjunción es un par de realizadores para los conjuntivos.
• Un par ( n , m ) realiza una fórmula A ∨ B si y solo si se cumplen las siguientes condiciones: n es 0 o 1; y si n es 0, entonces m realiza A ; y si n es 1, entonces m realiza B. Por lo tanto, un realizador para una disyunción elige explícitamente uno de los disyuntos (con n ) y proporciona un realizador para él (con m ).
• Un número n realiza una fórmula A → B si y solo si, para cada m que realiza A , φ _n ( m ) realiza B. Por lo tanto, un realizador para una implicación corresponde a una función computable que toma cualquier realizador para la hipótesis y produce un realizador para la conclusión.
• Un par ( n , m ) realiza una fórmula ( ∃ x ) A ( x ) si y solo si m es un realizador para A ( n ). Por lo tanto, un realizador para una fórmula existencial produce un testigo explícito para el cuantificador junto con un realizador para la fórmula instanciada con ese testigo.
• Un número n realiza una fórmula ( ∀ x ) A ( x ) si y solo si, para todo m , φ _n ( m ) está definida y realiza A ( m ). Por lo tanto, un realizador para una proposición universal es una función computable que produce, para cada m , un realizador para la fórmula instanciada con m .

Con esta definición, se obtiene el siguiente teorema: ^{[ 3 ]}

Sea A una sentencia de aritmética de Heyting (HA). Si HA prueba A, entonces existe un n tal que n realiza A.

Por otro lado, existen teoremas clásicos (incluso esquemas de fórmulas proposicionales) que se realizan pero que no son demostrables en HA, un hecho establecido por primera vez por Rose. ^{[ 4 ]} Por lo tanto, la realizabilidad no refleja exactamente el razonamiento intuicionista.

Se puede utilizar un análisis más profundo del método para demostrar que HA tiene las " propiedades de disyunción y existencia ": ^{[ 5 ]}

• Si HA prueba una sentencia ( ∃ x ) A ( x ), entonces existe un n tal que HA prueba A ( n ).
• Si HA prueba una oración A ∨ B , entonces HA prueba A o HA prueba B.

Se obtienen más propiedades de este tipo mediante fórmulas de Harrop .

Kreisel introdujo la realizabilidad modificada , que utiliza el cálculo lambda tipado como lenguaje de los realizadores. La realizabilidad modificada es una forma de demostrar que el principio de Markov no es derivable en la lógica intuicionista. Por el contrario, permite justificar constructivamente el principio de independencia de premisas .

${\displaystyle (A\rightarrow \exists x\;P(x))\rightarrow \exists x\;(A\rightarrow P(x))}$.

La realizabilidad relativa ^{[ 6 ]} es un análisis intuicionista de elementos computables o enumerables computacionalmente de estructuras de datos que no son necesariamente computables, como operaciones computables en todos los números reales cuando los reales solo pueden aproximarse en sistemas informáticos digitales.

La realizabilidad clásica fue introducida por Krivine ^{[ 7 ]} y extiende la realizabilidad a la lógica clásica. Además, realiza axiomas de la teoría de conjuntos de Zermelo-Fraenkel . Entendida como una generalización del forzamiento de Cohen , se utilizó para proporcionar nuevos modelos de teoría de conjuntos. ^{[ 8 ]}

La realizabilidad lineal extiende las técnicas de realizabilidad a la lógica lineal . El término fue acuñado por Seiller ^{[ 9 ]} para abarcar varias construcciones, como la geometría de los modelos de interacción, ^{[ 10 ]} la ludica ^{[ 11 ]} y los modelos de grafos de interacción. ^{[ 12 ]}

La realizabilidad es uno de los métodos utilizados en la minería de pruebas para extraer "programas" concretos de pruebas matemáticas aparentemente no constructivas. La extracción de programas mediante la realizabilidad está implementada en algunos asistentes de pruebas como Rocq .

• Correspondencia entre Curry y Howard
• interpretación de la dialéctica
• Fórmula de Harrop

• Birkedal, Lars; Jaap van Oosten (2000). Realizabilidad relativa y relativa modificada .
• Kreisel G. (1959). "Interpretación del análisis mediante funcionales constructivos de tipos finitos", en: Constructividad en matemáticas, editado por A. Heyting, North-Holland, pp.  101–128.
• Kleene, SC (1945). "Sobre la interpretación de la teoría de números intuicionista". Journal of Symbolic Logic . 10 (4): 109– 124. doi : 10.2307/2269016 . JSTOR 2269016 . 
• Kleene, SC (1973). «Realizabilidad: una revisión retrospectiva» de Mathias, ARD; Hartley Rogers (1973). Cambridge Summer School in Mathematical Logic : celebrada en Cambridge/Inglaterra, del 1 al 21 de agosto de 1971. Berlín: Springer. ISBN  3-540-05569-X., págs.  95–112.
• van Oosten, Jaap (2000). Realizabilidad: un ensayo histórico .
• Rose, GF (1953). "Cálculo proposicional y realizabilidad" . Transactions of the American Mathematical Society . 75 (1): 1– 19. doi : 10.2307/1990776 . JSTOR 1990776 .