Dois cientistas formalizaram um teorema sobre a existência de Deus escrito pelo matemático Kurt Gödel. Mas o viés de Deus é uma espécie de distração – o verdadeiro passo à frente é o exemplo que ele estabelece de como os computadores podem tornar mais simples o progresso científico.

A reportagem é de David Knight, publicada na revista Der Spiegel e reproduzida no Portal Uol, 28-10-2013.

No que diz respeito às manchetes, está é certamente uma atraente. "Cientistas provam a existência de Deus", escreveu o jornal diário alemão Die Welt na semana passada.

Mas, não é nenhuma surpresa, há uma ressalva bastante significativa nessa afirmação. Na verdade, o que os pesquisadores em questão dizem ter realmente comprovado é um teorema apresentado pelo renomado matemático austríaco Kurt Gödel – e a verdadeira notícia não é sobre um Ser Supremo, mas sim sobre o que se pode alcançar hoje nos campos científicos usando uma tecnologia superior.

Quando Gödel morreu em 1978, deixou para trás uma teoria tentadora baseada nos princípios da lógica modal – a teoria de que deve existir um ser superior. Os detalhes matemáticos envolvidos na prova ontológica de Gödel são complicados, mas em essência, o austríaco argumentou que, por definição, Deus é aquele para o qual não se pode conceber nada maior. E embora Deus exista no entendimento do conceito, poderíamos concebê-lo como algo maior se ele existisse na realidade. Portanto, ele deve existir.

Mesmo na época, o argumento não era exatamente novo. Durante séculos, muitos tentaram usar esse tipo de raciocínio abstrato para provar a possibilidade ou a necessidade da existência de Deus. Mas o modelo matemático composto por Gödel propôs uma prova da idéia. Seus teoremas e axiomas – pressupostos que não podem ser comprovados – podem ser expressos como equações matemáticas. E isso significa que podem ser comprovados.

Provando a existência de Deus com um MacBook

É aí que entram Christoph Benzmüller, da Universidade Livre de Berlim, e seu colega Bruno Woltzenlogel Paleo, da Universidade Técnica de Viena. Usando um computador MacBook comum, eles demonstraram que a prova de Gödel estava correta – pelo menos em nível matemático – por meio da lógica modal superior. Sua apresentação inicial no servidor de artigos científicos arXiv.org é chamada de "Formalização, Mecanização e Automação da prova da existência de Deus de Gödel".

O fato de que a formalização desses teoremas complicados pode ser feita por computadores abre todo tipo de possibilidades, disse Benzmüller à Spiegel Online. "É totalmente incrível que a partir deste argumento liderado por Gödel, todas essas coisas possam ser provadas automaticamente em poucos segundos ou menos num notebook comum", disse ele.

O nome Gödel pode não significar muito para alguns, mas entre os cientistas ele goza de uma reputação semelhante à de Albert Einstein – que era seu amigo. Nascido em 1906 na então Áustria-Hungria e hoje a cidade tcheca de Brno, Gödel mais tarde estudou em Viena antes de se mudar para os Estados Unidos após a eclosão da 2ª Guerra Mundial para trabalhar em Princeton, onde Einstein também estava. A primeira versão desta prova ontológica está em anotações datadas de cerca de 1941, mas foi só no início da década de 1970, quando Gödel temia que pudesse morrer, que ela veio a público.

Agora Benzmüller espera que usar um exemplo que atraia tantas manchetes possa chamar atenção para o método. "Eu não sabia que criaria tanto interesse público, mas (a prova ontológica de Gödel) foi definitivamente um exemplo melhor do que alguma coisa inacessível em matemática ou inteligência artificial", acrescentou o cientista. "É uma coisa muito pequena e clara, porque estamos lidando apenas com seis axiomas num pequeno teorema. (...) Pode haver outras coisas que usam um lógica similar. Podemos desenvolver sistemas de computador para verificar cada única etapa e verificar se estão certas agora?"

Uma lógica expressiva ambiciosa

Os cientistas, que vêm trabalhando juntos desde o início do ano, acreditam que seu trabalho pode ter muitas aplicações práticas em áreas como inteligência artificial e verificação de software e hardware.

Benzmüller também apontou que há muitos cientistas trabalhando em áreas semelhantes. Ele próprio foi inspirado a enfrentar o problema por um livro intitulado "Tipos, Tableaus e o Deus de Gödel", de Melvin.

O uso de computadores para reduzir a carga dos matemáticos não é novo, embora não seja bem recebido por todos no campo. O matemático norte-americano Doron Zeilberger tem citado o nome Shalosh B. Ekhad em seus trabalhos científicos desde 1980.

Segundo a Fundação Simons com sede em Nova York, o nome é na verdade um pseudônimo para os computadores que ele usa para ajudar a provar, em segundos, teoremas que antes exigiam página após página de raciocínio matemático. Zeilberger diz que deu ao computador um nome humano "para mostrar que os computadores devem receber o crédito quando isso é devido". O "fanatismo centrado no humano" por parte dos matemáticos, diz ele, tem um progresso limitado.

Em última análise, é improvável que a formalização da prova ontológica de Gödel conquiste muitos ateus, tampouco que conforte os verdadeiros crentes, que podem argumentar a ideia de que um poder superior é aquele que desafia a lógica, por definição. Para os matemáticos que procuram maneiras de abrir novos caminhos, no entanto, a notícia pode representar uma resposta às suas orações.