En lógica matemática , la interpretación de Brouwer-Heyting-Kolmogorov , o interpretación BHK , de la lógica intuicionista fue propuesta por LEJ Brouwer y Arend Heyting , e independientemente por Andrey Kolmogorov . También se la denomina a veces interpretación de la realizabilidad , debido a la conexión con la teoría de la realizabilidad de Stephen Kleene . Es la explicación estándar de la lógica intuicionista. [1]
La interpretación establece lo que se pretende que sea una prueba de una fórmula dada . Esto se especifica por inducción sobre la estructura de esa fórmula:
Se supone que la interpretación de una proposición primitiva se conoce a partir del contexto. En el contexto de la aritmética, una demostración de la fórmula es un cálculo que reduce los dos términos al mismo número.
Kolmogorov siguió la misma línea, pero formuló su interpretación en términos de problemas y soluciones. Afirmar una fórmula es afirmar que se conoce una solución al problema representado por esa fórmula. Por ejemplo , el problema de reducir a ; para resolverlo se requiere un método para resolver el problema dada una solución al problema .
La función identidad es una prueba de la fórmula , sin importar cuál sea P.
La ley de no contradicción se expande a :
Poniéndolo todo junto, una prueba de es una función que convierte un par < a , b > – donde es una prueba de , y es una función que convierte una prueba de en una prueba de – en una prueba de . Hay una función que hace esto, donde , lo que demuestra la ley de no contradicción, sin importar cuál sea P.
De hecho, la misma línea de pensamiento proporciona también una prueba de la regla del modus ponens , donde hay cualquier proposición.
Por otra parte, la ley del medio excluido se expande a , y en general no tiene prueba. Según la interpretación, una prueba de es un par < a , b > donde a es 0 y b es una prueba de P , o a es 1 y b es una prueba de . Por lo tanto, si ni P ni son demostrables, entonces tampoco lo son .
En general, no es posible que un sistema lógico tenga un operador de negación formal tal que exista una prueba de "no" exactamente cuando no exista una prueba de ; véanse los teoremas de incompletitud de Gödel . La interpretación de BHK, en cambio, considera que "no" significa que conduce al absurdo, designado , de modo que una prueba de es una función que convierte una prueba de en una prueba de absurdo.
Un ejemplo típico de absurdo se encuentra en el tratamiento de la aritmética. Supongamos que 0 = 1 y procedamos por inducción matemática : 0 = 0 por el axioma de igualdad. Ahora bien (hipótesis de inducción), si 0 fuera igual a un cierto número natural n , entonces 1 sería igual a n + 1 ( axioma de Peano : S m = S n si y sólo si m = n ), pero como 0 = 1, entonces 0 también sería igual a n + 1. Por inducción, 0 es igual a todos los números y, por lo tanto, dos números naturales cualesquiera se vuelven iguales.
Por lo tanto, hay una manera de pasar de una prueba de 0 = 1 a una prueba de cualquier igualdad aritmética básica, y por lo tanto a una prueba de cualquier proposición aritmética compleja. Además, para obtener este resultado no fue necesario invocar el axioma de Peano que establece que 0 "no" es el sucesor de cualquier número natural. Esto hace que 0 = 1 sea adecuado como en la aritmética de Heyting (y el axioma de Peano se reescribe 0 = S n → 0 = S 0). Este uso de 0 = 1 valida el principio de explosión .
La interpretación de BHK dependerá de la opinión que se adopte sobre lo que constituye una función que convierte una prueba en otra, o que convierte un elemento de un dominio en una prueba. Distintas versiones del constructivismo divergen sobre este punto.
La teoría de realizabilidad de Kleene identifica las funciones con las funciones computables . Se ocupa de la aritmética de Heyting, donde el dominio de cuantificación son los números naturales y las proposiciones primitivas son de la forma x = y . Una prueba de x = y es simplemente el algoritmo trivial si x evalúa el mismo número que y (que siempre es decidible para los números naturales), de lo contrario no hay prueba. Estos se construyen luego por inducción en algoritmos más complejos.
Si se toma el cálculo lambda como la definición de la noción de función, entonces la interpretación BHK describe la correspondencia entre la deducción natural y las funciones.
