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

• Ano de defesa: 2003
• Autor(a) principal: MARIA FERNANDA PALLARES COLOMAR
• Tipo de documento: Tese
• Tipo de acesso: Acesso aberto
• Idioma: por
• Instituição de defesa: MAXWELL
• Palavras-chave em Português: [pt] TEORIA DA PROVA; [pt] GENTZEN; [pt] PROVAS DE CONSISTENCIA; [en] PROOF THEORY; [en] GENTZEN; [en] CONSISTENCY PROOFS
• Link de acesso: https://www.maxwell.vrac.puc-rio.br/colecao.php?strSecao=resultado&nrSeq=4126&idi=1; https://www.maxwell.vrac.puc-rio.br/colecao.php?strSecao=resultado&nrSeq=4126&idi=2; http://doi.org/10.17771/PUCRio.acad.4126

[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.