Nem olhei direito o manuscrito, mas pelo que entendi o Nelson afirma ter provado em PRA que Q é inconsistente.
É conhecido que PRA prova que Q é consistente (corolário do teorema de Hilbert-Ackerman). Até onde posso compreender, "PRA prova que uma teoria T é inconsistente" significa que é possível exibir uma função primitiva recursiva f e um número natural n tal que f(n) é uma prova da inconsistencia em T. Acho que o argumento do Nelson é que uma tal f para a teoria Q não é total: f não para na entrada n. Daí, a inconsistência de PRA. É muito mais grave do que PA ser inconsistente. PRA é considerada a teoria que representa o raciocínio finitário. Teoremas centrais da lógica são demonstrados em PRA: eliminação do corte, Herbrand, etc. Por exemplo, eliminar corte aumenta muito o tamanho da prova. A operação de eliminar corte poderia não ser total na concepção do Nelson. É difícil até interpretar essa prova do Nelson: ele toma a consistência de Q como certa, mesmo "exibindo" no sentido finitário uma prova da inconsistência de Q. Claro que a matemática não finitária vai toda embora. O Nelson parece não estar muito preocupado, disse que vai fazer uma nova fundamentação da matemática. O problema é que não vai sobrar nada para ser fundamentado: exponenciação nos naturais não é total. Cálculo 1 vai embora. Se PRA é incosistente, acredito que não restará nada que mereça o título de "conhecimento". Abraço Rodrigo _______________________________________________ Logica-l mailing list [email protected] http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l
