[pt] APLICAÇÕES DA PRIMEIRA PROVA DE CONSISTÊNCIA APRESENTADA POR GENTZEN PARA A ARITMÉTICA DE PEANO

MARIA FERNANDA PALLARES COLOMAR

[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

Ficheros en el ítem

Ficheros	Tamaño	Formato	Ver
No hay ficheros asociados a este ítem.

Este ítem aparece en la(s) siguiente(s) colección(ones)

Documentos - PUC-RIO

Mostrar el registro sencillo del ítem