En lógica matemática , la realizabilidad es una colección de métodos en la teoría de pruebas que se utilizan para estudiar pruebas constructivas y extraer información adicional de ellas. [1] Las fórmulas de una teoría formal son "realizadas" por objetos, conocidos como "realizadores", de manera que el conocimiento del realizador proporciona conocimiento sobre la verdad de la fórmula. Hay muchas variaciones de realizabilidad; exactamente qué clase de fórmulas se estudia y qué objetos son realizadores difieren de una variación a otra.
La realizabilidad puede verse como 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 no se define en la interpretación de BHK) se reemplaza por una noción formal de "realizador". La mayoría de las variantes de realizabilidad comienzan con un teorema que establece que cualquier enunciado que sea demostrable en el sistema formal que se está estudiando es realizable. Sin embargo, el realizador generalmente brinda más información sobre la fórmula que la que proporcionaría directamente una prueba formal.
Además de brindar información sobre la demostrabilidad intuicionista, la realizabilidad se puede aplicar para demostrar las propiedades de disyunción y existencia de las teorías intuicionistas y para extraer programas de las pruebas, como en la minería de pruebas . También está relacionada con la teoría de topos a través de la realizabilidad topoi .
Ejemplo: la realizabilidad de Kleene en 1945
La versión original de Kleene de la realizabilidad utiliza números naturales como realizadores de fórmulas en la aritmética de Heyting . Se requieren algunas piezas de notación: 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 números naturales n y 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 verdadero. 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 sólo si n realiza A y m realiza B . Por lo tanto, un realizador de una conjunción es un par de realizadores de los conjuntos.
- Un par ( n , m ) realiza una fórmula A ∨ B si y solo si se cumple lo siguiente: 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 sólo 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á definido y realiza A ( m ). Por lo tanto, un realizador para un enunciado 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 oración de la aritmética de Heyting (HA). Si HA prueba A, entonces existe un n tal que n realiza A.
Por otra parte, hay 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 oración (∃ x ) A ( x ), entonces hay una 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 utilizando las fórmulas de Harrop .
Desarrollos posteriores
Kreisel introdujo la realizabilidad modificada , que utiliza el cálculo lambda tipificado 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 de manera constructiva el principio de independencia de premisas :
.
La realizabilidad relativa [6] es un análisis intuicionista de elementos computables o computablemente enumerables 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 lúdica , [11] los modelos de gráficos de interacción. [12]
Aplicaciones
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 realizabilidad se implementa en algunos asistentes de pruebas como Coq .
Véase también
Notas
- ^ de Oosten 2000
- ^ A. Ščedrov, "Teoría de conjuntos intuicionista" (pp. 263--264). De la obra de Harvey Friedman, Research on the Foundations of Mathematics (1985), Studies in Logic and the Foundations of Mathematics, vol. 117.
- ^ van Oosten 2000, pág. 7
- ^ Rosa 1953
- ^ van Oosten 2000, pág. 6
- ^ Birkedal 2000
- ^ Krivine, Jean-Louis (2001). "Cálculo lambda tipado en la teoría clásica de conjuntos de Zermelo-Fraenkel". Archivo de Lógica Matemática . 40 (2): 189–205.
- ^ Krivine, Jean-Louis (2011). "Álgebras de realizabilidad: un programa para ordenar bien R". Métodos lógicos en informática . 7 .
- ^ Seiller, Thomas (2024). Informática Matemática (Tesis de Habilitación). Universidad Sorbona París Norte.
- ^ Girard, Jean-Yves (1989). "Geometría de la interacción 1: interpretación del sistema F". Estudios de lógica y fundamentos de las matemáticas . 127 : 221–260.
- ^ Girard, Jean-Yves (2001). "Locus Solum: de las reglas de la lógica a la lógica de las reglas". Estructuras matemáticas en informática . 11 : 301–506.
- ^ Seiller, Thomas (2016). "Gráficos de interacción: lógica lineal completa". Actas del 31.º Simposio anual ACM/IEEE sobre lógica en informática .
Referencias
- Birkedal, Lars; Jaap van Oosten (2000). Realizabilidad relativa y relativa modificada.
- Kreisel G. (1959). "Interpretación del análisis por medio de funcionales constructivos de tipos finitos", en: Constructivity in Mathematics, 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). "Realizability: a retrospective survey" 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.
Enlaces externos
- Realizabilidad Colección de enlaces a artículos recientes sobre realizabilidad y temas relacionados.
