Uma prova irrefutável de que na matemática é impossível provar tudo.

Em fins do século XIX, no Congresso de Matemática de Paris, em 1900, Hilbert, renomado professor em Göttingen apresentou 23 problemas, que segundo ele estariam ocupando os matemáticos do século XX. Seu segundo problema perguntava se é possível provar que os axiomas da aritmética são consistentes, isto é, dado um número finito de passos lógicos corretos, nunca se chegará a uma contradição. Na esteira desse problema, Bertran Russell, um filósofo matemático (ou será matemático filósofo?) em 1910, começou uma série de livros (Principia Mathematica), na qual, baseado nos axiomas de Peano, desenvolvia todo um programa de formalização da matemática. A tentação era saborosa: provar que lógica e matemática eram a mesma coisa. Mas, o segundo problema de Hilbert continuava em aberto. Estudos posteriores de um jovem matemático austríaco, Kurt Gödel, emigrado para os EUA, que se consubstanciaram no teorema que leva o seu nome, deram o tiro de misericórdia na pretensão. Gödel provou que num sistema lógico formal existem assertivas verdadeiras que não podem ser provadas. Foi mais um sopetão na pretensão homocêntrica do Universo (assim como fizeram Copérnico, Darwin e Freud, só para ficar nos mais evidentes). Antes de passar pro Gödel, diga-se apenas que dos 23 problemas, aproximadamente a metade ainda não tem solução (terá algum dia?), e pior (ou melhor) a matemática se desenvolveu em centenas de direções nem sonhadas por Hilbert. Ainda bem que o trabalho final dele, terminava com a citação: Enquanto uma ciência oferece abundância de problemas, ela está viva.

Antes de entrar no tema, precisamos rever alguma coisa da lógica formal. Será o nosso jargão, por assim dizer. A Lógica remonta aos gregos (o poder de argumentação significava poder político nas democracias gregas). Sobre esta base, constrói-se a lógica matemática que a partir de Leibnitz (século XVII) começa o seu desenvolvimento. A partir daqui, chega-se ao primeiro alicerce: a lógica proposicional (aquela que só admite os valores F e V) e a lógica de primeira ordem (na qual os elementos do alfabeto são infinitos).

Sobre isto, se constrói:

• A matemática clássica, sobre a qual se constroem todas as ciências exatas.

• A computação.

• Lógica modal (além de V e F temos necessariamente V ou F e possivelmente V ou F).

• Lógica temporal (aquela cujos resultados dependem do tempo).

• Lógica linear.

• Lógica com mais de 2 valores (além de V e F, temos a ignorância e o contraditório: V e F juntos).

• Lógica de ordem superior.

Seja um exemplo ainda dos gregos: Protágoras ensinou Euathlos a argumentar. Pelo curso, Euathlos ficou de pagar uma certa quantia. Metade no fim do curso e a outra metade quando Euathlos ganhasse a sua primeira causa. Como o pagamento da segunda metade demorasse, Protágoras processou Euathlos.

Argumentos:

De Protágoras: Se ele ganhar, terá que me pagar (já que ele ganhou a sua primeira causa). Se ele perder, terá que me pagar, já que eu ganhei a causa contra ele.

De Euathlos: Se eu ganhar, nada terei que pagar, já que ganhei a causa. Se eu perder, nada terei que pagar, já que não ganhei ainda nenhuma causa.

Pergunta-se: quem está com a razão??

A lógica proposicional, busca descrever a realidade e se constrói sobre poucos conceitos, a saber:

1. Suponhamos querer afirmar que Mendes joga bilhar. Isso poderia ser escrito como a proposição BilharMendes, e que obviamente teria o valor V. Outra proposição poderia ser BilharJorge, que também seria V. Já a proposição BilharCadeira é claramente F, já que nenhuma cadeira joga bilhar.

2. Suponhamos querer encadear conhecimentos, do tipo: Se está quente, choverá. Usaremos o símbolo Þ (lê-se implica), e escrever-se-á: Quente Þ Chuva.

3. Podemos negar afirmações, do tipo: se chove, não há sol. Fica Chuva Þ ~Sol.

PS: Antes de continuar, reconheça-se a fragilidade da lógica para tratar o mundo real. Não há noção de passado / presente / futuro, e nem dá pra falar do tempo de Curitiba... Mas são os defeitos de qualquer modelagem. Não há o que fazer, a não ser ir em frente.

