Lógica proposicional via Lindenbaum-Tarski e Curry-Howard

Abstract

Pretendemos neste trabalho estudar a Lógica Proposicional enquanto “projecção” de duas correspondências di ferentes que a têm como parte comum. A primei ra estabelece uma ponte lógico-algébrica, a Álgebra de Lindenbaum-Tarski, e a segunda uma ponte lógico-operacional, o Isomorfismo de Curry-Howard. Debruçamo-nos sobre os dois paradigmas proposicionais que historicamente motivaram estas correspondências: a Lógica Proposicional Clássica e a Lógica Proposicional Intuicionista, respectivamente. Int roduzimos três cálculos lógicos e duas semânticas para ambos os paradigmas, e ainda o cálculo operacional por excelência – o Cálculo Lambda. Recorrendo à noção de assinatura em Álgebra Universal, uniformizamos o tratamento dado às três teorias em estudo. A título de exemplo do alcance das correspondências estabelecidas, exibimos duas consequências para as Lógicas Proposicionais Clássica e Intuicionista provenientes via Lindenbaum-Tarski e Curry-Howard: o Teorema de Glivenko e a consistência das Lógicas, respectivamente. Finalmente, propomos uma explicação geral para a “tradução” das reduções lambda, via Curry-Howard, enquanto normalização de provas onde ocorra o Metateorema de Dedução imediatemante seguido do Metateorema do Modus Ponens. O famoso Hauptsatz de Gentzen resulta como caso particular. Sugerimos ainda como desenvolvimento futuro uma generalização do Cálculo Lambda à 1ª ordem que segue de muito perto o seu tratamento tradicional.

In this work we intend to study Propositional Logic as “proj ection” of two different correspondences that have it as common part. The fi rst one establishes a logical -algebraic bridge, the Lindenbaum-Tarski, and the second one a logical-operational bridge, the Curry-Howard isomorphism. We focus our attention on the two propositional paradigms which historically motivated these correspondences: Classical Propositional Logic and Intuitionistic Propositional Logic, respectively. We introduce three logical calculi and two semantics for both paradigms, as well as the operational calculus by excellence – the Lambda Calculus. Borrowing the notion of signature from Universal Algebra, we uniformize the treatment given to the three theories under study. As an example of the established correspondences’ range, we exhibit two consequences for Classical and Intuitionistic Propositional Logic given via Lindenbaum-Tarski and Curry-Howard: Gli venko’s Theorem and the consistency of both Logics, respectively. Finally, we propose a broader explanation for the “translation” of the lambda reductions, via Curry-Howard, as proof normalization where the Deduction Metatheorem occurs immediately followed by the Detachment Metatheorem. Gentzen’s famous Hauptsatz results as a particular case. We also suggest as future development a first order generalization of the Lambda Calculus which follows very closely its traditional treatment.