Teorema de Gödel

Algumas pessoas já ouviram falar desse teorema. É um dos teoremas mais impactantes da Matemática do século passado. Diz que em toda teoria matemática que contenha a aritmética existem afirmações que não podem ser provadas...
A maioria das pessoas que ouviram falar desse teorema talvez não entenda seu verdadeiro enunciado, e talvez tenha muitas dificuldades pra entender sua demonstração (que raramente é posta na íntegra em textos da internet). Tanto é que alguns não Matemáticos refutam esse teorema (apesar de que "refutar teoremas" não faz muito sentido em Matemática, o que se faz é verificar se uma demonstração está correta ou não). Fala-se muita besteira na internet a respeito desse teorema por causa da falta de avisos contidos nos textos sobre o assunto. Por exemplo: Gödel não provou que a Matemática é inconsistente, mas apenas que teorias fortes são incompletas, no sentido que existem perguntas que a teoria não poderá responder. E isso apenas para teorias formais, ou seja, teorias definidasem um sentido preciso de lógica simbólica.
O que ele provou foi:
Toda teoria lógica formal em que se consegue definir as constantes, símbolos funcionais e relacionais da aritmética de Peano de primeira ordem, não é completa e (omega)consistente ao mesmo tempo. Não é completa no sentido de que existe uma fórmula sem variáveis livres (wff) que não pode ser provada verdadeira nem falsa pela teoria. E não é (omega)consistente no sentido que ou não é consistente ou existe uma fórmula (Existe x em IN tal que P(x)), tal que P(x) não vale pra nenhum x em IN no modelo correspondente a teoria. Mais tarde provaram que tal teoria não pode ser consistente e completa ao mesmo tempo.

Se a pessoa não entendeu o enunciado acima é melhor nem tentar comentar por aí sobre o teorema, fazer reflexões filosóficas esdrúxulas sobre o mesmo, e pior ainda: tentar refutá-lo (as tentativas de fazer isso levam a artigos risíveis do ponto de vista matemático, até mesmo uma falta de respeito com quem faz ciência de modo sério).
Bom, qual é a interpretação intuitiva do teorema?? Bom, uma delas é: não existe um algoritmo que produza todas as verdades aritméticas, ou mais informalmente, não existe um programa de computador que seja capaz de decidir exatamente quais fórmulas sobre os números naturais são válidas, por maior que ele seja. Em compensação, pode-se produzir um computador que produza somente verdades aritméticas, mas não todas elas.