Aplicações da primeira prova de consistência apresentada por Gentzen para a artimetica de Peano

Na antologia que M.E. Szabo 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 e 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é .Ao contrário, se baseia na definição de um processo de redução de sequentes que se associa sistematicamente a todo sequente derivável permitindo reconhecê-lo como verdadeiro. Nós reconstruímos essa prova realizando algumas variações e estudamos o modo em que a técnica principal utilizada (a definição do processo de redução de sequentes) 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 v ersão desta prova de consistência para um sistema formal para a Aritmética de Heyting.