Mostrar el registro sencillo del ítem

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

dc.contributorLUIZ CARLOS PINHEIRO DIAS PEREIRA
dc.creatorMARIA FERNANDA PALLARES COLOMAR
dc.date2003-11-14
dc.date.accessioned2022-09-21T21:42:03Z
dc.date.available2022-09-21T21:42:03Z
dc.identifierhttps://www.maxwell.vrac.puc-rio.br/colecao.php?strSecao=resultado&nrSeq=4126@1
dc.identifierhttps://www.maxwell.vrac.puc-rio.br/colecao.php?strSecao=resultado&nrSeq=4126@2
dc.identifierhttp://doi.org/10.17771/PUCRio.acad.4126
dc.identifier.urihttps://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.languagept
dc.publisherMAXWELL
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.typeTEXTO


Ficheros en el ítem

FicherosTamañoFormatoVer

No hay ficheros asociados a este ítem.

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

Mostrar el registro sencillo del ítem


© AUSJAL 2022

Asociación de Universidades Confiadas a la Compañía de Jesús en América Latina, AUSJAL
Av. Santa Teresa de Jesús Edif. Cerpe, Piso 2, Oficina AUSJAL Urb.
La Castellana, Chacao (1060) Caracas - Venezuela
Tel/Fax (+58-212)-266-13-41 /(+58-212)-266-85-62

Nuestras redes sociales

facebook Facebook

twitter Twitter

youtube Youtube

Asociaciones Jesuitas en el mundo
Ausjal en el mundo AJCU AUSJAL JESAM JCEP JCS JCAP