Teoremas da incompletude de Gödel – Wikipédia, a enciclopédia livre

Este artigo ou secção contém uma lista de referências no fim do texto, mas as suas fontes não são claras porque não são citadas no corpo do artigo, o que compromete a confiabilidade das informações. Ajude a melhorar este artigo inserindo citações no corpo do artigo. (Janeiro de 2015)

Os teoremas da incompletude de Gödel são dois teoremas da lógica matemática que estabelecem limitações inerentes a quase todos os sistemas axiomáticos, exceto aos mais triviais. Os teoremas, provados por Kurt Gödel em 1931, são importantes tanto para a lógica matemática quanto para a filosofia da matemática. Os dois resultados são amplamente, mas não universalmente, interpretados como indicações de que o programa de Hilbert para encontrar um conjunto completo e consistente de axiomas para toda a matemática é impossível, dando uma resposta negativa para o segundo problema de Hilbert.

O primeiro teorema da incompletude afirma que nenhum sistema consistente de axiomas, cujos teoremas podem ser listados por um “procedimento efetivo” (e.g., um programa de computador que pode ser qualquer tipo de algoritmo), é capaz de provar todas as verdades sobre as relações dos números naturais (aritmética). Para qualquer um desses sistemas, sempre haverá afirmações sobre os números naturais que são verdadeiras, mas que não podem ser provadas dentro do sistema. O segundo teorema da incompletude, uma extensão do primeiro, mostra que tal sistema não pode demonstrar sua própria consistência.

• Teorema 1: "Qualquer teoria axiomática recursivamente enumerável e capaz de expressar algumas verdades básicas de aritmética não pode ser, ao mesmo tempo, completa e consistente. Ou seja, em uma teoria consistente, sempre há proposições que não podem ser demonstradas nem verdadeiras, nem falsas".
• Teorema 2: "Uma teoria, recursivamente enumerável e capaz de expressar verdades básicas da aritmética e alguns enunciados da teoria da prova, pode provar sua própria consistência se, e somente se, for inconsistente."

No final do século XIX, a filosofia do conhecimento era considerada um bloco monolítico e muitos intelectuais da época consideravam que haveria pouca coisa fundamentalmente nova a ser descoberta. No Congresso Internacional de Matemática de Paris, em 1900, o jovem e genial David Hilbert, imbuído das ideias correntes, apresentou um surpreendente trabalho resumindo as 23 questões ainda "em aberto", as quais, após resolvidas, completariam todo o escopo da matemática.

Hilbert pretendia, como de fato foi parcialmente conseguido, desencadear um esforço geral da comunidade científica a fim de completar a fundamentação lógica da matemática. Nos poucos anos que se seguiram a maior parte das questões por ele propostas foram adequadamente resolvidas.

Em 1931, quando ainda vigorava a proposta de Hilbert de obter a completa construção da teoria matemática através da lógica formal, Gödel publicou o seu trabalho "Sobre as Proposições Indecidíveis", pondo fim a essa expectativa. Na Universidade de Princeton, o prestigiado Neumann, que trabalhava com afinco na proposta de Hilbert, imediatamente mergulhou nos trabalhos de Gödel, dando-lhe grande apoio.

Paralelamente, na Física, estava em pleno andamento o desenvolvimento da teoria quântica e quatro anos antes (1927) Heisenberg já divulgara seu "principio da incerteza", colocando um limite físico na experimentação microscópica direta. Foi mais um golpe nas hipóteses determinísticas da ciência.

Posteriormente, Church e Turing demonstraram que não existe nenhum algoritmo capaz de provar se "uma proposição qualquer faz ou não parte de uma teoria".

Curiosamente, até 1963, nem Gödel nem qualquer outro matemático havia apresentado alguma proposição que ilustrasse os teoremas da indecidibilidade. Somente então o jovem Paul Cohen, de Stanford, desenvolveu uma técnica para teste de proposições indecidíveis. Cohen mostrou que a hipótese do continuum, justamente uma das questões fundamentais da matemática, era indecidível.

Como afirmações da teoria formal estão escritas na forma simbólica, é possível verificar mecanicamente que uma prova formal de um conjunto finito de axiomas é válida. Essa tarefa, conhecida como verificação automática de provas, é relacionada a demonstração automática de teoremas. A diferença é que ao invés de construir uma nova prova, o verificador de prova simplesmente checa se a prova formal fornecida (ou em instruções que podem ser seguidas para criar a prova formal) é correta. Esse processo não é meramente hipotético; sistemas tais como Isabelle ou Coq são usados para formalizar provas e então verificar sua validade.

Muitas teorias de interesse incluem um conjunto infinito de axiomas, contudo. Neste caso, para verificar uma prova formal, deve ser possível determinar se a afirmação que é tida como axioma é realmente um axioma. Essa questão surge nas teorias de primeira ordem da aritmética, como a aritmética de Peano, porque o princípio da indução matemática é expresso como um conjunto infinito de axiomas (um esquema axiomático).

