Minha dúvida sobre o trabalho do Nelson é de outra natureza: mesmo que todas as expectativas se confirmem e realmente a coisa esteja furada, o que ainda poderá ser dito da *alternativa finitista* que ele propõe para "consertar PRA"? Será um sistema metamatemático cujo interesse poderá subsistir de modo independente a todo o resto?
Parte do trabalho do Nelson já está incorporada na lógica. Ele é um dos precursores da aritmética limitada. O livro predicative arithmetic, de 1986, está disponível online na página dele. Contém os primeiros passos do projeto dele. De especial interesse para lógicos é a aritmetização dos teoremas da lógica básica em sistemas interpretaveis em Q. Ele segue o Shoenfield, cap. 1 a 4. Ele consegue provar uma boa parte dos resultados, mas não consegue alguns resultados centrais. Nessa parte, acho que o melhor que ele conseguiu foi demonstrar o teorema de extensões funcionais (com unicidade) em um sistema compatível com Q e sem ter que fazer a prova enfadonha que tem no Kleene (que aliás é um livro é pouco humano). A prova desse teorema no Shoenfield não cabe em sistemas aceitáveis para o Nelson. Os resultados centrais que ele não consegue: Hilbert-Ackerman, Herbrand, Skolem (sobre extensões funcionais em geral) e tudo o mais relacionado a esses. Por que não dá para obter esses resultados? Hilbert-Ackerman e Herbrand provam a consistência de Q. O teorema de Skolem, eu não sei. Quem trabalha com aritmética limitada deve saber. O segundo teorema da incompletude também é modificado. Como Hilbert-Ackerman tem um papel central para o Nelson, ele consegue versões restritas do teorema (também dá para conseguir versões restritas de eliminação do corte e outros). Essa história de limitar rank e level das constantes especiais nas provas é para isso: a teoria que ele chama de Q* só prova a consistência das "subteorias" tais que as provas são por consequência tautológica de axiomas com rank e level limitados. Com isso ele consegue um mínimo de teoria de sistemas formais para, pelo menos, dar sentido para "formalização". Não é grande coisa. Considero que perder Herbrand é muito sério: a pureza de métodos está indo embora. Mas acho que é possível aceitar que trabalhando nessa aritmética limitada como metateoria dos sistemas formais (no lugar de PRA) faz sentido falar em "formalização". A partir daí você pode ter dois pontos de vista: 1) Essencialmente o ponto de vista de Hilbert trocando PRA por Q, Q* e outras teorias dessa aritmética do Nelson. Nesse caso, você formaliza a matemática em ZFC e trabalha normalmente, sempre lembrando que a metateoria é essa aritmética limitada. Isso vai gerar algumas preocupações só para quem trabalha em fundamentos. É preciso ver se forcing por exemplo é finitário nesse sentido. O resto da matemática fica igual. Não é possível dar provas de consistência, mas tudo bem, você continua praticamente como estamos hoje. 2) O ponto de vista atual do Nelson: PRA é inconsistente. Aí eu acho que não dá para fazer nada. Nem entendo o que significam essas afirmações dele. É praticamente uma contradição referencial ele dizer que exibe dois números n e m tal que a tetração n tetra m não existe. É aquela pergunta: o que faz o algoritmo que calcula essa superexponencial em termos das anteriores nesse caso? O erro desse trabalho do Nelson, que acredito já foi encontrado, está onde teria que estar. O erro está no plano básico do argumento, não em detalhes excruciantes de aritmetização (alguns desses detalhes podem ser encontrados já nesse livro de 1986). A aritmetização do teorema de Chaitin não fornece o que ele gostaria que fosse o caso. Se o erro estivesse em detalhes da aritmetização, o argumento dele seria usado para provar que ZFC prova que PA é inconsistente, já que em ZFC não há problemas de falta de recurso para codificação. Ou seja, se o plano dele estivesse correto, mas os detalhes não, ele conseguiria pelo menos uma prova da inconsistencia de ZF, o que já seria suficientemente interessante. E ele está gastanto centenas de páginas de aritmetização e está apenas no começo... Abraço Rodrigo _______________________________________________ Logica-l mailing list Logica-l@dimap.ufrn.br http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l
