|
|
In mathematical logic, Gödel's incompleteness theorems are two celebrated theorems proved by Kurt Gödel in 1931.
| Contents |
First incompleteness theorem
Gödel's first incompleteness theorem is perhaps the most celebrated result in mathematical logic. It basicly says that
- For any formal theory in which basic arithmetical facts are provable, it's possible to construct an arithmetical statement which, if the theory is consistent, is true but not provable or refutable in the theory
The meaning of "it's possible to construct" is that there is a mechanical procedure which when given a description of the theory e.g. in form of a computer program listing its axioms or a formula in the language of arithmetic defining the set of axioms of the theory produces a sentence in the language of arithmetic which has the stated property. That this sentence is true if the theory is consistent simply means that what it says about natural numbers is true, in a mathematically defined sense, if no contradiction can be derived in the theory. Specifically, the sentence is equivalent to the claim that there does not exist a natural number coding a proof of contradiction in the theory, and it's being true just means that there really is no such natural number. The sentence produced by the procedure is often referred to as "the" Gödel sentence for that theory.
Sometimes it's claimed that the proof of Gödel's first incompleteness theorem somehow allows humans to "see" the truth of the Gödel sentence of some theory. This is not at all correct. If we know the theory to be consistent, then it trivially follows form the incompleteness theorem that the Gödel sentence is also true. But in general we have no idea whether or not a theory is consistent or not and consequently no way of "seeing" whether the corresponding Gödel sentence is true or false.
Originally, Gödel proved a weaker statement:
- For any formal theory in which basic arithmetical facts are provable, it's possible to construct an arithmetical statement which, if the theory is omega-consistent, is true but not provable or refutable in the theory
Omega-consistency is a technical concept which applies to a theory T if T does not prove for any property P that there exists a number with a property P and simultaneously prove for every natural number n that n does not have the property P. The last clause means that for every natural number n, the theory proves the proposition not-P(n), not that the theory proves that for all n, not-P(n). Barkley Rosser later strengtened the theorem by removing the requirement for the theory to be omega-consistent. This is mostly of technical interest, since all true formal theories of arithmetic, i.e. theories the axioms of which are true statements about natural numbers, are omega-consistent and thus Gödel's original theorem applies to them.
Second theorem
We noted in the section about the first incompleteness theorem that the Gödel sentence of a theory T is equivalent to the consistency of T. If this fact itself is provable in T, it follows that the consistency of T is not provable in T. That the Gödel sentence of T is equivalent to the consistency of T is provable in T can be shown by formalizing the proof of the first incompleteness theorem in T.
There is a technical subtlety involved in the second incompleteness theorem, namely how exactly are we to express the consistency of T in the language of T. There are many ways to do this, and not all of them lead to the same result. In particular, different formalizations of the claim that T is consistent may be inequivalent in T, and some may even be provable. For example, first order arithmetic (Peano arithmetic or PA for short) can prove that the largest consistent subset of PA is consistent. But since PA is consistent, the largest consistent subset of PA is just PA, so in this sense PA "proves that it's consistent". What PA does not prove is that the largest consistent subset of PA is, in fact, the whole of PA.
In case of Peano arithmetic or any familiar explicitly axiomatized theory T, it's rather trivial to express the consistency of the T as an arithmetical formula Con(T), since Con(T) can be expressed canonically as "there does not exist an integer coding a sequence of sentences, such that each sentence is either one of the (canonical) axioms of T, or follows from preceding sentences by rules of inference of first order logic which ends in a contradiction". But for arbitrary T there is no canonical choice for Con(T).
The formalization of Con(T) depends on two factors: formalizing the notion of a sentence being derivable from a set of sentences and formalizing the notion of being an axiom of T. Formalizing derivability can be done in canonical fashion, so given an arithmetical formula A(x) defining a set of axioms we can canonically form the predicate Prov_A(P) which expresses that P is provable from the set of axioms defined by A(x). Using this predicate we can express, given a formula A(x) defining some set of axioms for T, Con(T) as "not Prov_A('P&~P')". Solomon Feferman showed that Gödel's second incompleteness theorem goes trough when the formula A(x) is chosen so that it has the form "there exists a number n satisfying the decidable predicate P" for some P. In addition, the provability predicate must satisfy so called Hilbert-Bernays provability conditions:
1. If T proves P, then T proves Prov_A(P)
2. T proves that 1., i.e. T proves that if T proves P, then T proves Prov_A(P)
3. T proves that if T proves that (P implies Q) then T proves that provability of P implies provability of Q
Gödel's second incompleteness theorem also implies that a theory T_1 satisfying the technical conditions outlined above can't prove the consistency of any theory T_2 which proves the consistency of T_1. This is because the T_1 can prove that if T_2 proves the consistency of T_1, then T_1 is in fact consistent. For the claim that T_1 is consistent has form "for all numbers n, n has the decidable property of not being a code for a proof of contradiction in T_1". If T_1 were in fact inconsistent, then T_2 would prove for some n that n is the code of a contradiction in T_1. But if T_2 also proved that T_1 is consistent, i.e. there is no such n, it would itself be inconsistent. We can carry out this reasoning in T_1 and conclude that if T_2 is consistent, then T_1 is consistent. Since by second incompleteness theorem, T_1 does not prove its consistency, it can't prove the consistency of T_2 either.
This easy corollary of the second incompleteness theorem shows that there is no hope of proving e.g. the consistency of first order arithmetic using finitistic means provided we accept that finitistic means are correctly formalized in a theory the consistency of which is provable in PA. It's generally accepted that the theory of primitive recursive arithmetic (PRA) is an accurate formalization of finitistic mathematics, and PRA is provably consistent in PA. Thus PRA can't prove the consistency of PA. This is generally seen to show that Hilbert's program of validating the use of "ideal" mathematical principles to prove "real" (finitistic) mathematical statements by showing that the "ideal" principles are consistent by finitistically acceptable principles can't be carried out.
Gentzen's theorem
In 1936 Gerhard Gentzen proved the consistency of first order arithmetic. In itself, the result is rather trivial, since the consistency of first order arithmetic has a very easy proof: the axioms are true - in a mathematically defined sense -, the rules of predicate calculus preserve truth and no contradiction is true, hence no contradiction follows form the axioms of first order arithmetic. What makes Gentzen proof interesting is that it shows much more than merely that first order arithmetic is consistent. Gentzen showed that the consistency of first order arithmetic is provable, over the very weak base theory of primitive recursive arithmetic mentioned earlier, using the principle of quantifier free transfinite induction up to the ordinal epsilon-0.
The principle of quantifier free transfinite induction up to epsilon-0 says that for any formula A(x) with no bound variables transfinite induction up to epsilon-0 holds. Epsilon-0 is the first ordinal alpha, such that alpha^omega = alpha, i.e. the limit of the sequence omega, omega^omega, omega^omega^omega,... To express ordinals in the language of arithmetic a notation is needed, i.e. a way to assign natural numbers to ordinals less than epsilon-0. This can be done in various ways, one example provided by Cantor's normal form theorem. That transfinite induction holds for a formula A(x) means that A does not define a infinite descending sequence of ordinals smaller than epsilon-0 (in which case epsilon-0 would not be well-ordered). Gentzen assigned ordinals smaller than epsilon-0 to proofs in first order arithmetic and showed that if there is a proof of contradiction, then there is an infinite descending sequence of ordinals < epsilon-0 produced by a primitive recursive operation on proofs corresponding to a quantifier free formula.
Gentzen's proof also highlights one commonly missed aspect of Gödel's second incompleteness theorem. It's sometimes claimed that the consistency of a theory can only be proved in a stronger theory. The theory obtained by adding quantifier free transfinite induction to primitive recursive arithmetic proves the consistency of first order arithmetic but is not stronger than first order arithmetic. For example, it doesn't prove ordinary mathematical induction for all formulae, while first order arithmetic does (it has this as an axiom schema). The resulting theory is not weaker than first order arithmetic either, since it can prove a number theoretical fact - the consistency of first order arithmetic - that first order arithmetic can't. The two theories are simply incomparable.
Gentzen's proof is the first example of what is called proof theoretical ordinal analysis. In ordinal analysis one gauges the strenght of theories by measuring how large ordinals they can prove to be well-ordered, or equivalently for how large ordinals is transfinite induction provable.
Meaning of Gödel's theorems
Gödel's theorems are theorems in first-order logic, and must ultimately be understood in that context. In formal logic, both mathematical statements and proofs are written in a symbolic language, one where we can mechanically check the validity of proofs so that there can be no doubt that a theorem follows from our starting list of axioms. In theory, such a proof can be checked by a computer, and in fact there are computer programs that will check the validity of proofs (automatic proof verification is closely related to automated reasoning (though proving and checking the proof are usually different tasks)).
To be able to perform this process, we need to know what our axioms are. We could start with a finite set of axioms, such as in Euclidean geometry, or more generally we could allow an infinite list of axioms, with the requirement that we can mechanically check for any given statement if it is an axiom from that set or not (an axiom schema). In computer science, this is known as having a recursive set of axioms. While an infinite list of axioms may sound strange, this is exactly what's used in the usual axioms for the natural numbers, the Peano axioms: the inductive axiom is in fact an axiom schema - it states that if zero has any property and the successor of any natural number has that property, all natural numbers have that property - it does not specify which property and the only way to say in first-order logic that this is true of all properties is to have an infinite number of statements.
Gödel's first incompleteness theorem shows that any such system that allows you to define the natural numbers is necessarily incomplete: it contains statements that are neither provably true nor provably false.
The existence of an incomplete system is in itself not particularly surprising. For example, if you take Euclidean geometry and you drop the parallel postulate, you get an incomplete system (in the sense that system does not contain all the true statements). An incomplete system can mean simply that you haven't discovered all the necessary axioms.
What Gödel showed is that in most cases, such as in number theory or real analysis, you can never discover the complete list of axioms. Each time you add a statement as an axiom, there will always be another statement out of reach.
You can add an infinite number of axioms; for example, you can add all true statements about the natural numbers to your list of axioms, but such a list will not be a recursive set. Given a random statement, there will be no way to know if it is an axiom of your system. If I give you a proof, in general there will be no way for you to check if that proof is valid.
Gödel's theorem has another interpretation in the language of computer science. In first-order logic, theorems are recursively enumerable: you can write a computer program that will eventually generate any valid proof. You can ask if they satisfy the stronger property of being recursive: can you write a computer program to definitively determine if a statement is true or false? Gödel's theorem says that in general you cannot.
Many logicians believe that Gödel's incompleteness theorems struck a fatal blow to David Hilbert's program towards a universal mathematical formalism. The generally agreed upon stance is that the second theorem is what specifically dealt this blow. However some believe it was the first, and others believe that neither did.
Examples of undecidable statements
The existence of an undecidable statement within a formal system is not in itself a surprising phenomenon.
The subsequent combined work of Gödel and Paul Cohen has given concrete examples of undecidable statements (statements which can be neither proven nor disproven): both the axiom of choice and the continuum hypothesis are undecidable in the standard axiomatization of set theory. These results do not require the incompleteness theorem.
In 1936, Alan Turing proved that the halting problem—the question of whether or not a Turing machine halts on a given program—is undecidable. This result was later generalised in the field of recursive functions to Rice's theorem which shows that all non-trivial decision problems are undecidable in a system that is Turing-complete.
In 1973, the Whitehead problem in group theory was shown to be undecidable in standard set theory. In 1977, Kirby, Paris and Harrington proved that a statement in combinatorics, a version of the Ramsey theorem, is undecidable in the axiomatization of arithmetic given by the Peano axioms but can be proven to be true in the larger system of set theory. Kruskal's tree theorem, which has applications in computer science, is also undecidable from the Peano axioms but provable in set theory. Goodstein's theorem is a relatively simple statement about natural numbers that is undecidable in Peano arithmetic.
Gregory Chaitin produced undecidable statements in algorithmic information theory and in fact proved his own incompleteness theorem in that setting.
One of the first problems suspected to be undecidable was the word problem for groups, first posed by Max Dehn in 1911, which states that there is a finitely presented group that has no algorithm to state whether two words are equivalent. It was not proven to be undecidable until 1952.
Misconceptions about Gödel's theorems
Since Gödel's first incompleteness theorem is so famous, it has given rise to many misconceptions. They are refuted here:
- The theorem does not imply that every interesting axiom system is incomplete. For example, Euclidean geometry can be axiomatized so that it is a complete system. (In fact, Euclid's original axioms are pretty close to being a complete axiomatization. The missing axioms express properties that seem so obvious that it took the emergence of the idea of a formal proof before their absence was noticed.)
- The theorem only applies to systems that allow you to define the natural numbers as a set. It is not sufficient that the system contain the natural numbers. You must also be able to express the concept "<math>x<math> is a natural number" using your axioms and first-order logic. There are plenty of systems that contain the natural numbers and are complete. For example both the real numbers and complex numbers have complete axiomatizations.
Discussion and implications
The incompleteness results affect the philosophy of mathematics, particularly viewpoints like formalism, which uses formal logic to define its principles. One can paraphrase the first theorem as saying that "we can never find an all-encompassing axiomatic system which is able to prove all mathematical truths, but no falsehoods."
On the other hand, from a strict formalist perspective this paraphrase would be considered meaningless because it presupposes that mathematical "truth" and "falsehood" are well-defined in an absolute sense, rather than relative to each formal system.
The following rephrasing of the second theorem is even more unsettling to the foundations of mathematics:
- If an axiomatic system can be proven to be consistent from within itself, then it is inconsistent.
Therefore, in order to establish the consistency of a system S, one needs to utilize some other system T, but a proof in T is not completely convincing unless T's consistency has already been established without using S. The consistency of the Peano axioms for natural numbers for example can be proven in set theory, but not in the theory of natural numbers alone. This provides a negative answer to problem number 2 on David Hilbert's famous list of important open questions in mathematics (called Hilbert's problems).
In principle, Gödel's theorems still leave some hope: it might be possible to produce a general algorithm that for a given statement determines whether it is undecidable or not, thus allowing mathematicians to bypass the undecidable statements altogether. However, the negative answer to the Entscheidungsproblem shows that no such algorithm exists.
There are some who hold that a statement that is unprovable within a deductive system may be quite provable in a metalanguage. And what cannot be proven in that metalanguage can likely be proven in a meta-metalanguage, recursively, ad infinitum, in principle. By invoking a sort of super Theory of Types with an axiom of Reducibility -- which by an inductive assumption applies to the entire stack of languages -- one may, for all practical purposes, overcome the obstacle of incompleteness.
Note that Gödel's theorems only apply to sufficiently strong axiomatic systems.
"Sufficiently strong" means that the theory contains enough arithmetic to carry out the coding constructions needed for the proof of the first incompleteness theorem. Essentially, all that is required are some basic facts about addition and multiplication as formalized, e.g., in Robinson arithmetic Q. There are even weaker axiomatic systems that are consistent and complete, for instance Presburger arithmetic which proves every true first-order statement involving only addition.
The axiomatic system may consist of infinitely many axioms (as first-order Peano arithmetic does), but for Gödel's theorem to apply, there has to be an effective algorithm which is able to check proofs for correctness. For instance, one might take the set of all first-order sentences which are true in the standard model of the natural numbers. This system is complete; Gödel's theorem does not apply because there is no effective procedure that decides if a given sentence is an axiom. In fact, that this is so is a consequence of Gödel's first incompleteness theorem.
Another example of a specification of a theory to which Gödel's first theorem does not apply can be constructed as follows: order all possible statements about natural numbers first by length and then lexicographically, start with an axiomatic system initially equal to the Peano axioms, go through your list of statements one by one, and, if the current statement cannot be proven nor disproven from the current axiom system, add it to that system. This creates a system which is complete, consistent, and sufficiently powerful, but not recursively enumerable.
Gödel himself only proved a technically slightly weaker version of the above theorems; the first proof for the versions stated above was given by J. Barkley Rosser in 1936.
In essence, the proof of the first theorem consists of constructing a statement p within a formal axiomatic system that can be given a meta-mathematical interpretation of:
- p = "This statement cannot be proven"
As such, it can be seen as a modern variant of the Liar paradox. Unlike the Liar sentence, p does not directly refer to itself; the above interpretation can only be "seen" from outside the formal system.
If the axiomatic system is consistent, Gödel's proof shows that p (and its negation) cannot be proven in the system. Therefore p is "true" (p claims to be not provable, and it is not provable) yet it cannot be formally proved in the system. Note that adding p to the axioms of the system would not solve the problem: there would be another Gödel sentence for the enlarged theory.
Many scholars have debated over what Gödel's incompleteness theorem implies about human intelligence. Much of the debate centers on whether the human mind is equivalent to a Turing machine, or by the Church-Turing thesis, any finite machine at all. If it is, and if the machine is consistent, then Gödel's incompleteness theorems would apply to it.
One of the earliest attempts to use incompleteness to reason about human intelligence was by Gödel himself in his 1951 Gibbs lecture entitled "Some basic theorems on the foundations of mathematics and their philosophical implications." In this lecture, Gödel uses the incompleteness theorem to arrive at the following disjunction: (a) the human mind is not a consistent finite machine, or (b) there exist Diophantine equations for which it cannot decide whether solutions exist. Gödel finds (b) implausible, and thus seems to have believed the human mind was not equivalent to a finite machine, i.e., its power exceeded that of any finite machine. It is worth noting that Marvin Minsky has reported that Gödel told him personally that he believed that human beings had an intuitive, not just computational, way of arriving at truth and that therefore his theorem did not limit what can be known to be true by humans.
In 1960, Hilary Putnam published a paper entitled "Minds and Machines," in which he outlines a typical anti-mechanist argument, meaning to point out its flaws. This is the argument that the (alleged) difference between "what can be mechanically proven" and "what can be seen to be true by humans" shows that human intelligence is not mechanical in nature. Or, as Putnam puts it:
Let T be a Turing machine which "represents" me in the sense that T can prove just the mathematical statements I prove. Then using Gödel's technique I can discover a proposition that T cannot prove, and moreover I can prove this proposition. This refutes the assumption that T "represents" me, hence I am not a Turing machine.
Putnam points out that this argument ignores the issue of consistency. Gödel's technique can only be applied to consistent systems. It is possible, argues Putnam, that the human mind is inconsistent. Many other scholars have echoed this view, including Marvin Minsky, who stated that human intelligence is capable of error and of understanding statements which are in fact inconsistent or false.
JR Lucas in Minds, Machines and Gödel (1963), and later in his book The Freedom of the Will (1970), lays out an anti-mechanist viewpoint, including arguments for why the human mind can be considered consistent. Lucas allows that, by Gödel's second theorem, a human mind cannot formally prove its own consistency, and even seems to allow (perhaps facetiously) that women and politicians are inconsistent. Nevertheless, he sets out arguments for why a male non-politician can be considered consistent. These arguments are philosophical in nature and are the subject of much debate; Lucas provides references to responses on his own website (http://users.ox.ac.uk/~jrlucas/Godel/referenc.html).
Another notable work was done by Judson Webb in his 1968 paper "Metamathematics and the Philosophy of Mind." Webb claims that previous attempts have glossed over whether we truly can see that the Gödelian statement p is true. Using a different formulation of Gödel's theorems, namely, that of Raymond Smullyan and Emil Post, Webb shows one can derive convincing arguments for oneself of both the truth and falsity of p. He furthermore argues that all arguments about the philosophical implications of Gödel's theorems are really arguments about whether the Church-Turing thesis is true.
Later, Roger Penrose entered the fray, providing some novel anti-mechanist arguments in his books, The Emperor's New Mind (1989) [ENM] and Shadows of the Mind (1994) [SM]. These books have proved highly controversial. Martin Davis responded to ENM in his paper "Is Mathematical Insight Algorithmic?" (ps) (http://www.cs.nyu.edu/cs/faculty/davism/penrose.ps), where he argues that Penrose ignores the issue of consistency. Solomon Feferman gives a critical examination of SM in his paper "Penrose's Gödelian argument" (pdf) (http://math.stanford.edu/~feferman/papers/penrose.pdf).
Proof sketch for the first theorem
The main problem in fleshing out the above mentioned proof idea is the following: in order to construct a statement p that is equivalent to "p cannot be proved", p would have to somehow contain a reference to p, which could easily give rise to an infinite regress. Gödel's ingenious trick, which was later used by Alan Turing to solve the Entscheidungsproblem, will be described below.
To begin with, every formula or statement that can be formulated in our system gets a unique number, called its Gödel number. This is done in such a way that it is easy to mechanically convert back and forth between formulas and Gödel numbers. Because our system is strong enough to reason about numbers, it is now also possible to reason about formulas.
A formula F(x) that contains exactly one free variable x is called a statement form. As soon as x is replaced by a specific number, the statement form turns into a bona fide statement, and it is then either provable in the system, or not. Statement forms themselves are not statements and therefore cannot be proved or disproved. But every statement form F(x) has a Gödel number which we will denote by G(F). The choice of the free variable used in the form F(x) is not relevant to the assignment of the Gödel number G(F).
By carefully analyzing the axioms and rules of the system, one can then write down a statement form P(x) which embodies the idea that x is the Gödel number of a statement which can be proved in our system. Formally: P(x) can be proved if x is the Gödel number of a provable statement, and its negation ~P(x) can be proved if it isn't. (While this is good enough for this proof sketch, it is technically not completely accurate. See Gödel's paper for the problem and Rosser's paper for the resolution. The key word is "omega-consistency".)
Now comes the trick: a statement form F(x) is called self-unprovable if the form F, applied to its own Gödel number, is not provable. This concept can be defined formally, and we can construct a statement form SU(z) whose interpretation is that z is the Gödel number of a self-unprovable statement form. Formally, SU(z) is defined as: z = G(F) for some particular form F(x), and y is the Gödel number of the statement F(G(F)), and ~P(y). Now the desired statement p that was mentioned above can be defined as:
- p = SU(G(SU)).
Intuitively, when asking whether p is true, we ask: "Is the property of being self-unprovable itself self-unprovable?" This is very reminiscent of the Barber paradox about the barber who shaves precisely those people who don't shave themselves: does he shave himself?
We will now assume that our axiomatic system is consistent.
If p were provable, then SU(G(SU)) would be true, and by definition of SU, z = G(SU) would be the Gödel number of a self-unprovable statement form. Hence SU would be self-unprovable, which by definition of self-unprovable means that SU(G(SU)) is not provable, but this was our p: p is not provable. This contradiction shows that p cannot be provable.
If the negation of p= SU(G(SU)) were provable, then by definition of SU this would mean that z = G(SU) is not the Gödel number of a self-unprovable form, which implies that SU is not self-unprovable. By definition of self-unprovable, we conclude that SU(G(SU)) is provable, hence p is provable. Again a contradiction. This one shows that the negation of p cannot be provable either.
So the statement p can neither be proved nor disproved within our system.
Proof sketch for the second theorem
Let p stand for the undecidable sentence constructed above, and let's assume that the consistency of the system can be proven from within the system itself. We have seen above that if the system is consistent, then p is not provable. The proof of this implication can be formalized in the system itself, and therefore the statement "p is not provable", or "not P(p)" can be proven in the system.
But this last statement is equivalent to p itself (and this equivalence can be proven in the system), so p can be proven in the system. This contradiction shows that the system must be inconsistent.
See also
References
Scientific articles
- K. Gödel: Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme, I. (http://home.ddc.net/ygg/etext/godel/) Monatshefte für Mathematik und Physik, 38 (1931), pp. 173-198. Translated in van Heijenoort: From Frege to Gödel. Harvard University Press, 1971.
- K. Gödel: Some basic theorems on the foundations of mathematics and their implications (1951). Printed in Collected works / Kurt Gödel v.III; edited by Solomon Feferman. Clarendon Press ; New York : Oxford University Press, 1995. pp. 304-323.
- J.R. Lucas: Minds, Machines, and Gödel (http://users.ox.ac.uk/~jrlucas/Godel/mmg.html). Philosophy XXXVI (1961):112-127.
- Putnam, Hilary. Minds and Machines, Dimensions of Mind: A Symposium, edited by Sidney Hook. New York University Press: New York, 1960. Reprinted in Minds and Machines, edited by A.R. Anderson, Prentice-Hall: Englewood Cliffs, New Jersey, 1964. page 77.
- B. Rosser: Extensions of some theorems of Gödel and Church. Journal of Symbolic Logic, 1 (1936), N1, pp. 87-91.
- J. Webb. Metamathematics and the Philosophy of Mind. Philosophy of Science, Vol 35, Issue 2, (Jun 1968):156-178.
Books
- Hao Wang: A Logical Journey: From Gödel to Philosophy Bradford Books (January 10, 1997) ISBN 0262231891
- Kārlis Podnieks: Around Goedel's Theorem, http://www.ltn.lv/~podnieks/gt.html
- D. Hofstadter: Gödel, Escher, Bach: An Eternal Golden Braid, 1979, ISBN 0465026850. (1999 reprint: ISBN 0465026567).
- Ernest Nagel, James Roy Newman, Douglas R. Hofstadter: Gödel's Proof, revised edition (2002). ISBN 0814758169.
- Hilbert's second problem (http://aleph0.clarku.edu/~djoyce/hilbert/problems.html#prob2) (English translation)
- Norbert Domeisen, Logik der Antinomien. Bern etc.: Peter Lang. 142 S. 1990. (ISBN 3-261-04214-1), Zentralblatt MATH (http://www.emis.de/cgi-bin/zmen/ZMATH/en/quick.html?first=1&maxdocs=3&type=html&an=0724.03003&format=complete)
External web pages
- Gödel's biography with photo (http://www-groups.dcs.st-and.ac.uk/~history/Mathematicians/Godel.html)
- Gentzen's biography with photo (http://www-groups.dcs.st-and.ac.uk/~history/Mathematicians/Gentzen.html)
- Godel's Theorem explained further (http://www.miskatonic.org/godel.html)bg:Теорема на Гьодел за непълнота
de:Gödelscher Unvollständigkeitssatz es:Teorema de la incompletud de Gödel eo:Teoremoj de nekompleteco fr:Théorème d'incomplétude de Gödel io:Teorio di Godel it:Teorema di incompletezza di Gödel he:משפט אי השלמות של גדל nl:Onvolledigheidsstelling ja:ゲーデルの不完全性定理 pt:Teorema da incompletude de Gödel ru:Теорема Гёделя о неполноте sv:Gödels ofullständighetsteorem tr:Gödel'in Yetersizlik Teoremi uk:Геделя теорема про неповноту zh:哥德尔不完备定理