Notas sobre lógica e a correspondência Curry-Howard

Todos fatos conhecidos, mas que eu estou entendendo um pouco melhor somente há pouco tempo. Senão vejamos: na lógica de primeira ordem a sintaxe é estratificada em duas camadas: termos e fórmulas. Os termos representam os valores sobre alguma estrutura sobre a qual se fala; as fórmulas tratam de propriedades sobre os termos. Pode-se interpretar a lógica intuicionista de primeira ordem no λ-cálculo tipado de primeira ordem: os termos são os valores (não necessariamente em sua forma normal, ou seja, não necessariamente avaliados) e as fórmulas são tipos, que são propriedades dos termos. Então um tipo é como se fosse um predicado sobre um termo, o que faz todo sentido. Isso é mais ou menos a essência da correspondência Curry-Howard.

Mas a coisa fica melhor. Na lógica de primeira ordem só podemos quantificar sobre variáveis, que são parte de termos. Na lógica de segunda ordem pode-se quantificar sobre predicados também. O correspondente no λ-cálculo é o Sistema F de Girard, que é um λ-calculo tipado de segunda ordem, no qual pode-se estabelecer abstrações de tipos e aplicações de tipos. Girard utilizou o Sistema F para estudar o PA₂, a aritmética de Peano de segunda ordem, e provar sua consistência. De forma similar temos a lógica de ordem superior e o Sistema F de ordem superior (Fω). A quantificação no caso da lógica é sobre predicados e predicados de predicados e por aí vai; no sistema Fω os tipos de ordem superior são como funções de tipos em tipos (no Sistema F de segunda ordem existem apenas funções de tipos em termos), em qualquer nível. Mais uma vez, Girard utilizou esse sistema para estudar o PA_ω, a aritmética de Peano de ordem superior, e provar sua consistência pela propriedade de normalização dos termos no sistema Fω.

Já na lógica de ordem superior a formulação mais utilizada é devida a Alonzo Church e, como esperado, envolve o λ-cálculo. É utilizado um cálculo tipado pois o cálculo sem tipos é inconsistente, graças ao paradoxo de Russell. Lógica de ordem superior também é utilizada como base para provadores de teoremas, por exemplo o sistema Isabelle/HOL. Um outro provador de teoremas famoso, o Coq, utiliza um cálculo baseado em tipos dependentes, que estabelecem uma conexão entre termos e tipos. Mas isso fica para outra hora.