[en] APPLICATIONS OF THE FIRST CONSISTENCY PROOF PRESENTED BY GENTZEN FOR PEANO ARITHMETIC

Autor: MARIA FERNANDA PALLARES COLOMAR
Jazyk: portugalština
Rok vydání: 2003
Předmět:
Druh dokumentu: TEXTO
DOI: 10.17771/PUCRio.acad.4126
Popis: [pt] Na antologia que M.E. Szabo realizara dos trabalhos de Gentzen e publicara em 1969 se transcrevem, em um apêndice, algumas passagens apresentadas por Bernays ao editor pertencentes a uma primeira prova de consistência para a Aritmética de Peano realizada por Gentzen que não tinha sido publicada até então. À diferença das outras provas de consistência realizadas por Gentzen e já conhecidas na década de trinta, esta prova não utiliza o procedimento de indução transfinita até e0. Ao contrário, baseia-se na definição de um processo de redução de seqüentes que se associa sistematicamente a todo seqüente derivável permitindo reconhecê-lo como verdadeiro. Nós reconstruímos essa prova realizando algumas variações e estudamos o modo pelo qual a técnica principal utilizada (a definição do processo de redução de seqüentes) pode ser vista em relação a resultados da lógica clássica de primeira ordem tais como provas de completude. A parte central da nossa dissertação é a realização de uma versão desta prova de consistência para um sistema formal para a Aritmética de Heyting.
[en] In the antology of Gentzens works made by M.E.Szabo and published in 1969, we find out in an appendix, some passages presented by Bernays to the editor. These texts belong to a first proof of Peanos Arithmetic consistency that Gentzen did not publish. In a different way from the other proofs of consistency made by Gentzen and already known in the thirties, this proof does not use the procedure of transfinite induction up to e0. On the contrary, it is based on the definition of a reduction process for sequents that is systematically associated to every derivable sequent allowing us to recognize it as a true sequent. We reconstructed this proof making some variations and we studied how the main technique used (the definition of the reduction process) could be seen in relation with other results of first order logic like proofs of completness. The main part of our dissertation is another version of this consistency proof for a formal system for Heyting Arithmetic.
Databáze: Networked Digital Library of Theses & Dissertations
Externí odkaz: