[pt] APLICAÇÕES DA PRIMEIRA PROVA DE CONSISTÊNCIA APRESENTADA POR GENTZEN PARA A ARITMÉTICA DE PEANO
[en] APPLICATIONS OF THE FIRST CONSISTENCY PROOF PRESENTED BY GENTZEN FOR PEANO ARITHMETIC
| dc.contributor | LUIZ CARLOS PINHEIRO DIAS PEREIRA | |
| dc.creator | MARIA FERNANDA PALLARES COLOMAR | |
| dc.date | 2003-11-14 | |
| dc.date.accessioned | 2022-09-21T21:42:03Z | |
| dc.date.available | 2022-09-21T21:42:03Z | |
| dc.identifier | https://www.maxwell.vrac.puc-rio.br/colecao.php?strSecao=resultado&nrSeq=4126@1 | |
| dc.identifier | https://www.maxwell.vrac.puc-rio.br/colecao.php?strSecao=resultado&nrSeq=4126@2 | |
| dc.identifier | http://doi.org/10.17771/PUCRio.acad.4126 | |
| dc.identifier.uri | https://hdl.handle.net/20.500.12032/42318 | |
| dc.description | [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. | |
| dc.description | [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. | |
| dc.language | pt | |
| dc.publisher | MAXWELL | |
| dc.subject | [pt] TEORIA DA PROVA | |
| dc.subject | [pt] GENTZEN | |
| dc.subject | [pt] PROVAS DE CONSISTENCIA | |
| dc.subject | [en] PROOF THEORY | |
| dc.subject | [en] GENTZEN | |
| dc.subject | [en] CONSISTENCY PROOFS | |
| dc.title | [pt] APLICAÇÕES DA PRIMEIRA PROVA DE CONSISTÊNCIA APRESENTADA POR GENTZEN PARA A ARITMÉTICA DE PEANO | |
| dc.title | [en] APPLICATIONS OF THE FIRST CONSISTENCY PROOF PRESENTED BY GENTZEN FOR PEANO ARITHMETIC | |
| dc.type | TEXTO |
Files in this item
| Files | Size | Format | View |
|---|---|---|---|
|
There are no files associated with this item. |
|||