A idéia é criar uma sentença que diz: "eu não posso ser provada", ou seja, uma sentença, cujo número de godel é x, que diz que não existe demonstração para a fórmula cujo número de godel é x. Para entender a fórmula que godel criou, é necessário o conceito de variável livre. A fórmula "x é primo" possui uma variável livre x, não podemos deizer que ela é verdadeira ou falsa sem conhecer o valor de x. Para eliminar essa variável livre, tem duas maneiras: uma é substituir x por um número (p.ex. "7 é primo"), outra é colocar um quantificador ("existe x t.q. x é primo"). Note que uma fórmula sem variável livre (que chamamos "sentença") deve ser ou verdadeira ou falsa (i.e, sua negação verdadeira) em um modelo matemático fixado (que precisa ser definido, mas, intuitivamente, é uma interpretação para o significado das fórmulas). O sistema de axiomas ideal deve provar ou a sentença ou sua negação. Pois bem, godel cria uma sentença que não pode ser provada nem ela nem sua negação.
Para obter essa sentença, godel criou a fórmula PROVA(x,y,y) que significa: "A sequência de fórmulas cujo número é x é uma demonstração da fórmula (de número y) de uma variável livre, substituindo sua variável livre pelo valor y". Por exemplo, se 1000 é o número da fórmula "x é primo", PROVA(12345,1000,1000) diz: "12345 é o número da demonstração de "1000 é primo". A fórmula ¬ExPROVA(x,y,y) diz "a fórmula de número y, substituindo sua variável livre por y, não póde ser provada". No nosso exemplo, ¬ExPROVA(x,100,1000) diz "não existe demonstração de que 1000 é primo". Pois bem, ¬ExPROVA(x,y,y) tem uma variável livre y, e tem um número (seja g esse número). Portanto a fórmula ¬ExPROVA(x,g,g) é uma sentença (note que g não é uma variável, mas um número conhecido, que eu já calculei). E essa sentença diz: "A fórmula de número g, substituindo sua variável livre por g, não pode ser provada". Mas quem é a fórmula de número g? É o próprio ¬ExPROVA(x,y,y). E substituindo sua variável livre por g? É a propria sentença ¬ExPROVA(x,g,g). Portanto, ¬ExPROVA(x,g,g) diz "¬ExPROVA(x,g,g) não pode ser provada", que gera o paradoxo que queríamos (uma sentença que diz "eu não posso ser provada"). Observe que, se um sistema for consistente, eu de fato não consigo provar ¬ExPROVA(x,g,g). Mas isso se o sistema for consistente (i.e., não provar uma fórmula e sua negação). Caso contrário, tudo vira teorema, e tudo pode ser provado (de uma contradição provamos qualquer coisa), inclusive ¬ExPROVA(x,g,g). Mas se eu provar a consistência do sistema, eu acabei de provar que ¬ExPROVA(x,g,g) não pode ser provada. Mas isso, como vimos, é o próprio ¬ExPROVA(x,g,g), e chegamos numa contradição. Concluindo: a segunda parte do Teorema de Godel (conhecido como segundo teorema de godel) diz que, se um sistema for consistente, sua consistência não pode ser provada (dentro do próprio sistema). Uma observação importante é que, apesar de dar a idéia geral da demonstração, a demonstração que está no site está longe de ser completa. Fica a pergunta: como godel criou (ou provou que existe) a fórmula PROVA(x,y,y) usando só o fato de que o sistema é capaz de exprimir a aritmética e de que seus axiomas formam um conjunto recursivo (consigo decidir, através de um algoritmo finito, se uma fórmula é axioma ou não). É interessante olhar no trabalho original de godel ("On formally undecidable propositions of principia mathematica and related systens") como ele codifica cada axioma, e cada regra de inferência, em termos de relações aritméticas. Repare que a fórmula indecidível ¬ExPROVA(x,g,g), no fundo é uma gigantesca fórmula que só envolve números, conectivos lógicos, e as operações + e *. >From: Carlos Maçaranduba <[EMAIL PROTECTED]> >Reply-To: [EMAIL PROTECTED] >To: [EMAIL PROTECTED], [EMAIL PROTECTED] >Subject: Teorema de Godel >Date: Wed, 2 Jan 2002 18:43:16 -0300 (ART) > >neste endereço há uma demonstração do teorema de godel >que aparentemente é simples de se entender.Alguem >poderia ver a parte que ele usa o predicado >PROVA(x,g,g) e explicar-me pq ele faz isso????? > > >http://www.pr.gov.br/celepar/celepar/batebyte/edicoes/2000/bb95/teorema.htm > >_______________________________________________________________________________________________ >Yahoo! GeoCities >Tenha seu lugar na Web. Construa hoje mesmo sua home page no Yahoo! >GeoCities. É fácil e grátis! >http://br.geocities.yahoo.com/ _________________________________________________________________ Send and receive Hotmail on your mobile device: http://mobile.msn.com