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/ _______________________________________________ Logica-l mailing list Logica-l@dimap.ufrn.br http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l
