En lógica matemática , la interpretación 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 . A veces también se le llama 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 pretende ser una prueba de una fórmula determinada . 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 prueba 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 pretender conocer una solución al problema representado por esa fórmula. Por ejemplo , está el problema de reducir a ; resolverlo 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 :
En conjunto, una prueba de es una función que convierte un par < a , b > – donde es una prueba de P , y es una función que convierte una prueba de P en una prueba de – en una prueba de . Hay una función que hace esto, donde , demostrando la ley de no contradicción, sin importar cuál sea P.
De hecho, la misma línea de pensamiento también proporciona una prueba de la regla del modus ponens , donde hay cualquier proposición.
Por otro lado, la ley del tercero excluido se expande hasta , 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 es demostrable, entonces tampoco lo es .
En general, no es posible que un sistema lógico tenga un operador de negación formal tal que haya una prueba de "no" exactamente cuando no hay una prueba de ; véase los teoremas de incompletitud de Gödel . En cambio, la interpretación de BHK 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 al abordar la aritmética. Supongamos que 0 = 1 y procedamos por inducción matemática : 0 = 0 por el axioma de igualdad. Ahora (hipótesis de inducción), si 0 fuera igual a 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 , por lo tanto 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 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 el 0 "no" es el sucesor de ningún 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 visió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. Las diferentes versiones del constructivismo divergirán en este punto.
La teoría de la realizabilidad de Kleene identifica las funciones con las funciones computables . Se trata 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 se evalúa como el mismo número que y (que siempre es decidible para números naturales); de lo contrario, no hay prueba. Luego, estos se construyen por inducción en algoritmos más complejos.
Si se toma el cálculo lambda como 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.
