Blog Marcos L. Mucheroni Filosofia, Noosfera e cibercultura

A ideia que podemos resolver problemas propondo um número finito de interações entre diversas tarefas (ou comandos como são chamados em linguagens de computação) para diversos problemas tem origem na Aritmética.
Ainda que a máquina de Charles Babbage (1791-1871), e a Álgebra de Boole (1815-1864) tenham uma enorme contribuição para os modernos computadores, a maioria dos lógicos e historiadores do nascimento do mundo digital, concorda que o problema de fato foi levantado pelo segundo problema de David Hilbert (1962-1943), numa conferência de 1900, em Paris.
Entre 23 problemas para a matemática resolver, alguns resolvidos recentemente como o Conjectura de Goldbach (veja nosso post), e outros a resolver, o segundo problema se propunha a provar que a aritmética é consistente, livre de qualquer contradição interna.
Nos anos de 1930, dois lógicos matemáticos, Kurt Gödel (1906-1975) e Gerhard Gentzen (1909-1945) provaram dois resultados que chamavam de novo atenção ao problema proposto, ambos se referiam a Hilbert, então de fato, ali está a origem da questão, grosso modo, se um problema enumerável é resolvido por um conjunto finito de passos.
Na verdade, a solução de Gentzen era uma prova da consistência dos axiomas de Peano, publicada em 1936, mostrava que a prova de consistência pode ser obtida em um sistema mais fraco do que a teoria de Zermelo-Fraenkel, usava axiomas da aritmética primitiva recursiva, não sendo portanto uma prova geral.
Já a prova da inconsistência da aritmética, chamada de segundo teorema da incompletude de Gödel, é mais completa e mostra que não é possível alguma prova da consistência dos axiomas de Peano ser desenvolvida sem essa própria aritmética.
Esse teorema afirma: se os únicos procedimentos de prova aceitáveis são aqueles que podem ser formalizados dentro da aritmética, então o problema de Hilbert não pode ser resolvido, dito de outra forma mais direta, se ou o sistema é completo ou consistente.
Há polêmicas levantadas sobre estes resultados, como Kreisel (1976) que afirmou que as provas eram sintáticas para problemas semânticos, Detlefsen(1990) que diz que o teorema não proíbe a existência de uma prova de consistência, e Dawson(2006) que afirmou que a prova da consistência é errônea usando a prova dada por Gentzen e do próprio Gödel em trabalho de 1958.
Polêmicas a parte, a participação de Kurt Gödel no importante circulo de Viena na década de 20 antes da guerra explodir, e as posteriores discussões de seus teorema por Alain Turing (1912-1954) e Claude Shannon (1916-2001) atentam sua importância para a história dos algoritmos e dos modernos computadores digitais.