[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.
| Identifer | oai:union.ndltd.org:puc-rio.br/oai:MAXWELL.puc-rio.br:4126 |
| Date | 14 November 2003 |
| Creators | MARIA FERNANDA PALLARES COLOMAR |
| Contributors | LUIZ CARLOS PINHEIRO DIAS PEREIRA |
| Publisher | MAXWELL |
| Source Sets | PUC Rio |
| Language | Portuguese |
| Detected Language | English |
| Type | TEXTO |
Page generated in 0.0021 seconds