A teoria axiomática é tida como efetivamente gerada se seu conjunto de axiomas é um conjunto recursivamente enumerável. Isto significa que há um programa de computador que, em princípio, pode enumerar todos os axiomas da teoria sem listar qualquer afirmação que não é axioma. Isto é equivalente à existência de um programa que enumera todos os teoremas da teoria sem enumerar qualquer afirmação que não é teorema. Exemplos de teorias efetivamente geradas com conjunto infinito de axiomas incluem a aritmética de Peano e a teoria dos conjuntos de Zermelo-Fraenkel.

Ao escolher um conjunto de axiomas, um objetivo é que seja possível provar quantos resultados corretos forem possíveis, sem provar algum resultado incorreto. Um conjunto de axiomas é completo se, para qualquer afirmação na linguagem axiomática, ou a afirmação ou sua negação é demonstrável a partir dos axiomas. Um conjunto de axiomas é (simplesmente) consistente se não existir nenhuma afirmação tal que ambas a afirmação e sua negação são demonstráveis a partir dos axiomas. No sistema padrão da lógica de primeira ordem, um conjunto inconsistente de axiomas provará toda afirmação em sua linguagem (isso às vezes é chamado de princípio da explosão), e é, então, automaticamente completa. Um conjunto de axiomas que é tanto completo quanto consistente, contudo, prova um conjunto maximal de teoremas não-contraditórios. O teorema da incompletude de Gödel mostra que em certos casos não é possível obter uma teoria efetivamente gerada, completa e consistente.

O primeiro teorema da incompletude de Gödel apareceu primeiro em 1931 como “Teorema VI” no artigo de Gödel chamado On Formally Undecidable Propositions in Principia Mathematica and Related Systems I.

O teorema formal é escrito em linguagem bastante técnica. Pode ser parafraseado em português como:

“Qualquer teoria efetivamente gerada capaz de expressar a aritmética elementar não pode ser tanto consistente quanto completa. Em particular, para qualquer teoria formal consistente e efetivamente gerada que prova certa verdade da aritmética básica, existe uma afirmação aritmética que é verdade, mas não demonstrável na teoria (Kleene 1967, p 250).”

A verdadeira mas indemonstrável afirmação referida pelo teorema é, às vezes, referida como “sentença de Gödel” para a teoria. A prova constrói uma sentença específica de Gödel para cada teoria efetivamente gerada, porém há infinitas afirmações na linguagem da teoria que compartilha a propriedade de ser verdade mas indemonstrável. Por exemplo, a conjunção entre uma sentença de Gödel e qualquer sentença logicamente válida terá essa propriedade.

Para cada teoria formal consistente T que possui uma pequena quantidade necessária da teoria dos números, a sentença de Gödel G correspondente afirma: “G não pode ser provada dentro da teoria T”. Essa interpretação de G nos leva à seguinte análise informal: se G fosse demonstrável sob os axiomas e regras de inferência de T, então T teria um teorema, G, que efetivamente se contradiz, e então a teoria T seria inconsistente. Isto significa que se a teoria T é consistente, então G não pode ser provada dentro dela, e assim a teoria T é incompleta. Além disso, a alegação que G faz sobre sua própria indemonstrabilidade é correta. Nesse sentido, G não é somente indemonstrável como também é verdadeira, e a “demonstrabilidade dentro da teoria T” não é o mesmo que verdade. Essa análise informal pode ser formalizada para fazer uma prova rigorosa do teorema da incompletude. A prova formal revela exatamente a hipótese necessária para a hipótese T para que a natureza contraditória de G nos leve a uma genuína contradição.

Cada teoria efetivamente gerada tem sua própria sentença de Gödel. É possível definir uma teoria T’ maior que contém T inteira mais G como um axioma adicional. Isto não resultará numa teoria completa, porque o teorema de Gödel também se aplicará a T’, e assim T’ não pode ser completa. Nesse caso, G é um teorema em T’, porque é um axioma. Como G somente afirma que não é provável em T, nenhuma contradição é apresentada por sua indemonstrabilidade em T’. No entanto, como o teorema da incompletude se aplica a T’, existirá uma nova afirmação de Gödel, G’, para T’, mostrando que T’ também é incompleta. G’ se diferenciará de G, pois se referirá a T’ e não, a T.

Para provar o primeiro teorema da incompletude, Gödel representou as afirmações por números. Então a teoria em mãos, que se supõe provar certos fatos sobre números, também prova fatos sobre suas próprias afirmações, visto que é efetivamente gerada. Questões sobre a indemonstrabilidade das afirmações são representadas como questões sobre as propriedades de números, que poderiam ser decidiveis pela teoria se ela fosse completa. Nesses termos, a sentença de Gödel afirma que nenhum número natural existe com certa propriedade. Um número com essa propriedade codificaria uma prova da inconsistência da teoria. Se existisse tal número, então a teoria seria inconsistente, ao contrário da hipótese da consistência. Então, assumindo que a teoria é consistente, não existe esse número.