4. São necessários 2 conectivos, E (^) e OU (Ú), para tornar mais ricas as frases. Podemos dizer que a Fulana é rica e boazuda. Ficaria: BoazudiceFulana ^  RiquezaFulana. Nesse caso, para que a assertiva completa seja verdadeira, a Fulana terá que ser rica e boazuda. Já o conector OU, funciona parecido. Podemos dizer que Fulano é inteligente ou maluco. A frase em lógica seria: InteligênciaFulano Ú MaluquiceFulano. A assertiva seria V, se qualquer uma das duas o fosse.

Até aqui, a lógica é chamada proposicional, porque se baseia em proposições claramente V ou F. Mas, isso é incompleto para descrever o mundo, senão vejamos o problema famoso:

Sócrates é homem. Todo homem é mortal, logo... Sócrates é mortal.

O problema surge ao ter que se tratar o fato de que Sócrates é uma instância de homem. A regra não se aplica só a Socrates, e sim a todos os homens. Nasce a necessidade de quantificadores, a menos que estejamos interessados em fazer uma proposição distinta para um dos homens da terra.

O passo seguinte, é passar da lógica de proposições para a lógica de predicados. Aqui, a proposição BilharMendes, seria escrita Bilhar(Mendes), mostrando claramente que Mendes é uma das pessoas que joga bilhar, ou Mendes tem o predicado Bilhar. Na lógica de predicados precisamos de 2 novos símbolos, chamados qualificadores. O Universal é "  (lê-se qualquer que seja), e o Existencial é $ (lê-se existe). Introduz-se aqui o conceito de variável, que pode assumir qualquer valor dentro de um domínio especificado.

Eis como ficaria a frase "Quem trabalha duro ou é amigo do chefe, tem promoção" em lógica de predicados:

"x Promoção(x) Þ TrabalhaDuro(x) Ú AmigoChefe(x)

Ou a frase: "Todo funcionário tem um chefe"
                    "x $y ÉChefe(y,x).

Há uma distinção aqui: assertivas iniciais do problema, são chamadas axiomas, enquanto conclusões obtidas a partir das regras da lógica e dos axiomas originais, são chamados teoremas. O processo recebe o nome pomposo de Modus Ponens, que nada mais é que "Se há uma axioma E1 Þ E2, e há outro axioma E1, segue-se que E2 é V".

Há também outra regra de inferência chamada Modus Tolens, que diz: Se há um axioma E1 Þ E2, e há também ~E2, segue-se logicamente que ~E1. (Donde o símbolo Þ pode ser lido como se e somente se).

A demonstração de um teorema pode seguir dois caminhos. O primeiro, chamado RESOLUÇÃO, vai operando os axiomas e os teoremas até topar com o teorema que se quer provar. O segundo chamado REFUTAÇÃO, parte da negação lógica do que se quer provar e mediante as tratativas usuais chega a um ponto em que uma contradição é encontrada. Está provado o teorema original.

Para que os teoremas possam ser provados, todos os axiomas e teoremas precisam estar na fórmula de cláusulas. Para conseguir isso, usam-se as seguintes regras:

1. Eliminar a implicação, lembrando que A Þ B pode ser escrito como ~A Ú B

2. Reduzir o escopo do ~, lembrando que
            ~~A = A                    (Não aperte F10 para não atualizar... Aperte                                                 F10 para atualizar)

            ~(A^B) = ~A Ú ~B (e vice-versa ~(A Ú B) = ~A^ ~B) (Lei de Morgan)
                                              Supondo que P = Aluno aprovado, F =                                                 freqüência acima de 75% e N = nota maior                                                 que 7. Então P Þ (F ^ N). Negando P - o que                                                 seria a reprovação, fica: ~P Þ ~F Ú ~N

            ~"x P(x) = ~P(x)      (Não há qualquer um que seja marciano = não                                                 há marcianos)  

           ~$x P(x) = "x ~P(x) (Não existe uma pessoa que seja azul = para                                                 qualquer pessoa, ela não será azul)

3. Separar as variáveis que querem dizer coisas diferentes. Como os nomes são só referências, isso não altera a cláusula.

"x P(x) Ú "x Q(x) deve ser trocado para

"x P(x) Ú "y Q(y)

4. Deslocar todos os quantificadores para a esquerda. Isso agora pode ser feito, pois não há mais confusão de nomes, graças ao passo 3.

5. Eliminar o $, graças a um truque descoberto por Skolem em 1920. Trata-se de introduzir uma função (sobre a qual nada se sabe ainda), mas que permite ir em frente. Por exemplo: $x Maluco (x), pode ser trocado por Maluco(S1), onde S1 é a função proposta, e que em tempo oportuno dirá V ou F em relação à maluquice. A propósito, o nome da função "S" é homenagem a Skolem.

6. Retirar os quantificadores. Graças às etapas anteriores, isso pode ser feito. (Acredite por enquanto, no exemplo a seguir, virá senão uma prova, pelo menos uma razoável indicação de que isso funciona).

