stringtranslate.com

Realizabilidad

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]

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]

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

  1. ^ de Oosten 2000
  2. ^ 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.
  3. ^ van Oosten 2000, pág. 7
  4. ^ Rosa 1953
  5. ^ van Oosten 2000, pág. 6
  6. ^ Birkedal 2000
  7. ^ 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.
  8. ^ Krivine, Jean-Louis (2011). "Álgebras de realizabilidad: un programa para ordenar bien R". Métodos lógicos en informática . 7 .
  9. ^ Seiller, Thomas (2024). Informática Matemática (Tesis de Habilitación). Universidad Sorbona París Norte.
  10. ^ 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.
  11. ^ 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.
  12. ^ 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

Enlaces externos