O primeiro teorema da incompletude mostra que qualquer sistema formal consistente, que inclui o suficiente da teoria dos números naturais, é incompleto: existem afirmações verdadeiras expressáveis em sua linguagem que são indemonstráveis dentro do sistema. Então, nenhum sistema formal (satisfazendo as hipóteses dos teoremas), que visa a caracterizar os números naturais, pode realmente fazer isso, pois existirão afirmações verdadeiras que o sistema não pode provar. Esse fato é, algumas vezes, pensado como tendo severas consequências para o programa de logicismo proposto por Gottlob Frege e Bertrand Russell, que visa a definir os números naturais em termos da lógica (Hellman 1981, p. 451-468). Bob Hale e Crispin Wright discutem que não é um problema para a lógica, porque os teoremas da incompletude se aplicam igualmente à lógica de primeira ordem assim como faz para a aritmética. Eles discutem que apenas aqueles que acreditam que os números naturais estão para ser definidos em termos da lógica de primeira ordem têm esse problema.

A existência de um sistema formal incompleto não é, particularmente, uma surpresa. O sistema pode estar incompleto simplesmente porque nem todos os axiomas necessários foram descobertos. Por exemplo, a geometria Euclideana sem o postulado das paralelas é incompleto; não é possível provar ou deixar de provar o postulado a partir dos axiomas restantes.

O teorema de Gödel mostra que, em teorias que incluem uma pequena parte da teoria dos números, uma completa e finita lista de axiomas não pode nunca ser criada, ou sequer uma lista infinita que pode ser enumerada por um programa de computador. Cada vez que uma nova afirmação é adicionada como um axioma, há outras afirmações verdadeiras que ainda não podem ser provadas, mesmo com o novo axioma. Se axiomas forem sendo adicionados, isso tornará o sistema completo, com o custo de tornar o sistema inconsistente.

Existem listas completas e consistentes de axiomas para a aritmética que não podem ser enumeradas por programas de computador. Por exemplo, alguém pode considerar todas as afirmações verdadeiras sobre os números naturais como axiomas (e nenhuma afirmação falsa), o que dá na teoria conhecida por “aritmética verdadeira”. A dificuldade é que não existe uma forma mecânica de decidir, dado uma afirmação sobre os números naturais, se é um axioma da teoria, e assim não há uma forma efetiva de verificar uma prova formal dessa teoria.

Muitos pesquisadores da lógica acreditam que os teoremas da incompletude de Gödel golpeou fortemente o segundo problema de David Hilbert, que pediu por uma prova consistente e finita para a matemática. O segundo teorema da incompletude, em particular, é geralmente visto como se tivesse tornado o problema impossível. Nem todos os matemáticos concordam com essa análise, contudo, e o status do segundo problema de Hilbert ainda não está decidido (veja “Visão moderna sobre o status do problema”).

O paradoxo do mentiroso é a sentença “Esta sentença é falsa”. Uma análise do paradoxo mostra que a sentença não pode ser verdade (porque alega ser falsa), nem é falsa (porque seria verdadeira, então). Uma sentença de Gödel G para a teoria T faz uma alegação similar à alegação do mentiroso, mas com uma demonstrabilidade trocada: G diz “G não é demonstrável na teoria T”. A análise da verdade e demonstrabilidade de G é uma versão formalizada da análise da verdade da sentença do mentiroso.

Não é possível trocar “não demonstrável” por “falso” numa sentença de Gödel, porque o predicado “Q é um número de Gödel de uma fórmula falsa” não pode ser representado como uma fórmula da aritmética. Esse resultado, conhecido como teorema de não definibilidade de Tarski, foi descoberto independentemente por Gödel (quando trabalhou na prova do teorema da incompletude) e por Alfred Tarski.

Gödel demonstrou a incompletude do Principia Mathematica, uma teoria particular da aritmética, mas uma demonstração paralela não pôde ser dada por nenhuma teoria efetiva de certa expressividade. Gödel comentou esse fato na introdução de seu artigo, mas restringiu a prova a um sistema para ser mais concreto. Em afirmações modernas do teorema, é comum afirmar condições efetivas e expressivas como hipóteses para o teorema da incompletude, então não seria limitada a nenhuma teoria formal particular. A terminologia usada para afirmar essas condições não tinha sido desenvolvida em 1931 quando Gödel publicou esses resultados.