7. Separar as clásusulas unidas por ou em cláusulas unidas por E (graças a DeMorgan).

O resultado final é uma série de cláusulas, cada uma delas unidas por E, que fica implícito.

A resolução agora é tomar duas cláusulas quaisquer, que resolvidas dão origem a uma nova cláusula. Para tanto, em cada uma das cláusulas juntadas deve haver o mesmo literal ora afirmado ora negado. Esses dois se cancelam, e a cláusula resultante é o que sobrou da anulação.

Se se tentar o processo de resolução por refutação (o mais fácil), deve-se acrescentar a negação do teorema a provar.

Vamos a um exemplo: Seja uma mesa que tem 2 tijolos, um sobre o outro. O de baixo é A, e o de cima é B. Claramente pode-se afirmar que Sobre(B,A) é V, e que Sobre(A,Mesa) também é V. Queremos provar que B está em cima da mesa. Ou, Acima(B,mesa).

Axiomas:

"x "y [Sobre(x,y) Þ Acima(x,y)]

"x "y "z [Acima(x,y) ^ Acima(y,z) Þ Acima(x,z)]

Percorrendo os procedimentos acima, os axiomas ficam

~Sobre (u, v) Ú Acima (u, v)

~Acima(x, y) Ú ~Acima(y, z) Ú Acima(x, z)

Queremos provar Acima(B, mesa), logo introduzimos ~Acima (B, mesa). Fica o conjunto

(1) ~Sobre (u, v) Ú Acima (u, v)

(2) ~Acima (x, y) Ú ~Acima(y, z) Ú Acima (x, z)

(3) Sobre (B, A)

(4) Sobre (A, mesa)

(5) ~Acima (B, mesa)

Tomando (2) e (5) fazendo x = B e z = mesa, juntando e anulando, fica

(6) ~Acima(B, y) Ú ~Acima(y, mesa)

Tomando (1) e (6) fazendo u = y e v = mesa, fica

(7) ~Sobre (y, mesa) Ú ~Acima (B, y)

Tomando (1) com (7) fazendo u = B e v = y, fica

(8) ~Sobre (B, y) Ú ~Sobre (y, mesa)

Tomando (3) e (8) fazendo y = A

(9) ~Sobre (A, mesa)

Tomando (4) e (9), ambas se anulam e o resultado é NIHIL. Logo, a assertiva negada estava correta.

Há ainda o teorema da unificação, que permite - em tempo finito - substituir literais dentro das cláusulas, (já que homem (João) e ~homem (José) não podem se anular, são coisas diferentes) devido a Kowalski em 1970. Do trabalho dele surgiu a Linguagem PROLOG.

Bom, tudo isso foi para construir o jargão. Agora vamos ao Gödel. Seu teorema se baseia em um processo de 3 etapas:

1. Estabelecer as regras pelas quais axiomas (e teoremas) podem gerar novos teoremas (é isso que eu tentei mostrar aí em cima).

2. Estabelecer os axiomas da aritmética em linguagem de lógica de predicados.

3. Estabelecer uma forma de numeração para os teoremas assim gerados.

Pulando a etapa 1, (já vista...(?), vamos para a etapa 2). Eis os axiomas de Peano para os números naturais. Note-se que o símbolo s denota sucessor, um conceito primitivo. O sucessor de 0 é 1, de 1 é 2, ... de n é n+1:

1. "x ~(0=sx)                          [Não existe x tal que 0 seja seu sucessor]

2. "x, y (sx = sy) Þ (x = y)     [Se 2 números têm o mesmo sucessor, são                                                   iguais]

3. "x  x+0 = x                          [0 é o elemento neutro na adição]

4. "x, y x+sy = s(x+y)             [x somado com o sucessor de y é igual ao                                                  sucessor de x+y]

5. "x, y  x × sy = xy + x           [x=2, y=5 leva a 2 × 6 = 2.5 + 2 = 12]

6. "x x × 0 = 0                        [0 é o elemento absorvente na multiplicação]

7. "x x = x

8. "x,y,z (x=y) Þ ((x = z) Þ (y = z))
          [propriedade transitiva]

9. "x,y (x=y) Þ (A(x,x) Þ A(x,y)) [A é qualquer fórmula com 2 variáveis livres]

