Rodrigo, Muito obrigada pela informacao detalhada abaixo! Aprendi muito, mas continuo com uma duvidas basica.
Nao, eu nao quero fazer "aritmetica limitada" e nao quero perder consistencia. Mas quero saber se voce (e todo mundo que a gente acredita) tambem acha que PRA realmente 'e garantidamente consistente. obrigada, valeria 2011/9/29 Rodrigo Freire <freires...@gmail.com>: > 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 > > > > > > > > > > > > -- Valeria de Paiva http://www.cs.bham.ac.uk/~vdp/ http://valeriadepaiva.org/www/ _______________________________________________ Logica-l mailing list Logica-l@dimap.ufrn.br http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l