A afirmação e a prova original de Gödel do teorema da incompletude requerem que tomemos por hipótese que a teoria não é somente consistente, mas ω-consistente. A teoria é ω-consistente se não for ω-inconsistente, e é ω-inconsistente se houver um predicado P tal que para todo número natural n a teoria prova ~P(n), e ainda a teoria prova que existe um número n com a propriedade P tal que P(n). Isto é, a teoria diz que um número com a propriedade P existe enquanto nega que ele tem um valor específico. A ω-consistência de uma teoria implica sua consistência, mas consistência não implica ω-consistência. J. Barkley Rosser (1936) fortaleceu o teorema da incompletude ao encontrar uma variação da prova (truque de Rosser) que requer que a teoria seja apenas consistente ao invés de ω-consistente. Isso é de interesse técnico, visto que todas as verdadeiras teorias formais da aritmética (teorias cujos axiomas são todos afirmações verdadeiras sobre os números naturais) são ω-consistentes, e assim o teorema de Gödel, como alegado originalmente, implica neles. A versão forte do teorema da incompletude, que apenas assume consistência ao invés de ω-consistência, é agora comumente conhecida como o teorema da incompletude de Gödel e como o teorema de Gödel-Rosser.

O segundo teorema da incompletude de Gödel apareceu primeiro em 1931 como “Teorema XI” no artigo de Gödel chamado On Formally Undecidable Propositions in Principia Mathematica and Related Systems I.

Como com o primeiro teorema, Gödel escreveu em linguagem matemática muito técnica, podendo ser parafraseada:

“Para qualquer teoria formal efetivamente gerada T, que inclua verdades da aritmética básica e também certas verdades de demonstrabilidades formais, se T inclui afirmações de sua própria consistência, então é inconsistente.”

Isso fortalece o primeiro teorema da incompletude, porque a afirmação construída nele não expressa diretamente a consistência da teoria. A prova do segundo teorema é obtida pela formalização da prova do primeiro teorema da incompletude dentro da própria teoria.

Uma sutileza técnica do segundo teorema da incompletude é como expressar a consistência de T como uma fórmula na linguagem de T. Há muitas formas de fazer isso, e nem todas elas levam ao mesmo resultado. Em particular, diferentes formalizações da alegação de que T é consistente pode não ser equivalente a T, e algumas podem até ser provadas. Por exemplo, a aritmética de primeira ordem de Peano (PA) pode provar que o maior subconjunto de PA é consistente. Mas como PA é consistente, o maior subconjunto consistente de PA é PA, então, nesse sentido, PA “prova que é consistente”. O que PA não prova é que o maior subconjunto consistente de PA é, de fato, todo o PA. (O termo “maior subconjunto consistente de PA” é tecnicamente ambíguo, mas o que quer dizer é que o maior segmento inicial e consistente dos axiomas de PA, ordenados seguindo um critério específico; i.e., por “números de Gödel”, os números codificados pelo axioma como usados por Gödel, mencionado acima).

Para a aritmética de Peano, ou qualquer teoria axiomática familiar T, é possível definir canonicamente a fórmula Con(T) expressando a consistência de T; essa fórmula expressa a propriedade de que “não há um número natural codificando a sequência de fórmulas tal que cada fórmula é ou uma axioma de T, ou um axioma lógico ou uma consequência imediata das fórmulas anteriores de acordo com as regras de inferência da lógica de primeira ordem, e tal que a última fórmula seja uma contradição”.

A formalização de Con(T) depende de dois fatores: formalizar a noção de a sentença ser derivável de um conjunto de sentenças e formalizar a noção de uma axioma de T. A formalização de derivabilidade pode ser feita de modo canônico: dada uma fórmula aritmética A(x) definindo um conjunto de axiomas, pode ser formado um predicado Prov_A(P) que expressa que P é demonstrável a partir do conjunto de axiomas definido por A(x).

Além disso, a prova padrão do segundo teorema da incompletude assume que Prov_A(P) satisfaz a condição de demonstrabilidade de Hilbert-Bernays. Fazendo #(P) representar o número de Gödel da fórmula P, a condição de derivabilidade diz:

