Gödel's incompleteness theorems are two celebrated theorems in mathematical logic proven by Kurt Gödel in 1930. Somewhat simplified, the first theorem states that in any axiomatic system sufficiently complex to allow one to do basic arithmetic, one can construct a statement that
- can be neither proven nor disproven within that system
- OR -
- can be both proven and disproven within that system.
In the first case, we call the axiomatic system incomplete, in the second case we call it inconsistent. A statement of the above type is called undecidable in the system.
Gödel's second incompleteness theorem, which is proved by formalizing part of the proof of the first within the system itself, states that a sufficiently strong consistent system cannot prove its own consistency.
Examples of undecidable statements
The subsequent combined work of Gödel and Paul Cohen has given concrete examples of undecidable statements (without using Gödel's theorem): both the axiom of choice and the continuum hypothesis are undecidable in the standard axiomization of set theory. Following this work, many more statements in set theory have been proven to be undecidable.
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.
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." 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.
In principle, Gödel's theorems still leave some hope: it might be possible to produce a general algorithm which 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.
Note that Gödel's theorems only apply to sufficiently strong axiomatic systems. This means that the axiomatic system should be strong enough to formulate the properties of natural numbers; this is true for example for all systems which are at least as powerful as Peano's axioms. There are weak axiomatic systems which are provably consistent and complete, for instance Presburger arithmetic.
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 Rosser in 1936.
In essence, the proof of the first theorem consists of constructing the statement
- p = "This statement cannot be proven"
within a formal axiomatic system. As such, it can be seen as a modern variant of the Liar paradox.
Note that, if the axiomatic system is consistent, Gödel's proof shows that p (and its negation) cannot be proven in the system. Therefore, if interpreted properly, p is "true" in some sense: after all, p claims not to be provable, and it isn't. Gödel himself adopted this interpretation: for him, p was a true statement that could not be proven within the system. Nowadays, mathematical logicians often prefer to avoid speaking about truth altogether.
Roger Penrose claims that this difference between "truth that can be mechanically proven" and "truth that can be understood by humans" shows that human intelligence is not mechanical in nature. This view is not widely accepted, because as stated by Marvin Minsky, human intelligence is capable of error and of understanding statements which are in fact inconsistent or false.
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 proven", p would have to somehow contain a reference to p, which could easily end in an infinite regress. Gödel's ingenious trick, which was later used by Alan Turing to solve the Entscheidungsproblem, will be described below.
First of all, 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 then is either provable in the system, or not. Statement forms themselves are not statements and therefore cannot be proven or disproven. But every statement form F(x) has a Gödel number which we will denote by 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 proven in our system. Formally: P(x) can be proven if and only if x is the Gödel number of a statement that can be proven. (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 F(G(F)), i.e. the form F applied to its own Gödel number, is not provable. This concept can be defined formally, and therefore we can construct a statement form SU(x) which embodies the concept: SU(x) is provable if and only if x is the Gödel number of a self-unprovable statement form. Then define the statement p = SU(G(SU)). This is the statement p that was mentioned above
Intuitively, we are now asking the question: "Is the property of being self-unprovable itself self-unprovable?" This is very reminiscent of the Barber's paradox: the barber who shaves precisely those people who don't shave themselves, does he shave himself?
If p were provable, then SU(G(SU)) would be true, and by definition of SU, that would make x = G(SU) 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 were provable, then, assuming our system to be consistent, p cannot also be provable, i.e. SU(G(SU)) is not provable, and by definition of SU this means that x = 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.
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. This proof 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.
- K. Gödel, Über formal unentscheidbare Sätze der Principia Mathematica und verwandter System. I. Monatshefte für Mathematik und Physik, 38 (1931), pp. 173-198. [transl. in From Frege to Gödel, van Heijenoort, Harvard Univ. Press, 1971., online at http://www.ddc.net/ygg/etext/godel/]
- B. Rosser. Extensions of some theorems of Goedel and Church. Journal of Symbolic Logic", 1 (1936), N1, pp. 87-91