Este artigo é dividido em quatro partes. Esta é a primeira parte.
Vou basear muito da minha prosa no livro "Gödel's proof", de Nagel & Newman, e no famoso "Godel, Escher, Bach: an eternal golden braid" de Douglas Hofstadter. Este último livro é conhecido pelo carinhoso apelido de GEB pelos nerds mundo afora.
No artigo sobre aritmética de Peano, toquei no assunto dos axiomas, ou seja, como a aritmética com números naturais é definida por um punhado de definições muito simples, os axiomas de Peano.
Veja que "axiomas de Peano", "aritmética de Peano" e "aritmética normal" que aprendemos no ensino fundamental, são basicamente a mesma coisa. A diferença é a fundamentação lógica. No meu tempo, se alguém contestasse a afirmação 2+2=4, a professora batia com a régua na cabeça :) Argumentum ad baculum.
Relembrando uma parte dos axiomas de Peano:
Número é todo objeto que possui um sucessor y = S(x), então x é número [a] Não existe número cujo sucessor é zero não existe x tal que S(x) = 0 [b] O sucessor de um número é outro número y = S(x), y é número [c] Dois números diferentes possuem diferentes sucessores a ≠ b, S(a) ≠ S(b) [d] a = b, S(a) = S(b) [d*] Define-se "soma" de dois números como: x + S(y) = S(x + y) [e1] x + 0 = x (elemento neutro) [e2] Define-se "multiplicação" de dois números como: x . 0 = 0 [f1] S(x) . y = y + x . y [f2]
Axioma é uma afirmação que aceitamos sem discussão, seja por fé, ou porque é evidente, ou porque temos a intuição que é razoável.
Por exemplo, faz sentido (para nós) dizer que todo número tem sucessor, de modo que os diversos números formem uma seqüência contínua: 0, 1, 2, 3... Ou I, II, III, IV...
A notação utilizada realmente não importa. Conforme já dissemos no artigo sobre aritmética unária e Peano, o número "três" ou 3 ou III é apenas um rótulo para o terceiro sucessor de zero.
A partir dos poucos axiomas acima, podemos deduzir quase tudo na aritmética. Dá muito trabalho, assim como usar aritmética unária não seria prático. Mas o fato é que é possível, e isto nos assegura que a aritmética do dia-a-dia tem respaldo na lógica. Não há chance de chegar um extraterrestre amanhã e dizer "olha, isso aí tá tudo errado".
Vamos provar que 1+1=2. Você pode ter notado que eu rotulei os axiomas com letras entre colchetes, como [a]. Vou usar esta notação para apontar que axiomas apóiam cada passo da prova.
Primeiro, vamos provar um "lema", mostrando que x+1=S(x), estabelecendo uma relação bastante conveniente entre sucessão e soma:
S(0) = 1 [a] x + 1 = x + S(0) x + S(0) = S(x + 0) [e1] x + 1 = S(x) [e2]
Agora, a soma em si:
x + 1 = S(x) [lema] 1 + 1 = S(1) [fazendo x = 1] 1 + 1 = 2
Podemos fazer uma prova mais direta, que não produz o lema:
1 + 1 = S(0) + S(0) [a] S(0) + S(0) = S(S(0) + 0) [e1] S(S(0) + 0) = S(S(0)) [e2] 1 + 1 = S(S(0)) [a] 1 + 1 = S(1) 1 + 1 = 2
Altamente trabalhoso, mas serve para dar um respaldo filosófico, digamos assim.
Neste ponto, se começarmos a pensar filosoficamente, começam a aparecer muitas perguntas de cunho filosófico. Por exemplo:
Um conjunto de axiomas é dito "consistente" se ele não conduz a contradições. É mais fácil enxergar isto introduzindo deliberadamente um axioma "vilão", como 1+1=3.
Tal axioma, junto com os demais, torna a aritmética inconsistente, já que acabamos de provar que 1+1=2. Daí poderíamos deduzir que 2=3, S(2)=3 e S(2)=S(3), que conflita com o axioma [d].
Podemos continuar com este absurdo "provar" facilmente que 2=4 pois 2=3 e 3=S(3)=4. Finalmente, podemos dizer que a fórmula 1+1=x é "verdadeira" para qualquer valor de x, elevando-a ao nível de um teorema.
Segundo os logicistas, um sistema de axiomas inconsistente permite "provar" que qualquer fórmula é um teorema, ou seja, verdadeira sob quaisquer variáveis. Um sistema inconsistente permite "provar" inclusive a sua própria consistência. (É claro que tal prova não vale nada.) Esta é a marca de um sistema inconsistente.
Por outro lado, um "sintoma" de consistência de um sistema é a presença de fórmulas que não sejam teoremas. Por exemplo, a fórmula 1+1=x só é verdadeira quando x=2.
É um bom sinal, porém Gödel provou que um sistema consistente não pode provar que ele mesmo é consistente... Sistemas consistentes são forçosamente humildes.
Também a intuição nos diz que Peano parece ser consistente. Há uma prova "de verdade" da consistência de Peano (Gentzen) mas ela baseia-se na introdução de um conceito externo, novo (números ordinais), que vai além da aritmética. A aritmética "baunilha" não comporta tal prova.
Na verdade, há sistemas baseados em axiomas, consistentes, e que provam sua própria consistência, mas eles têm obrigatoriamente de ser "fracos", ou seja, com menos poder expressivo que a aritmética.
Há sistemas que foram criados deliberadamente fracos, como a aritmética de Presburger. Ela compartilha de algumas, mas não de todas características da aritmética normal. Por exemplo, nela não é possível definir o que é numero primo; mas é possível definir o que é número par ou ímpar.
A aritmética de Presburger é fraca, completa, consistente e decidível (vou esclarecer mais adiante o que é "decidível"). Ela torna-se tão poderosa quanto Peano (e deixa de ser completa e decidível) quando adiciona-se a ela a operação de multiplicação.
Nem sempre adicionar um axioma conflitante com os demais é uma má ideia. Considere o seguinte axioma:
Existe um número z tal que S(z) = 0
A priori este novo axioma conflita com [b] (zero não sucede nenhum número natural). Mas quem falou de números naturais? Se admitirmos que z é "não-natural", o novo axioma pode conviver com os demais.
É claro, nós sabemos que z=-1, um número inteiro negativo. Este novo axioma estica a aritmética dos naturais para os inteiros. O axioma [b] permanece na função de discriminante entre números naturais e inteiros.
Quanto à questão de provar teoremas usando meios automáticos, como um software de computador. Seria possível?
De fato é possível, e existem alguns softwares que fazem isto. São bastante úteis para conferir provas desenvolvidas por humanos, por exemplo. Mas esta possibilidade tem alguns limites, tanto teóricos quanto práticos.
Um limite prático é que trata-se de uma tarefa "difícil". Um teorema não-trivial pode demorar muuuuuito para ser provado, o que torna o procedimento inútil na prática. Um ser humano munido de papel e lápis tem mais chance, pois pode achar a prova do teorema por pura sorte.
É preciso tomar um certo cuidado para alimentar o software "provador" apenas com teoremas que sejam tratáveis, ou fornecer alguns "lemas" que facilitem o trabalho. Assim, o software permance útil e prova teoremas num tempo aceitável.
É prudente lembrar que verificar uma prova é diferente de elaborar um teorema (fórmula com prova). Embora ambas as atividades possam ser feitas mecanicamente, elaborar teoremas é infinitamente mais difícil.
Na verdade, elaborar teoremas é muito fácil; um computador pode cuspir zilhões deles, mas não sabe julgar quais destes teoremas são úteis, inéditos, ou elegantes. O matemático humano trabalha "ao contrário": parte de uma hipótese, ou mesmo algo observado empiricamente, e aí tenta elaborar uma prova, sabendo onde quer chegar.
O limite teórico dos programas verificadores de provas é ditado pela incompleteza de Gödel. falaremos mais deste cidadão e da sua teoria ao longo deste texto.
Gödel provou que nem toda verdade matemática é um teorema que possa ser demonstrado. Há verdades que são independentes dos axiomas de Peano.
Ou seja, a aritmética não é completa; nem todo fato da aritmética possui prova baseada na própria aritmética. A começar pelos axiomas de Peano, é claro; eles simplesmente existem, sem prova. Mas além deles, há infinitos outros.
Um possível exemplo é a conjectura de Goldbach: todo numero par é (talvez) a soma de dois primos. Todos os testes sugerem que a conjectura é verdadeira, mas ninguém provou isso, ainda.
Então, Goldbach pode ser a) um teorema cuja prova ainda não foi encontrada; b) uma verdade matemática nova, ou seja, um axioma; c) uma afirmação falsa, pois há um número par x que não é a soma de dois primos.
Supondo que de fato a conjectura de Goldbach seja verdadeira mas não possa ser provada, o que acontece? Bem, ela pode ser admitida como um novo axioma, o "axioma de Goldbach". Com a ajuda dele, muitos outros teoremas, que hoje não passam de hipóteses, passam a ser válidos.
Um computador pode ficar procurando para sempre por esta resposta, sem nunca encontrar. Esta possibilidade caracteriza o sistema como indecidível. Sistemas de axiomas mais "fracos", como a aritmética de Presburger, são decidíveis porque nestes há a certeza que "um dia" o computador achará a resposta. Existe um algoritmo para procurar a resposta e é possível calcular quanto tempo ele vai levar. (Lembra que eu prometi lá em cima a esclarecer o que era "decidível"? Aí está.)
(Note que o problema prático que mencionamos antes — que o algoritmo pode demorar um tempo inaceitavelmente longo — continua existindo para sistemas decidíveis.)
Este artigo é dividido em quatro partes. Esta é a primeira parte. Clique aqui para abrir a próxima parte..