O teorema da normalização para lógica de primeira ordem

Abstract

Nesta dissertação apresentamos um estudo sobre a Dedução Natural, cujo objectivo principal é a demonstração do Teorema da Normalização, quer para a Lógica Clássica, quer para a Lógica Intuicionista. Apresentamos também alguns dos corolários e aplicações imediatas do Teorema da Normalização, em particular algumas das propriedades mais características da Lógica Intuicionista, como o teorema da separação, a propriedade da disjunção e a propriedade do quantificador existencial. O processo de normalização usa operações de substituição, em derivações, de variáveis por termos e de hipóteses por derivações. Associadas a estas operações estão condições de substituibilidade, que garantem que as condições de aplicabilidade das regras de inferência dos quantificadores são satisfeitas. Esta tese contém um tratamento rigoroso destas questões.

In this dissertation we present a study of Natural Deduction, whose main goal is to prove the Normalization Theorem, both for Classic Logic and Intuitionistic Logic. We also present some of the corollaries and immediate applications of the Normalization Theorem, in particular some of the most characteristic properties of Intuitionistic Logic, like the separation theorem, the disjunction property, and the existential quantifier property. The normalization process makes use of the operations of substitution, in derivations, of terms for variables and of derivations for hypotheses. There are substitutivity conditions associated with those operations, which guarantee the satisfaction of the side conditions of quantifiers' inference rules. This thesis contains a rigorous treatment of these matters.