In mathematical logic, Gödel's incompleteness theorems are two celebrated theorems proven by Kurt Gödel in 1930. Somewhat simplified, the first theorem states that:
In any consistent formal system of mathematics sufficiently strong to allow one to do basic arithmetic, one can construct a statement about natural numbers that can be neither proven nor disproven within that system.
In this context, a formal system of mathematics is an axiomatic system with a recursive set of axioms; equivalently, the theorems of the system can be generated by a Turing machine. The statement which cannot be proven nor disproven in the system is furthermore true in the sense that what it asserts about the natural numbers in fact holds. Because the system fails to prove a true statement, it is said to be incomplete. In other words, then, Gödel's first incompleteness theorem says that any sufficiently strong formal system of mathematics is either inconsistent or incomplete.
Gödel's second incompleteness theorem, which is proved by formalizing part of the proof of the first within the system itself, states that
Any sufficiently strong consistent system cannot prove its own consistency.
This answers Hilbert's second problem, which set the problem of proving that mathematics could be reduced to a consistent set of axioms from which all mathematical truths could be derived. See Hilbert's 23 problems for background.
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 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 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 "omegaconsistency".)
Now comes the trick: a statement form F(x) is called selfunprovable 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 selfunprovable 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 selfunprovable itself selfunprovable?" 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 selfunprovable statement form. Hence SU would be selfunprovable, which by definition of selfunprovable 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 selfunprovable form, which implies that SU is not selfunprovable. By definition of selfunprovable, 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.
External links and References
K. Gödel: Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme, I. Monatshefte für Mathematik und Physik, 38 (1931), pp. 173198. Translated in van Heijenoort: From Frege to Gödel. Harvard University Press, 1971., online at http://home.ddc.net/ygg/etext/godel/
Karl Podnieks: Around Goedel's Theorem
D. Hofstadter: Gödel, Escher, Bach: An Eternal Golden Braid, 1979, ISBN 0465026850. (1999 reprint: ISBN 0465026567).
An English translation of Hilbert's second problem
This article is licensed under the GNU Free Documentation License. It uses material from the Wikipedia article "Gödel's incompleteness theorems".
