Acho que pode valer a pena esclarecer ainda um pouco melhor este ponto gödeliano, para o benefício de outros colegas da lista que porventura possam fazer alguma confusão do mesmo gênero.
(Se eu falar alguma besteira ou for impreciso, você me corrige, ok, Doria?) > O seguinte não é correto: > > > O que Gödel mostrou é precisamente que isso não pode ser feito porque há > > verdades aritméticas que não podem ser demonstradas logicamente em qualquer > > sistema suficientemente forte para conter a aritmética. Não sei se percebeste, Desidério, mas a ambiguidade está antes de mais nada na ordem das tuas quantificações (como ocorre no Argumento da Causa Primeira): não é que haja "verdades aritméticas que não podem ser demonstradas logicamente em qualquer sistema" tal-e-tal (ou, como alguém pode entender daí, que haja verdades não demonstráveis em *nenhum* sistema tal-e-tal) suficientemente forte, mas mais precisamente que para cada sistema [omega-consistente, ou simplesmente consistente, e com um conjunto recursivamente enumerável de teoremas] "suficientemente forte" (basta este sistema conter a aritmética primitiva recursiva) há "verdades" que este sistema não será capaz de demonstrar. Se você acrescentar então esta verdade como novo axioma, obviamente ela passa a ser demonstrável, e o sistema resultante seria "mais completo" do que o anterior... Mas o diabo do resultado do Gödel implica a *incompletabilidade*, mais que a *incompletude* (eis aí mais uma má tradução), e ao acrescentar a tal "nova verdade" como teorema poder-se-á exibir em seguida uma outra verdade não demonstrável no novo sistema! (Nota as condições de aplicabilidade do teorema, entre colchetes/parênteses rectos. O problema de usar esta estratégia de ir acrescentando novas verdades para "completar" a axiomatização inicial falha justamente pelo fato de que o conjunto de asserções verdadeiras não é recursivamente enumerável.) > Já falei que PA + regra de Shoenfield, um sistema não-construtivo mas > razoável e manipulável, prova todas as verdades da aritmética. (E a > formulação acima está confusa: pega uma dessas verdades, X. O sistema PA + X > prova-a, sem problemas. Se X for ∏1, melhor ainda, pois PA + X é quase > irmão-gêmeo de PA.) Esclarecendo: PA é a "Aritmética de Peano", e a tal regra-ômega (o ômega é o ordinal do menor número transfinito) é simplesmente uma regra com um número enumerável de premissas que diz por exemplo que da verdade de P(0), P(1), ..., P(n), ... se pode derivar Ax.P(x), para todo natural x. Confesso que não faço idéia de qual seria a diferença da regra ômega de Shoenfield para a de qualquer outro cidadão, mas é fato que a regra aritmética da indução, por exemplo, obviamente segue da regra-ômega, estando esta última presente no sistema. É fato também que se pudermos falar em versões "construtivas" desta regra (por exemplo, com premissas definidas recursivamente), e se podemos aceitar tais versões desta regra como "meios finitários" válidos de inferência (é comum acordo que a aritmética primitiva recursiva como um todo só fornece "meios finitários válidos") talvez se possa salvar então algo do programa Formalista de Hilbert (uma boa questão, de qualquer forma, é o quanto de expressividade deve ser adicionada à linguagem objeto para que se possa expressar nela tais versões construtivas da regra-ômega). Há toda uma literatura sobre o assunto, com a qual não tenho muita familiaridade, e creio que outras pessoas da lista podem assumir a partir deste ponto. Finalmente, as sentenças do tipo Pi_1 são aquelas que têm a forma Ax.P(x), onde P expressa uma propriedade recursiva (efetivamente decidível) dos números naturais. As sentenças de incompletude do Gödel são deste tipo. O argumento gödeliano do Penrose em "Shadows of the Mind" sobre a implausibilidade de se criar um modelo computacional para a mente humana também menciona apenas sentenças deste tipo. Espero ter contribuído com mais clarificações do que obscuridades. JM _______________________________________________ Logica-l mailing list [email protected] http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l
