Interpretación de Brouwer-Heyting-Kolmogorov - Brouwer–Heyting–Kolmogorov interpretation

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 . A veces también se le llama interpretación de realizabilidad , debido a la conexión con la teoría de realizabilidad de Stephen Kleene .

La interpretación

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:

• Una prueba de es un par < un ,  b > donde una es una prueba de y b es una prueba de . ${\ Displaystyle P \ wedge Q}$${\ Displaystyle P}$${\ displaystyle Q}$
• Una prueba de es un par < a ,  b > donde a es 0 y b es una prueba de , o a es 1 y b es una prueba de . ${\ Displaystyle P \ vee Q}$${\ Displaystyle P}$${\ displaystyle Q}$
• Una prueba de es una función que convierte una prueba de en una prueba de . ${\ Displaystyle P \ a Q}$${\ Displaystyle f}$${\ Displaystyle P}$${\ displaystyle Q}$
• Una prueba de es un par < a ,  b > donde a es un elemento de S y b es una prueba de . ${\ Displaystyle \ existe x \ en S: \ varphi (x)}$${\ Displaystyle \ varphi (a)}$
• Una prueba de es una función que convierte un elemento a de S en una prueba de . ${\ Displaystyle \ forall x \ in S: \ varphi (x)}$${\ Displaystyle f}$${\ Displaystyle \ varphi (a)}$
• La fórmula se define como , por lo que una prueba de ella es una función f que convierte una prueba de en una prueba de . ${\ Displaystyle \ neg P}$${\ Displaystyle P \ a \ bot}$${\ Displaystyle P}$${\ Displaystyle \ bot}$
• No hay pruebas de (el absurdo o el tipo de fondo (no determinación en algunos lenguajes de programación)). ${\ Displaystyle \ bot}$

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 s = t es un cálculo que reduce los dos términos al mismo número.

Kolmogorov siguió la misma línea pero expresó 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 Q a P ; para resolverlo requiere un método para resolver el problema Q dado una solución al problema  P . ${\ Displaystyle P \ a Q}$

Ejemplos

La función identidad es una prueba de la fórmula , no importa lo que P es. ${\ Displaystyle P \ to P}$

La ley de no contradicción se expande a : ${\ Displaystyle \ neg (P \ wedge \ neg P)}$${\ Displaystyle (P \ wedge (P \ to \ bot)) \ to \ bot}$

• Una prueba de es una función que convierte una prueba de en una prueba de . ${\ Displaystyle (P \ wedge (P \ to \ bot)) \ to \ bot}$${\ Displaystyle f}$${\ Displaystyle (P \ wedge (P \ to \ bot))}$${\ Displaystyle \ bot}$
• Una prueba de es un par de pruebas < a ,  b >, donde es una prueba de P y es una prueba de . ${\ Displaystyle (P \ wedge (P \ to \ bot))}$${\ Displaystyle a}$${\ Displaystyle b}$${\ Displaystyle P \ a \ bot}$
• Una prueba de es una función que convierte una prueba de P en una prueba de . ${\ Displaystyle P \ a \ bot}$${\ Displaystyle \ bot}$

Poniéndolo todo junto, 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 , lo que demuestra la ley de no contradicción, no importa lo que P es. ${\ Displaystyle (P \ wedge (P \ to \ bot)) \ to \ bot}$${\ Displaystyle f}$${\ Displaystyle a}$${\ Displaystyle b}$${\ Displaystyle \ bot}$${\ Displaystyle \ bot}$${\ Displaystyle f}$${\ Displaystyle f (\ langle a, b \ rangle) = b (a)}$

De hecho, la misma línea de pensamiento proporciona también una prueba de dónde está cualquier proposición. ${\ Displaystyle (P \ wedge (P \ a Q)) \ a Q}$${\ displaystyle Q}$

Por otro lado, la ley del medio excluido se expande 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 tanto, si ni P ni es demostrable, tampoco lo es . ${\ Displaystyle P \ vee (\ neg P)}$${\ Displaystyle P \ vee (P \ to \ bot)}$${\ Displaystyle P \ vee (\ neg P)}$${\ Displaystyle P \ a \ bot}$${\ Displaystyle P \ a \ bot}$${\ Displaystyle P \ vee (\ neg P)}$

¿Qué es el absurdo?

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 hay una prueba de ; ver los teoremas de incompletitud de Gödel . En cambio, la interpretación BHK toma "no" para significar que lleva al absurdo, designado , de modo que una prueba de es una función que convierte una prueba de en una prueba de absurdo. ${\ Displaystyle P}$${\ Displaystyle P}$${\ Displaystyle P}$${\ Displaystyle P}$${\ Displaystyle \ bot}$${\ Displaystyle \ lnot P}$${\ Displaystyle P}$

Un ejemplo estándar de absurdo se encuentra al tratar con la aritmética. Suponga que 0 = 1 y proceda por inducción matemática : 0 = 0 por el axioma de igualdad. Ahora (hipótesis de inducción), si 0 fuera igual a un cierto número natural n , entonces 1 sería igual an  + 1, ( axioma de Peano : S m  =  S n si y solo si m = n ), pero como 0 = 1 , por lo tanto, 0 también sería igual an  + 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 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 . ${\ Displaystyle \ bot}$

¿Qué es una función?

La interpretación de BHK dependerá de la visión que se adopte sobre qué constituye una función que convierte una prueba en otra, o que convierte un elemento de un dominio en una prueba. 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 con el mismo número que y (que siempre es decidible para números naturales); de lo contrario, no hay prueba. Estos luego se construyen por inducción en algoritmos más complejos.

Si se considera que el cálculo lambda define la noción de función, entonces la interpretación de BHK describe la correspondencia entre la deducción natural y las funciones.

Referencias

• Troelstra, A. (1991). "Historia del constructivismo en el siglo XX" (PDF) . Citar diario requiere |journal= ( ayuda )
• Troelstra, A. (2003). "Constructivismo y teoría de la prueba (borrador)". CiteSeerX   10.1.1.10.6972 . Citar diario requiere |journal= ( ayuda )