Oi, Valeria, Minha msg foi uma provocação... Concordo com seu último parágrafo, como tenh0 insistido aqui - sobretudo porque a noção de conjunto de máquinas polinomiais, exponenciais, etc, só tem sentido se referida a algum sistema formal.
Na prova de Kunen vc vê a indução transfinita, sob forma de um cálculo de função que representa um sistema de notação de ordinais construtivos. PA não sabe disso, mas a gente sabe: o cálculo chega ao fim. 2011/9/30 Valeria de Paiva <valeria.depa...@gmail.com> > Doria, > eu nao conheco a prova do Kunen, nao posso opinar. > > quanto a prova do Goedel, se voce estiver falando da prova que usa a > interpretacao dialectica e a "negative translation" a razao pra nao > acreditar 'e dupla: voce pode nao acreditar em logica classica, > somente na intuicionistica e/ou voce pode nao acreditar que os > funcionais necessitados pela interpretacao sejam razoaveis. tem uma > discussao legal nos collected works editados pelo Feferman et al. > > pra terminar eu acho que tenho varias razoes pra nao acreditar nas > nocoes usuais de teoria da complexidade. elas sao "coding" da pior > especie, mascaram a realidade matematica, na minha opiniao. > > abs > Valeria > > 2011/9/30 Francisco Antonio Doria <famado...@gmail.com>: > > 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 > > > > > > > > -- > 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
