Título: | APPLICATIONS OF THE FIRST CONSISTENCY PROOF PRESENTED BY GENTZEN FOR PEANO ARITHMETIC | ||||||||||||||||||||||||||||||||||||||||
Autor: |
MARIA FERNANDA PALLARES COLOMAR |
||||||||||||||||||||||||||||||||||||||||
Colaborador(es): |
LUIZ CARLOS PINHEIRO DIAS PEREIRA - Orientador |
||||||||||||||||||||||||||||||||||||||||
Catalogação: | 14/NOV/2003 | Língua(s): | PORTUGUESE - BRAZIL |
||||||||||||||||||||||||||||||||||||||
Tipo: | TEXT | Subtipo: | THESIS | ||||||||||||||||||||||||||||||||||||||
Notas: |
[pt] Todos os dados constantes dos documentos são de inteira responsabilidade de seus autores. Os dados utilizados nas descrições dos documentos estão em conformidade com os sistemas da administração da PUC-Rio. [en] All data contained in the documents are the sole responsibility of the authors. The data used in the descriptions of the documents are in conformity with the systems of the administration of PUC-Rio. |
||||||||||||||||||||||||||||||||||||||||
Referência(s): |
[pt] https://www.maxwell.vrac.puc-rio.br/projetosEspeciais/ETDs/consultas/conteudo.php?strSecao=resultado&nrSeq=4126&idi=1 [en] https://www.maxwell.vrac.puc-rio.br/projetosEspeciais/ETDs/consultas/conteudo.php?strSecao=resultado&nrSeq=4126&idi=2 |
||||||||||||||||||||||||||||||||||||||||
DOI: | https://doi.org/10.17771/PUCRio.acad.4126 | ||||||||||||||||||||||||||||||||||||||||
Resumo: | |||||||||||||||||||||||||||||||||||||||||
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.
|
|||||||||||||||||||||||||||||||||||||||||
|