Re: Defini��o de N�mero e teorema de Godel

["Nicolau C. Saldanha" <nicolau@xxxxxxxxxxxxxx>]

On Fri, 4 Jun 1999, Paulo Santa Rita wrote:

> O Teorema de Godel se situa no campo da l�gica-matem�tica e mantem estreitas 
> liga��es com a filosofia. Ele deriva de uma an�lise exaustiva do Trabalho de 
> Bertrand Russel - Os Principia - sobre os fundamentos l�gicos da matem�tica.
> Neste sentido ele n�o se fundamenta em "axiomas tradicionais" tais como 
> vemos costumeiramente...

O parentesco entre o teorema de G�del e os trabalhos de Russel � que ambos
fazem uso de varia��es do paradoxo do barbeiro/paradoxo do mentiroso.
Russel usou estas id�ias para fornecer mais um paradoxo para a vers�o
de teoria dos conjuntos pr�-ZF: seja

R = { X | X \not\in X };

(onde \not\in significa "n�o pertence")

temos, para todo X, X \in R se e somente se X \not\in X.
Tomando X = R temos R \in R se e somente se R \not\in R,
uma contradi��o.

O teorema de G�del � um teorema exatamente no sentido cl�ssico:
de proposi��o demonstrada a partir de um conjunto de aximas usando l�gica
de primeira ordem. A diferen�a � que ele fala de proposi��es e
demonstra��es (ao inv�s de falar de n�meros primos, elipses, conjuntos de
Cantor...).

> A prova parece bastante complexa e existem muitos bons livros de divulga��o 
> sobre o tema: � um racioc�nio engenhoso no qual Godel mostra como podemos 
> representar por n�meros afirma��es (teoremas) sobre n�meros e, a seguir. 
> aplicado de forma engenhosa e correta uma vers�o v�lida paradoxo matem�tico 
> bastante conhecido.

Acho que a melhor demonstra��o que se pode dar atualmente para o teorema
de G�del � a partir do problema da parada.

Consideremos um computador idealizado, sem limite predeterminado de
mem�ria. Neste computador vamos executar programas (em uma linguagem
tamb�m idealizada). Um programa � descrito por um inteiro (obtido
considerando-o como a expans�o de um n�mero na base N, onde N � maior
do que o n�mero de s�mbolos permitidos; nos computadores de verdade
poder�amos tomar N = 256). Alguns programas recebem um ou mais inteiros
como entrada. Alguns programas terminam sua execu��o em tempo finito
e outros nunca param.

Ser� poss�vel decidir algoritmicamente olhando para um programa P e para
sua entrada n se a execu��o vai parar algum dia? Ou seja, ser� que existe
um programa X que recebe como entradas [P] (o n�mero do programa P) e n e
responde "para" ou "n�o para", sempre ap�s um tempo finito? 
A resposta � n�o.

A raz�o � que se existisse X poder�amos facilmente construir um outro
programa Q que, recebendo como entrada [P], para se e somente se
P, recebendo como entrada [P], n�o para. Basta a Q rodar X com entradas
[P] e [P] e aguardar a resposta; se a resposta for "n�o para", Q para;
se a resposta for "para", Q joga-se deliberadamente em loop infinito.
O paradoxo do barbeiro aparece se fazemos Q receber [Q]:
a execu��o para se e somente se a execu��o n�o para...

Voltando ao teorema de G�del, n�o � dif�cil convencer-se que a afirma��o
"a execu��o do programa P com entrada n para depois de tempo finito"
pode ser traduzida para a aritm�tica. Se for verdadeira, a frase
ser� um teorema: basta exibir a execu��o completa.
� portanto imposs�vel escrever um programa que decida em tempo finito
se frases deste tipo s�o teoremas. Com mais forte raz�o, � imposs�vel
escrever um programa que decida se uma proposi��o aritm�tica � um teorema.

Mas se toda proposi��o aritm�tica (A) fosse um teorema ou a nega��o de um
teorema, seria muito f�cil escrever um programa que decidisse qual das
duas possibilidades � a correta: basta procurar
sistematicamente demonstra��es de (A) e de (n�o A).
Assim, existem proposi��es que n�o s�o nem teoremas nem a nega��o de
teoremas, i.e., que n�o podem ser nem provadas nem refutadas.

> Se me permite uma opini�o, o que � maravilhoso no teorema de Godel � que ele 
> demonstra ( ou sugere ) que a vis�o intuicionista ou platonica � mais 
> consistente que a formalista e que a "realidade matem�tica ( Como diria 
> Poincare )" � t�o consistente e verdadeira e dotada dee um sabor e de uma 
> vida perene

Pessoas diferentes derivaram consequ�ncias filosoficas diferentes a partir
do teorema de G�del. Ser� que devemos concluir a partir do teorema que
existem proposi��es *humanamente* indecid�veis? Turing e muitos outros
acham que sim, e baseiam-se na cren�a de que a mente humana pode ser
explicada a partir do mecanismo do corpo (especialmente do c�rebro),
e que o corpo por sua vez obedece as leis da f�sica, que podem ser
simuladas (em princ�pio, pelo menos) pelo nosso computador idealizado.
Assim, tudo o que a mente humana faz seria algoritmico. Mas o pr�prio
G�del defende o ponto de vista oposto: para ele o teorema "mostra" que a
mente humana *n�o* � uma m�quina, e que seu comportamento n�o �
algoritmico. Penrose defendeu este mesmo ponto de vista no livro "shadows
of the mind". Eu pr�prio tendo a ficar do lado de Turing, mas � uma
quest�o de opini�o...