Em 1936 Kleene publicou um teorema da incompletude diverso do de Gödel: usa uma sentença Pi_2 e esta implica de modo estrito a sentença de Gödel que formaliza a consistência de PA. Kreisel combina este resultado com a prova de Gentzen e obtem uma hierarquia sobre PA indexada pelos ordinais recursivos. Daqui sai uma prova relativamente simples da consistência de PA, que Ken Kunen formalizou em 1994 num programa de computador essa prova de que PA é consistente (consistência dada pela sentença de Gödel que formaliza a consistencia de PA).
Isso mesmo: um programa de computador que prova a consistência de PA. Muito bonito. -- fad ahhata alati, awienta Wilushati _______________________________________________ Logica-l mailing list Logica-l@dimap.ufrn.br http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l
