Leo Gordeev acaba de me comunicar um bonito teorema de consistência para teorias T com aritmética suficiente e um conjunto recursivamente enumerável de teoremas. Chama de Con* uma propriedade que é, waving hands, não existe uma prova de uma contradição limitada por uma função F especificada.
Se F é a função usada na definição exótica de P<NP, então T + Con*T não pode ser provada em T. E T + Con*T < T + ConT, estrito. Leo mostra, mais ainda, que há uma hierarquia infinita Con* < Con** < Con***... até Con, usual. Esse negócio de consistência é delicado mesmo. E essas funções F são muito estranhas, e pouco exploradas. São como que Busy Beavers relativos.
_______________________________________________ Logica-l mailing list [email protected] http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l
