Consequências Computacionais da lei do Terceiro Excluído

Recentemente em meu doutorado tenho dedicado grande esforço em compreender e utilizar a lógica intuicionista. Sendo extremamente simplista, a lógica intuicionista é um sistema formal que difere da lógica clássica em apenas um ponto: a lei do terceiro excluído e eliminação da dupla negação não são axiomas.

A lei do terceiro excluído é de simples compreensão: Toda proposição lógica deve ser verdadeiro ou falsa. Mais formalmente:

\forall p . P \lor \neg P

Aparentemente tal afirmação ingênua (e por sinal bastante lógica!) não possui nenhum tipo de complicação inerente ou mesmo qualquer relação com os fundamentos da computação. De acordo com o isomorfismo de Curry-Howard, caso sejamos capazes de construir uma prova para uma proposição qualquer, é possível extrair desta prova um programa funcional cujo tipo é isomórfico à proposição provada. Sendo assim, assuma o seguinte predicado halt(p) que é verdadeiro se um determinado programa p pára e falso caso contrário. Considere, então, agora a seguinte proposição:

\forall p. halt(p) \lor \neg halt(p)

Se o isomorfismo de curry howard estiver correto, podemos construir uma prova para esta afirmativa e esta poderia ser utilizada para obtermos um algoritmo que decide para um programa arbitrário p se este pára ou não. É fato bem conhecido, que o chamado problema da parada é indecidível e portanto não é possível obter tal programa. Então, qual o problema? O isomorfismo de Curry Howard está incorreto? O grande “pulo-do-gato” é que o isomorfismo de Curry-Howard é restrito à lógica intuicionista, que requer uma prova para afirmar que uma determinada proposição é verdadeira ou falsa.

É evidente que a adoção da lei do terceiro excluído é problemática em termos computacionais, já que esta implicaria na solução do problema da parada.

Anúncios

Deixe um comentário

Preencha os seus dados abaixo ou clique em um ícone para log in:

Logotipo do WordPress.com

Você está comentando utilizando sua conta WordPress.com. Sair / Alterar )

Imagem do Twitter

Você está comentando utilizando sua conta Twitter. Sair / Alterar )

Foto do Facebook

Você está comentando utilizando sua conta Facebook. Sair / Alterar )

Foto do Google+

Você está comentando utilizando sua conta Google+. Sair / Alterar )

Conectando a %s


%d blogueiros gostam disto: