Interpretação de Brouwer–Heyting–Kolmogorov

Em Lógica matemática, a interpretação de Brouwer–Heyting–Kolmogorov, ou interpretação BHK, de Lógica intuicionista foi proposta por L. E. J. Brouwer, Arend Heyting e independentemente por Andrey Kolmogorov. É também chamada às vezes de interpretação de realizabilidade, devido a sua conexão com a teoria de Realizabilidade por Stephen Kleene.

A interpretação

A interpretação afirma exatamente o que deve ser uma prova de uma dada Fórmula (lógica). Isso é especificado por Indução estrutural daquela fórmula:

• Uma prova de $P\wedge Q$ é um par <a, b> onde a é uma prova de P e b é uma prova de Q.
• Uma prova de $P\vee Q$ é um par <a, b> onde a é 0 e b é uma prova de P, ou a é 1 e b é uma prova de Q.
• Uma prova de $P\to Q$ é uma função f que converte uma prova de P em uma prova de Q.
• Uma prova de $\exists x\in S:\phi (x)$ é um par <a, b> onde a é um elemento de S, e b é uma prova de φ(a).
• Uma prova de $\forall x\in S:\phi (x)$ é uma função f que converte um elemento a de S em uma prova de φ(a).
• A fórmula $\neg P$ é definida como $P\to \bot$, então uma prova disto é uma função f que converte uma prova de P em uma prova de $\bot$.
• Não há prova de $\bot$ (o absurdo).

A interpretação de uma proposição primitiva deve ser conhecida a partir do contexto. No contexto da aritmética, uma prova da fórmula s=t é um cálculo de redução dos dois termos com o mesmo numeral.

Kolmogorov seguia a mesma linha, mas expressou sua interpretação em termos de problemas e soluções. Afirmar uma fórmula é afirmar saber a solução para o problema representado por essa fórmula. Por exemplo $P\to Q$ é o problema da redução de Q para P; resolvê-lo requer um método para resolver o problema Q dada uma solução para o problema P.

Exemplos

A função identidade é uma prova da fórmula $P\to P$, independente do valor de P.

O Princípio da não contradição $\neg (P\wedge \neg P)$ expande a $(P\wedge (P\to \bot ))\to \bot$:

• Uma prova de $(P\wedge (P\to \bot ))\to \bot$ é uma função f que converte uma prova de $(P\wedge (P\to \bot ))$ em uma prova de $\bot$.
• Uma prova de $(P\wedge (P\to \bot ))$ é um par de provas <a,b>, onde a é uma prova de P, e b é uma prova de $P\to \bot$.
• Uma prova de $P\to \bot$ é uma função que converte uma prova de P em uma prova de $\bot$.

Consequentemente, uma prova de $(P\wedge (P\to \bot ))\to \bot$ é uma função f que converte um par <a,b> – onde a é uma prova de P, e b é uma função que converte uma prova de P em uma prova de $\bot$ – em uma prova de $\bot$. A função $f(\langle a,b\rangle )=b(a)$ se encaixa bem, provando a lei de não-contradição, independente do que P seja.

Por outro lado, a Lei do terceiro excluído $P\vee (\neg P)$ expande a $P\vee (P\to \bot )$, e de modo geral não possui prova. De acordo com a interpretação, uma prova de $P\vee (\neg P)$ é um par <a, b> onde a é 0 e b é uma prova de P, ou a é 1 e b é uma prova de $P\to \bot$. Assim, se nem P nem $P\to \bot$ pode ser provado então também não podemos provar $P\vee (\neg P)$.

O que é absurdo?

De modo geral não é possível a um Sistema formal possuir um operador de negação formal tal que exista uma prova de ¬P exatamente quando não há uma prova de P ; Ver Teoremas da incompletude de Gödel. A interpretação BHK em vez disso utiliza ¬P para significar que P leva a um absurdo, leia-se $\bot$, de modo que uma prova de ¬P é uma função que converte uma prova de P em uma prova de absurdo.

Um exemplo padrão de absurdo é encontrado na aritmética. Assuma que 0 = 1, e prossiga por Indução matemática: 0 = 0 pelo axioma da igualdade. Agora (hipótese indutiva), se 0 fosse igual a um certo número natural n, então 1 seria igual a n+1, (Axiomas de Peano: Sm = Sn se e somente se m = n), mas como 0=1, 0 por conseguinte também seria igual n + 1. Por indução, 0 é igual a todos os números, e portanto quaisquer dois números naturais tornam-se iguais.

Portanto, existe uma forma de ir de uma prova de 0=1 a uma prova de qualquer igualdade aritmética básica, e consequentemente para uma prova de qualquer proposição aritmética complexa. Além disso, para obter esse resultado não foi necessário invocar o Axioma de Peano que afirma que 0 "não" é o sucessor de qualquer número natural. Isso torna 0=1 adequado como $\bot$ na Aritmética de Heyting (e o axioma de Peano é reescrito 0 = Sn → 0 = S0). Este uso de 0 = 1 valida o Princípio de explosão.

O que é uma função?

A interpretação BHK dependerá do entendimento sobre o que constitui uma função que converte uma prova para outra, ou que converte um elemento de um domínio para uma prova. Diferentes versões do construtivismo vão divergir sobre este ponto. Diferentes versões de Construtivismo (matemática) irão divergir neste ponto.

A teoria de realizabilidade de Kleene identifica as funções com a Função computável. Ela lida com Aritmética de Heyting, onde o domínio de quantificação são os números naturais e as proposições primitivas são da forma x = y. Uma prova de x = y é simplesmente o algoritmo trivial se x der como resultado o mesmo número que y der (o que é sempre decidível para os números naturais), caso contrário, não há nenhuma prova. Estes são, então, desenvolvidos por indução em algoritmos mais complexos.

Se considerarmos o Cálculo lambda como definição do conceito de uma função, então a interpretação BHK descreve o Isomorfismo de Curry-Howard entre dedução natural e funções.

Referências

• Troelstra, A. (1991). "History of Constructivism in the Twentieth Century"
• "O Isomorfismo de Curry-Howard via Teoria de Categorias"
• "The Development of Intuitionistic Logic"