En lógica matemática , la realizabilidad es una colección de métodos en la teoría de la prueba 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 estudian y qué objetos son realizadores difieren de una variación a otra.
La realizabilidad puede verse como una formalización de la interpretación BHK de la lógica intuicionista ; en realizabilidad, la noción de "prueba" (que no está definida 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 el teorema de que cualquier enunciado que sea demostrable en el sistema formal que se estudia es realizable. Sin embargo, el realizador suele dar más información sobre la fórmula que la que proporcionaría directamente una prueba formal.
Más allá de dar una idea de la demostrabilidad intuicionista, la realizabilidad se puede aplicar para probar 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á relacionado con la teoría del topos a través de los topoi de realizabilidad .
La versión original de realizabilidad de Kleene utiliza números naturales como realizadores de fórmulas en la aritmética de Heyting . Se requieren algunas notaciones: primero, un par ordenado ( n , m ) se trata como un número único usando una función de emparejamiento recursiva primitiva fija ; en segundo lugar, 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 relación de realizabilidad de Kleene de 1945: [2]
Con esta definición se obtiene el siguiente teorema: [3]
Por otro lado, 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] Así que la realizabilidad no refleja exactamente el razonamiento intuicionista.
Se puede utilizar un análisis más detallado 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 fórmulas de Harrop .
Kreisel introdujo la realizabilidad modificada , que utiliza cálculo lambda escrito 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 premisa :
La realizabilidad relativa [6] es un análisis intuicionista de elementos recursivos o recursivamente enumerables de estructuras de datos que no son necesariamente computables, como operaciones computables en todos los números reales cuando los reales sólo pueden aproximarse en sistemas informáticos digitales.
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 se implementa en algunos asistentes de prueba como Coq .
