Por que não acreditar na prova de consistência de Goedel para PA? Ou na de Kunen, baseada num algoritmo?
2011/9/30 Valeria de Paiva <valeria.depa...@gmail.com> > 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/ > -- 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
