Análise estruturada e formal das provas

Abstract

Nesta dissertação introduzimos a Teoria da Prova através de sistemas dedutivos como o cálculo de Hilbert para a Lógica Proposicional Clássica e, de uma forma mais pormenorizada, o sistema de Dedução Natural para a Lógica Proposicional Clássica e para a Lógica de Primeira Ordem. As regras de inferência do sistema de Dedução Natural reflectem de forma convincente o raciocínio lógico envolvido nas provas matemáticas usuais. Apresentamos outros cálculos para a Lógica Proposicional Clássica: cálculo de sequentes, cálculo de Smullyan, e ainda, de uma forma resumida, o cálculo Intuicionista. Por fim, apresentamos uma discussão sobre provas de alguns resultados matemáticos abordadas no ensino secundário, fazendo uma análise comparativa entre as demonstrações standard e as correspondentesdemonstrações usando o sistema de Dedução Natural. Este último capítulo pode ser mais um elemento de apoio para os professores de Matemática do ensino secundário, pois permite-lhes uma melhor compreensão de alguns argumentos lógicos envolvidos nas provas de resultados matemáticos.

ABSTRACT: In this thesis, we introduce the Proof Theory by using some deductive systems. The systems we considered are the Hilbert Calculus for Classic Propositional Logic and, in more detail, the Natural Deduction system for the Classic Propositional Logic and for the First Order Logic. The inference rules of the Natural Deduction system, convincingly reflects the logical reasoning present in the usual mathematical proofs. We present other calculus for Classical Propositional Logic: sequents calculus, Smullyan calculus, and also briefly, the Intuitionist calculus. Finally, we discuss proofs of some mathematical results studied in the high school, by making a comparative analysis between standard proofs and the corresponding ones using the Natural Deduction system. This last study can be a useful resource for high school mathematics teachers, since it allows a better understanding of some logical arguments used in the proofs of some mathematical results.