10. (P(0) ^ "x P(x) Þ P(sx))) Þ "x P(x) [Regra fundamental da indução matemática]

Com estas informações, Gödel, passou à etapa 3 do teorema, usando a tabela a seguir:

Note-se que só existe a variável x. Logo quando só aparece x, ele será identificado como x₁. Quando aparecerem x e y, eles serão x₁ e x₁₁, e assim por diante.

Agora para cada cláusula, Gödel bolou um número, que mais tarde foi chamado "Número de Gödel", e que é construído da seguinte maneira. Tomam-se os primos a partir do 2. São eles: 2, 3, 5, 7, 11, 13, 17, 23, 29...

Cada axioma terá seu número de Gödel calculado por um sistema de numeração onde as bases são os primos e os expoentes são o numerinho da tabela acima. Pra clarear, vejamos o número de Gödel do axioma 4 de Peano:

"x, y x+sy = s(x+y)                      [Escrito em matematiquez]

x₁ + sx₁₁ = s(x₁ + x₁₁)                [Escrito em Gödelez], e o número é:

2⁹ .3¹⁰ . 5³ . 7² . 11⁹ . 13¹⁰ . 17¹⁰ . 19⁵ . 23² . 29⁶ . 31⁹ . 37¹⁰ . 41³ . 43⁹ . 47¹⁰ . 53¹⁰ . 59⁷

Note-se que o numerão é enorme, mas isso é de propósito. É para que, dado um número, SE ELE FOR UM NÚMERO DE GÖDEL, possa-se recuperar qual o axioma ou teorema que lhe deu origem. Basta fatorá-lo em seus componentes primos, e verificar qual o expoente de cada um dos primos. Ou seja, a relação axioma - número de Gödel é bi-unívoca.

Calma que estamos chegando perto da prova:

Seja o predicado PROVA(x,y,z), lido como x é o número de Gödel da prova da fórmula Y (que tem número de Gödel y), o qual teve o inteiro z inserido dentro dela. Note-se que PROVA(x,y,z) é um jeito fácil de escrever uma imensa e longa expressão onde aparecem x₁, x₁₁ e x₁₁₁, Essa expressão inclui muitos procedimentos, entre eles:

• dado um inteiro, fatore-o em seus fatores primos;
• ache a expressão que lhe deu origem;
• verifique se a expressão é uma fórmula;
• verifique se ela está provada;

Claramente são procedimentos irrealizáveis na prática, mas, em princípio, computáveis.

Vamos considerar um caso especial do predicado acima: Suponha que a fórmula Y é alimentada com seu próprio número de Gödel, e vamos tentar negar a existência de tal prova. Escreve-se

~$x PROVA(x,y,y)

Em palavras: x é o número de Gödel da prova obtida na fórmula Y pelo número y (Número de Gödel de Y). Vamos chamar ao número de Gödel da PROVA(x,y,y) de g.

Finalmente:

~$x PROVA(x,g,g) é verdadeiro, mas não é provável (no sentido de poder ser provado) no sistema aritmético formal.

A demonstração ocupa poucas linhas:

Suponha que ~$x PROVA(x,g,g) é provável (no mesmo sentido) e seja p o número de Gödel dessa prova P. Então, nós temos que PROVA(p,g,g) é verdadeiro, desde que P é a prova de G, na qual foram substituídas as variáveis livres. MAS, a veracidade de PROVA(p,g,g) contradiz ~$x PROVA(x,g,g), e daqui temos que não existe essa prova P.

Então, se tudo foi construído direitinho, a afirmação ~$x PROVA(x,g,g) é verdadeira e portanto não existe a PROVA(x,g,g) dentro do sistema.

Em resumo: Dentro de um sistema de lógica formal existem teoremas que são indecidíveis.

Este tema está em conexão com o Paradoxo de Russel (O barbeiro da aldeia barbeia todos os homens que não se barbeiam sozinhos.) e com o argumento de Turing de que não há máquina de Turing capaz de resolver o problema de quando parar. Todos eles se baseiam na genial sacada de Cantor, chamada de corte diagonal, quando ele estudava o infinito. E que segundo a Jane, o levou à loucura...

A propósito, Gödel também sofreu surtos paranóicos que determinaram sua internação em hospícios por longos períodos, em vários momentos de sua vida.

Tinha muito medo que lhe envenenassem a comida e, um belo dia, deixou de comer. Pois é, morrendo de fome logo depois. Como dizia um professor meu, "A matemática é fogo na roupa".

DEWDNEY, A. K. The Turing Omnibus: 61 excursions in computer science. Rockville: Computer Science Press, 1989.

FUCHS, Walter R. A matemática moderna. São Paulo: Polígono, 1970.

PENROSE, Roger. The emperors new mind: concerning computers, minds, and laws of physics. Oxford: Oxford University Press, 1989.

RICH, Elaine. Inteligência artificial. São Paulo: Makron, 1993.

WINSTON, Patrick Henry. Inteligência artificial. Rio de Janeiro: LTC, 1988.