1. Se T prova P, então T prova Prov_A(#(P)).
2. T prova 1.; isto é, T prova que se T prova P, então T prova Prov_A(#(P)). Em outras palavras, T prova que Prov_A(#(P)) implica Prov_A(#(Prov_A(#(P)))).
3. T prova que se T prova que (P → Q) e T prova P então T prova Q. Em outras palavras, T prova que Prov_A(#(P → Q)) e Prov_A(#(P)) implica Prov_A(#(Q)).

O segundo teorema da incompletude de Gödel também implica que a teoria T₁, satisfazendo a condição técnica mostrada acima, não pode provar a consistência de qualquer teoria T₂ a qual prova a consistência de T₁. Isso acontece porque a teoria T₁ pode provar que se T₂ prova a consistência de T₁, então T₁ é, de fato, consistente. Pois a alegação de que T₁ é consistente tem a forma “para todo número n, n tem a propriedade de decidibilidade de não ser codificada para a prova de contradição em T₁”. Se T₁ for de fato inconsistente, então T₂ provaria para algum n que n é o código de uma contradição em T₁. Mas se T₂ também provasse que T₁ é consistente (isto é, que não há tal n), então ele próprio seria inconsistente. Este pensamento pode ser formalizado em T₁ para mostrar que se T₂ é consistente, então T₁ também o é. Visto que, pelo segundo teorema da incompletude, T₁ não prova sua consistência, também não prova a consistência de T₂.

Este corolário do segundo teorema da incompletude mostra que não há esperança de se provar, por exemplo, a consistência da aritmética de Peano usando meios finitos que podem ser formalizados em uma teoria de consistência que é demonstrável na aritmética de Peano. Por exemplo, a teoria da aritmética primitiva recursiva (PRA), a qual é amplamente aceita como uma formalização precisa da matemática finita, é demonstravelmente consistente em PA. Assim PRA não pode provar a consistência de PA. Esse fato é geralmente visto como uma implicação do programa de Hilbert, que visava a justificar o uso dos princípios matemáticos (infinitistas) “ideais” nas provas de afirmações matemáticas (finitistas) “reais”, dando uma prova finita de que o princípio ideal é consistente, que não pode ser executada.

O corolário também indica a relevância epistemológica do segundo teorema. Ele poderia, na verdade, fornecer nenhuma informação interessante se a teoria T provasse sua consistência. Isto acontece porque teorias inconsistentes provam tudo, incluindo sua consistência. Assim, a prova de consistência de T em T não poderia nos dar nenhuma pista de que T é realmente consistente; não há dúvida de que a consistência de T poderia ser resolvida por tal prova de consistência. O interesse nas provas de consistência está na possibilidade de provar a consistência da teoria T em alguma teoria T’ que é, de alguma forma, menos duvidosa que a própria T, por exemplo, mais fraca que T. Para muitas teorias naturais T e T’ recorrentes, tal que T = teoria do conjunto de Zermelo-Fraenkel e T’ = aritmética primitiva recursiva, a consistência de T’ é provável em T, e, assim, T’ não pode provar a consistência de T pelo corolário acima do segundo teorema da incompletude.

O segundo teorema não desconsidera as provas de consistência completamente, apenas prova que podem ser formalizadas na teoria que é provada consistente. Por exemplo, Gerhard Gentzen provou a consistência da aritmética de Peano (PA) em uma teoria diferente que inclui um axioma alegando que o ordinal chamado ε₀ é bem-fundado; veja a prova de consistência de Gentzen. O teorema de Gentzen incitou o desenvolvimento da análise ordinal em teoria da prova.

Existem dois sentidos distintos da palavra “indecidível” na matemática e na ciência da computação. O primeiro é o sentido da teoria da prova relacionada aos teoremas de Gödel, sobre uma sentença não ser demonstrável nem refutável em um sistema dedutivo específico. O segundo, que não será discutido aqui, é em relação à teoria de computabilidade e se aplica não a afirmações, mas a problemas de decisão, os quais são conjuntos de questões infinitos que requer uma resposta “sim” ou “não”. Tal problema é dito ser indecidível se não houver uma função computável que responde corretamente todas as questões do conjunto (veja problema indecidível).

Por causa desses dois sentidos da palavra, o termo independente é, às vezes, usado no lugar de indecidível para o sentido de “nem demonstrável nem refutável”. O uso de “independente” também é ambíguo, contudo. Este sentido pode ser usado como “não demonstrável”, deixando aberto se uma afirmação independente deve ser refutada.

A indecidibilidade de uma afirmação em um sistema particular não remete a questão de o valor verdade da afirmação ser bem definido ou que ele pode ser determinado de outras formas. Indecidibilidade apenas implica que um sistema dedutivo particular, a ser considerado, não prova a validade ou falsidade da afirmação. Se existem afirmações “absolutamente indecidíveis”, cujo valor verdade nunca pode ser sabido ou é pouco específico, é um ponto controverso na filosofia da matemática.

O trabalho conjunto de Gödel e Paul Cohen nos deu dois exemplos concretos de afirmações indecidíveis (no primeiro sentido do termo): a hipótese do continuum não pode ser provada nem refutada no conjunto de Zermelo-Fraenkel – ZFC (a axiomização padrão da teoria dos conjuntos), e o axioma da escolha não pode ser refutado nem provado na ZF (que são todos os axiomas do ZFC exceto o axioma da escolha. Esses resultados não requerem o teorema da incompletude. Gödel provou em 1940 que nenhuma dassas afirmações podem ser refutadas nas teorias dos conjuntos ZF ou ZFC. Na década de 1960, Cohen provou que nenhuma afirmação pode ser provada a partir do ZF, e a hipótese do continuum não pode ser provada a partir do ZFC.

Em 1973, o problema de Whitehead na teoria dos grupos foi mostrado como indecidível, no primeiro sentido da palavra, na teoria padrão dos conjuntos.

Gregory Chaitin produziu afirmações indecidíveis na teoria algorítmica da informação e provou outro teorema da incompletude nesse cenário. O teorema da incompletude de Chaitin afirma que para qualquer teoria que pode representar a aritmética suficientemente, existe um limite superior c tal que nenhum número específico pode ser provado, nessa teoria, ter a complexidade Kolmogorov maior que c. Enquanto o teorema de Gödel está relacionado ao paradoxo do mentiroso, o de Chaitin está relacionado ao paradoxo de Berry.

Estas são equivalentes matemáticos naturais da sentença de Gödel: “verdade, mas indecidível”. Elas podem ser provadas em sistemas maiores que são, geralmente, aceitos como formas válidas de raciocínio, mas são indecidíveis em um sistema mais limitado como a aritmética de Peano.

Em 1977, Paris e Harrington provaram que o princípio Paris-Harrington, uma versão do teorema de Ramsey, é indecidível na axiomatização de primeira ordem da aritmética chamada de aritmética de Peano, mas pode ser provada no sistema maior da aritmética de segunda ordem. Kirby e Paris depois mostraram que o teorema de Goodstein, uma afirmação sobre sequências de números naturais mais simples que o princípio de Paris-Harrington, era decidível na aritmética de Peano.

O teorema da árvore de Kruskal, que tem aplicações na ciência da computação, também é indecidível a partir da aritmética de Peano, mas demonstrável na teoria dos conjuntos. Na realidade, o teorema da árvore de Kruskal (ou sua forma finita) é indecidível em um sistema mais forte que codifica os princípios aceitáveis, baseados numa filosofia da matemática chamada de predicativismo. O teorema relacionado, porém mais geral, do menor grafo (2003) tem consequências para a teoria da complexidade computacional.

As conclusões dos teoremas de Gödel só são provadas para as teorias formais que satisfazem as hipóteses necessárias. Nem todos os sistemas axiomáticos satisfazem essas hipóteses, mesmo quando esses sistemas têm modelos que incluem os números naturais como um subconjunto. Por exemplo, existem axiomatizações de primeira ordem da geometria de Euclides, de corpo real fechado, e da aritmética na qual a multiplicação não é demonstravelmente total; nenhum desses atende às hipóteses dos teoremas de Gödel. O ponto chave é que essas axiomatizações não são expressivas o suficiente para definir o conjunto dos números naturais ou para desenvolver propriedades para eles. Em relação ao terceiro exemplo, Dan Willard (2001) estudou muitos sistemas fracos da aritmética que não satisfazem as hipóteses do segundo teorema da incompletude, e que são consistentes e capazes de provar sua própria consistência (veja teorias auto-verificáveis).

Os teoremas de Gödel apenas se aplicam a teorias efetivamente geradas (que são recursivamente enumeráveis). Se todas as afirmações verdadeiras sobre os números naturais forem tomados como axiomas para uma teoria, então esta teoria é consistente, uma extensão completa da aritmética de Peano (chamada de aritmética verdadeira) para o qual nenhum dos teoremas de Gödel se aplica significativamente, porque essa teoria não é recursivamente enumerável.

O segundo teorema da incompletude apenas mostra que a consistência de certas teorias não pode ser provada a partir de axiomas dessas próprias teorias. Ele não mostra que a consistência não pode ser provada a partir de outros axiomas (consistentes). Por exemplo, a consistência da aritmética de Peano pode ser provada na teoria dos conjuntos de Zermelo-Fraenkel (ZFC), ou nas teorias aritméticas aumentadas com indução transfinita, como na prova de consistência de Gentzen.

• Teorema da completude de Gödel
• Teorema de Löb
• Trilema de Münchhausen
• Modelo de aritmética não-padrão
• Argumento do terceiro homem

Referências

• 1931, Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme, I. Monatshefte für Mathematik und Physik 38: 173-98.
• 1931, Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme, I. and On formally undecidable propositions of Principia Mathematica and related systems I in Solomon Feferman, ed., 1986. Kurt Gödel Collected works, Vol. I. Oxford University Press: 144-195. The original German with a facing English translation, preceded by a very illuminating introductory note by Kleene.
  • Hirzel, Martin, 2000, On formally undecidable propositions of Principia Mathematica and related systems I.. A modern translation by Hirzel.
• 1951, Some basic theorems on the foundations of mathematics and their implications in Solomon Feferman, ed., 1995. Kurt Gödel Collected works, Vol. III. Oxford University Press: 304-23.

• George Boolos, 1989, "A New Proof of the Gödel Incompleteness Theorem", Notices of the American Mathematical Society v. 36, pp. 388–390 and p. 676, reprinted in Boolos, 1998, Logic, Logic, and Logic, Harvard Univ. Press. ISBN 0-674-53766-1
• Arthur Charlesworth, 1980, "A Proof of Godel's Theorem in Terms of Computer Programs," Mathematics Magazine, v. 54 n. 3, pp. 109–121. JStor
• Martin Davis, "The Incompleteness Theorem", in Notices of the AMS vol. 53 no. 4 (April 2006), p. 414.
• Jean van Heijenoort, 1963. "Gödel's Theorem" in Edwards, Paul, ed., Encyclopedia of Philosophy, Vol. 3. Macmillan: 348-57.
• Geoffrey Hellman, How to Gödel a Frege-Russell: Gödel's Incompleteness Theorems and Logicism. Noûs, Vol. 15, No. 4, Special Issue on Philosophy of Mathematics. (Nov., 1981), pp. 451–468.
• David Hilbert, 1900, "Mathematical Problems." English translation of a lecture delivered before the International Congress of Mathematicians at Paris, containing Hilbert's statement of his Second Problem.
• Kikuchi, Makoto; Tanaka, Kazuyuki (1994), «On formalization of model-theoretic proofs of Gödel's theorems», Notre Dame Journal of Formal Logic, ISSN 0029-4527, 35 (3): 403–412, MR 1326122, doi:10.1305/ndjfl/1040511346 
• Stephen Cole Kleene, 1943, "Recursive predicates and quantifiers," reprinted from Transactions of the American Mathematical Society, v. 53 n. 1, pp. 41–73 in Martin Davis 1965, The Undecidable (loc. cit.) pp. 255–287.
• John Barkley Rosser, 1936, "Extensions of some theorems of Gödel and Church," reprinted from the Journal of Symbolic Logic vol. 1 (1936) pp. 87–91, in Martin Davis 1965, The Undecidable (loc. cit.) pp. 230–235.
• John Barkley Rosser, 1939, "An Informal Exposition of proofs of Gödel's Theorem and Church's Theorem", Reprinted from the Journal of Symbolic Logic, vol. 4 (1939) pp. 53–60, in Martin Davis 1965, The Undecidable (loc. cit.) pp. 223–230
• C. Smoryński, "The incompleteness theorems", in J. Barwise, ed., Handbook of Mathematical Logic, North-Holland 1982 ISBN 978-0-444-86388-1, pp. 821–866.
• Dan E. Willard (2001), "Self-Verifying Axiom Systems, the Incompleteness Theorem and Related Reflection Principles", Journal of Symbolic Logic, v. 66 n. 2, pp. 536–596. doi:10.2307/2695030
• Zach, Richard (2003), «The Practice of Finitism: Epsilon Calculus and Consistency Proofs in Hilbert's Program» (PDF), Berlin, New York: Springer-Verlag, Synthese, ISSN 0039-7857, 137 (1): 211–259, doi:10.1023/A:1026247421383 
• Richard Zach, 2005, "Paper on the incompleteness theorems" in Grattan-Guinness, I., ed., Landmark Writings in Western Mathematics. Elsevier: 917-25.

• Francesco Berto. There's Something about Gödel: The Complete Guide to the Incompleteness Theorem John Wiley and Sons. 2010.
• Domeisen, Norbert, 1990. Logik der Antinomien. Bern: Peter Lang. 142 S. 1990. ISBN 3-261-04214-1. Zentralblatt MATH
• Torkel Franzén, 2005. Gödel's Theorem: An Incomplete Guide to its Use and Abuse. A.K. Peters. ISBN 1-56881-238-8 MR2007d:03001
• Douglas Hofstadter, 1979. Gödel, Escher, Bach: An Eternal Golden Braid. Vintage Books. ISBN 0-465-02685-0. 1999 reprint: ISBN 0-465-02656-7. MR80j:03009
• Douglas Hofstadter, 2007. I Am a Strange Loop. Basic Books. ISBN 978-0-465-03078-1. ISBN 0-465-03078-5. MR2008g:00004
• Stanley Jaki, OSB, 2005. The drama of the quantities. Real View Books.
• Per Lindström, 1997, Aspects of Incompleteness, Lecture Notes in Logic v. 10.
• J.R. Lucas, FBA, 1970. The Freedom of the Will. Clarendon Press, Oxford, 1970.
• Ernest Nagel, James Roy Newman, Douglas Hofstadter, 2002 (1958). Gödel's Proof, revised ed. ISBN 0-8147-5816-9. MR2002i:03001
• Rudy Rucker, 1995 (1982). Infinity and the Mind: The Science and Philosophy of the Infinite. Princeton Univ. Press. MR84d:03012
• Smith, Peter, 2007. An Introduction to Gödel's Theorems. Cambridge University Press. MathSciNet
• N. Shankar, 1994. Metamathematics, Machines and Gödel's Proof, Volume 38 of Cambridge tracts in theoretical computer science. ISBN 0-521-58533-3
• Raymond Smullyan, 1991. Godel's Incompleteness Theorems. Oxford Univ. Press.
• —, 1994. Diagonalization and Self-Reference. Oxford Univ. Press. MR96c:03001
• Hao Wang, 1997. A Logical Journey: From Gödel to Philosophy. MIT Press. ISBN 0-262-23189-1 MR97m:01090

• Francesco Berto. "The Gödel Paradox and Wittgenstein's Reasons" Philosophia Mathematica (III) 17. 2009.
• John W. Dawson, Jr., 1997. Logical Dilemmas: The Life and Work of Kurt Gödel, A.K. Peters, Wellesley Mass, ISBN 1-56881-256-6.
• Goldstein, Rebecca, 2005, Incompleteness: the Proof and Paradox of Kurt Gödel, W. W. Norton & Company. ISBN 0-393-05169-2
• Juliet Floyd and Hilary Putnam, 2000, "A Note on Wittgenstein's 'Notorious Paragraph' About the Gödel Theorem", Journal of Philosophy v. 97 n. 11, pp. 624–632.
• Carl Hewitt, 2008, "Large-scale Organizational Computing requires Unstratified Reflection and Strong Paraconsistency", Coordination, Organizations, Institutions, and Norms in Agent Systems III, Springer-Verlag.
• David Hilbert and Paul Bernays, Grundlagen der Mathematik, Springer-Verlag.
• John Hopcroft and Jeffrey Ullman 1979, Introduction to Automata theory, Addison-Wesley, ISBN 0-201-02988-X
• James P. Jones, Undecidable Diophantine Equations, Bulletin of the American Mathematical Society v. 3 n. 2, 1980, pp. 859–862.
• Stephen Cole Kleene, 1967, Mathematical Logic. Reprinted by Dover, 2002. ISBN 0-486-42533-9
• Russell O'Connor, 2005, "Essential Incompleteness of Arithmetic Verified by Coq", Lecture Notes in Computer Science v. 3603, pp. 245–260.
• Graham Priest, 2006, In Contradiction: A Study of the Transconsistent, Oxford University Press, ISBN 0-19-926329-9
• Graham Priest, 2004, Wittgenstein's Remarks on Gödel's Theorem in Max Kölbel, ed., Wittgenstein's lasting significance, Psychology Press, pp. 207–227.
• Graham Priest, 1984, "Logic of Paradox Revisited", Journal of Philosophical Logic, v. 13,` n. 2, pp. 153–179
• Hilary Putnam, 1960, Minds and Machines in Sidney Hook, ed., Dimensions of Mind: A Symposium. New York University Press. Reprinted in Anderson, A. R., ed., 1964. Minds and Machines. Prentice-Hall: 77.
• Rautenberg, Wolfgang (2010), A Concise Introduction to Mathematical Logic, ISBN 978-1-4419-1220-6 3rd ed. , New York: Springer Science+Business Media, doi:10.1007/978-1-4419-1221-3 .
• Victor Rodych, 2003, "Misunderstanding Gödel: New Arguments about Wittgenstein and New Remarks by Wittgenstein", Dialectica v. 57 n. 3, pp. 279–313. doi:10.1111/j.1746-8361.2003.tb00272.x
• Stewart Shapiro, 2002, "Incompleteness and Inconsistency", Mind, v. 111, pp 817–32. doi:10.1093/mind/111.444.817
• Alan Sokal and Jean Bricmont, 1999, Fashionable Nonsense: Postmodern Intellectuals' Abuse of Science, Picador. ISBN 0-312-20407-8
• Joseph R. Shoenfield (1967), Mathematical Logic. Reprinted by A.K. Peters for the Association of Symbolic Logic, 2001. ISBN 978-1-56881-135-2
• Jeremy Stangroom and Ophelia Benson, Why Truth Matters, Continuum. ISBN 0-8264-9528-1
• George Tourlakis, Lectures in Logic and Set Theory, Volume 1, Mathematical Logic, Cambridge University Press, 2003. ISBN 978-0-521-75373-9
• Wigderson, Avi (2010), «The Gödel Phenomena in Mathematics: A Modern View» (PDF), Kurt Gödel and the Foundations of Mathematics: Horizons of Truth, Cambridge University Press 
• Hao Wang, 1996, A Logical Journey: From Gödel to Philosophy, The MIT Press, Cambridge MA, ISBN 0-262-23189-1.
• Richard Zach, 2006, "Hilbert's program then and now", in Philosophy of Logic, Dale Jacquette (ed.), Handbook of the Philosophy of Science, v. 5., Elsevier, pp. 411–447.

• Stanford Encyclopedia of Philosophy: "Kurt Gödel" — by Juliette Kennedy.
• MacTutor biographies:
  • Kurt Gödel.
  • Gerhard Gentzen.
  • What is Mathematics:Gödel's Theorem and Around by Karlis Podnieks. An online free book.
• World's shortest explanation of Gödel's theorem using a printing machine as an example.
• October 2011 RadioLab episode about/including Gödel's Incompleteness theorem
• Hazewinkel, Michiel, ed. (2001), «Gödel incompleteness theorem», Enciclopédia de Matemática, ISBN 978-1-55608-010-4 (em inglês), Springer