Goedel, incompleteness theorem, liar paradox, liar, self reference, second, incompleteness, paradox, theorem, Rosser, Godel, Bernays

Back to title page.

5. Incompleteness Theorems

5.1. Liar's Paradox

Epimenides (VI century BC) was a Cretan angry with his fellow-citizens who suggested "All Cretans are liars". Is this statement true or false?

a) If Epimenides' statement is true, then Epimenides also is a liar, i.e. he is lying permanently, hence, his statement about all Cretans is false (and there is a Cretan who is not a liar). We have come to a contradiction.

b) If Epimenides' statement is false, then there is a Cretan, who is not a liar. Is Epimenides himself a liar? No contradiction here.

Hence, there is no direct paradox here, only an amazing chain of conclusions: if a Cretan says that "All Cretans are liars", then there is a Cretan who is not a liar.

Still, do not allow a single Cretan to slander all Cretans. Let us assume that Epimenides was speaking about himself only: "I am a liar". Is this true or false?

a) If this is true, then Epimenides is lying permanently, and hence, his statement "I am a liar" also is false. I.e. Epimenides is not a liar (i.e. sometimes he does not lie). We have come to a contradiction.

b) If Epimenides' statement is false, then he is not a liar, i.e. sometimes he does not lie. Still, in this particular case he is lying. No contradiction here.

Again, there is no direct paradox here, only an amazing chain of conclusions: if someone says "I am a liar", then he is not a (permanent) liar.

The next step in this story is due to Eubulides (IV century BC) who suggested, "I am lying". I.e. he said that he is lying right now. Is this true or false?

a) If this is true, then Eubulides is lying (right now!), and hence, his statement must be false. We have come to a contradiction.

b) If this is false, then Eubulides is not lying, and hence, his statement must be true. We have come to a contradiction.

Thus we have a real paradox, the famous Liar's paradox.

We would believe that any sentence like as "I am writing" or "I am reading" must be either true or false. Still, the sentence "I am lying" cannot be qualified as true or false without contradictions. During the past two thousand years many people have thought that such paradoxes should be "solved" by inventing appropriate "rules of correct speaking". They have never been 100% successful, since any such "rules" always prohibit not only (some, but not all) paradoxes, but also many harmless and even useful sentences. For me, the creative potential hidden in paradoxes seems much more interesting than the "rules of correct speaking".

The "development process" of the Liar's paradox described above ended in XIV century when Jean Buridan stated it in an absolutely clear form:

"All statements on this folio are false."

P.S. There is only this one statement on "this folio".

Today's Buridan would say simply:

p: p is false.

If p is true, then p must be false. If p is false, then p must be true.

Note. Buridan is known also as the owner of the famous ass, who starved to death standing equidistant from two identical bales of hay being unable to find "sufficient arguments" to choose one of them.

For those people who believe that the "rules of correct speaking" do not allow statements referring to themselves, Albert of Saxony proposed in XIV century the following paradoxes (see Styazhkin [1967]):

p1: p2 is false,
p2: p1 is true.

q1: q2 is false,
q2: q3 is false,
q3: q1 is false.

Exercise 5.1. Today, following these examples, mathematicians could invent much more sophisticated paradoxes... End of Exercise 5.1.

Let us try to "accept" the Liar's paradox by extending the usual classification of statements as true or false only:

a) True statements,

b) False statements,

c) Statements having no truth-value.

Now consider the statement:

q: q is false or q has no truth-value.

a) If q is true, then either q is false or q has no truth-value, i.e. q is not true. We have come to a contradiction.

b) If q is false, then q is true. We have come to a contradiction.

c) If q has no truth-value, then q is true. We have come to a contradiction.

Hence, our extended classification of statements is incomplete again. The above statement q is called the Extended Liar's paradox.

Exercise 5.2. In some sense, the Liar is a paradox of the usual two-valued logic, and q is a paradox of three-valued logic. Formulate an analogous paradox of four-valued logic etc. How far can we go this way?

For historic details see

N.I.Styazhkin. Formation of the Mathematical Logic. Nauka Publishers, Moscow, 1967, 400 pp. (in Russian, see also the English translation: Styazhkin, N. I. History of Mathematical Logic from Leibniz to Peano. MIT Press, Cambridge, MA, 1969)

5.2. Self-Reference Lemma

Would it be possible to formulate the paradoxes of the previous section in a formal theory like PA? If you wish to reconstruct the classical Liar's paradox, then you must build a formula Q "asserting" that "PA proves ~Q". How could you force a formula to "assert" its own properties? Moreover, how to force a formula to "speak" about formulas? Normally, formulas of the first order arithmetic are "speaking" about natural numbers. In order to force these formulas to "speak" about themselves we must introduce some numerical coding of formulas.

First let us fix some enumeration of basic symbols of PA (let us build variable names via the following pattern: x, xa, xaa, xaaa...):

x -- a -- 0 -- 1-- + -- * -- = -- ( -- ) -- ~ -- & -- v -- -> -- E -- A
0 -- 1 -- 2 -- 3 -- 4 -- 5 -- 6 - 7 - 8 - 9 - 10 -- 11 -- 12 -- 13 -- 14

Now, each formula can be represented as a sequence of natural numbers. For example, the formula x=xa+1+1 can be represented as 0, 6, 0, 1, 4, 3, 4, 3. By using Goedel beta-function (see Section 3.3) each sequence of natural numbers can be represented by two numbers. For example, the code of the formula x=xa+1+1 will consist or two numbers m, n such that:

beta(m, n, 0)=8 (length of the formula);

beta(m, n, 1)=0; beta(m, n, 2)=6; beta(m, n, 3)=0; beta(m, n, 4)=1; beta(m, n, 5)=4; beta(m, n, 6)=3; beta(m, n, 7)=4; beta(m, n, 8)=3.

From Section 3.3 we know that such two numbers do exist. As the last step, we can represent the pair (m, n) by a single number, for example, by

k = (m+n)²+m.

Exercise 5.3. Show how to restore m and n from a given k.

Therefore, we can represent each PA-formula F by a single natural number. Let us denote by bold F the PA-term corresponding to this number, and let us call it Goedel number of F. (It was Goedel's idea to represent formulas by numbers, thus making possible to discuss formulas in the language of arithmetic). Having a formula F we can calculate its Goedel number F and having the number F, we can restore F.

Note. Today, the idea of a numerical coding of formulas may seem almost trivial (just "another coding" among thousands of them used every second). However, in 1930, when Goedel invented such a coding for the first time, it was, perhaps, the most difficult idea of his famous incompleteness proof.

Now let us take two PA-formulas C(x) and B. We can view the formula C(B) as an assertion "formula B possess the property C". If we could prove in PA that B <-> C(B), we could say that B "asserts" that it possess the property C.

Self-Reference Lemma. If a PA-formula C(x) contains exactly one free variable, then one can build a closed PA-formula B such that:

PA proves: B <-> C(B).

Note. In other textbooks, this lemma is called also Diagonal Lemma, or Fixed-Point Lemma.

Proof. Let us introduce the so-called substitution function sub(x, y). We define the value sub(x, y) as follows: if x is Goedel number of of some formula F(u, v, w,...), then we substitute the number-term y for all free variables of F, i.e. we obtain the formula F(y, y, y,...), then we calculate its Goedel number n, and set sub(x, y)=n. If x is not Goedel number of a formula, then we set sub(x, y)=0.

No doubt, sub(x, y) is a computable function. Given x and y, we determine first, is x number of some formula or not. If not, our function returns 0. If yes, we restore the formula, substitute y for all of its free variables and return the number of the formula obtained. No problem to code this program, for example, in Pascal (it would be an extensive work, yet not a hard one). Somewhat more tedious work would be coding the program of sub(x, y) for a Turing machine. We will not do this work here, using the Church's thesis instead: any function that seems to be computable can be coded for an appropriate Turing machine.

So, let us assume that we already have a Turing machine computing sub(x, y). Using the algorithm from the proof of the Representation theorem (Section 3.3) we can build a PA-formula SUB(x, y, z) such that for all k, m, n: if sub(k, m)=n, then

a) PA proves: SUB(k, m, n),

b) PA proves: ~(z=n) -> ~SUB(k, m, z).

First step. Having two formulas SUB(x, y, z) and C(x) let us introduce the following formula C₁(x): C(sub(x, x)). Or more precisely (since we do not have in PA the function symbol sub):

Az(SUB(x, x, z) -> C(z)).

The main idea is here the repetition of x in sub! Now, what is "asserted" in the formula C₁(x)? Literally, the following: "Take the number x, restore from x the formula F_x(u, v, w,...) having this number, substitute x (i.e. the number of F_x itself) for all free variables of F_x, then you will obtain the formula F_x (x, x, x,...) that possess the property C".

Second step. Let us try to apply this operation to the formula C₁(x) itself! I.e., if k is the number of C₁(x), let us denote by B the formula C₁(k). What is the "assertion" of B? "If you take the formula having the number k (i.e. the formula C₁(x)), and substitute its number k for x, then you will obtain a formula (in fact, the formula C₁(k), i.e. the formula B) that possess the property C." Hence, B asserts; "I possess the property C"!

Warning! Do not try to follow the above argument more than twice. It may cause health problems - the Self-Reference Lemma is a kind of fixed-point theorems!

Now, to complete the proof, we must prove in PA that B <-> C(B).

1. Let us prove in PA that B -> C(B). Let us assume B, i.e. C₁(k), or

Az(SUB(k, k, z) -> C(z)). --------(1)

Since sub(k, k)= B, then:

PA proves: SUB(k, k, B), and PA proves: ~(z=k) -> ~SUB(k, k, z). ---------(2)

Hence, z in (1) equals to B, and we obtain C(B). The Deduction theorem does the rest: PA proves: B -> C(B).

2. Let us prove in PA that C(B) -> B. Let us assume C(B). Then we have SUB(k, k, B) -> C(B). Add (2) to this, and you will have Az(SUB(k, k, z) -> C(z)), and this is exactly the formula B. The Deduction theorem does the rest: PA proves: C(B) -> B.

Q. E. D.

So, for any property of formulas we can build a formula that "asserts" that it possess this property.

About the authors. Kurt Goedel invented the argument used in the proof of Self-Reference Lemma to prove his famous incompleteness theorem in 1930. Still, he did not formulate the Self-Reference Lemma as a general statement. Perhaps, Rudolf Carnap pointed out first the possibility of the above general formulation (see copies of all the relevant papers in Davis [1965]):

R.Carnap. Die Antinomien und die Unvollstaendigkeit der Mathematik. "Monatshefte fuer Mathematik und Physik", 1934, Vol.41, pp.263-284.

Exercise 5.4 (inspired by the paper by Andrzej Mostowski mentioned below). Show that, if B(x,y) and C(x,y) are two PA-formulas containing exactly two free variables, then one can build two closed PA-formulas D and E such that:  

PA proves: D <-> B(D, E), and PA proves: E <-> C(D, E).

If B contains only y, and C contains only x then D <-> B(E) and E <-> C(D), i.e. formulas D, E "slander" each other. (Hint: Introduce the substitution function sub₂(x, y, z) - define the value sub₂(x, y, z) as follows: if x is Goedel number of of some formula F(u, v, w,...), then substitute the number-term y for u, and the number term z - for all the other free variables of F, i.e. obtain the formula F(y, z, z,...), then calculate its Goedel number n, and set sub₂(x, y, z)=n. After this, consider B(sub₂(x, x, y), sub₂(y, x, y)) and C(sub₂(x, x, y), sub₂(y, x, y)), etc.).

A.Mostowski. A generalization of the incompleteness theorem. "Fundamenta Mathematicae", 1961, vol.49, N2, pp.205-232.

5.3. Goedel's Incompleteness Theorem

It seems that Self-Reference Lemma allows formulating the Liar's paradox in PA. In this way, inconsistency of PA will be proved?

The formal version of Liar's paradox would be a formula L that asserts "PA proves ~ L". Then ~L would assert "PA cannot prove ~ L". Hence, instead of L we could use a formula G asserting, "PA cannot prove G" (i.e. "I am not provable in PA"). This version of Liar's paradox was used in the original Goedel's proof. So let us follow the tradition.

We could obtain Goedel's formula:

G: PA cannot prove G

from Self-Reference Lemma, if we had a formula PR(x) asserting "the formula number x can be proved in PA". Indeed, by applying this lemma to the formula ~PR(x) we would obtain the formula G such that

PA proves: G <-> ~PR(G),

i.e. G would be equivalent to "PA cannot prove G". So, let us first build the formula PR(x). Each proof (in PA) is a sequence of formulas. Replace all formulas by their Goedel numbers, this converts each proof into a sequence of natural numbers. You can code this sequence by a single number (using the techniques of the previous section). Let us call this number the Goedel number of the proof. Given a natural number y, you can:

a) Determine whether y is a number of some sequence of formulas or not.

b) If it is, you can restore the sequence.

c) Having the sequence of formulas you can check whether it is a proof in PA or not. In a PA-proof each formula must be either an axiom of PA, or a logical axiom, or it must be derived from some previous formulas of the proof by using one of the logical inference rules.

Hence, the following predicate seems to be computable:

prf(x, y) = "y is a proof-number of the formula number x".

According to Church's thesis we can construct a Turing machine checking correctly the truth value of prf(x, y) for arbitrary x and y. After this, according to Representation theorem (Section 3.3) we can construct a PA-formula PRF(x, y) expressing the predicate prf(x, y).

Now we can take the formula EyPRF(x, y) as a formula asserting "the formula number x can be proved in PA". By applying Self-Reference Lemma to the formula ~EyPRF(x, y) we obtain Goedel's formula G such that

PA proves: G <-> ~EyPRF(G, y). --------(1)

I.e. G says, "PA cannot prove G".

Let us try to check whether the assertion of G is true or false.

1. First, let us assume that PA proves G, and k is the number of this proof. Then prf(G, k) is true and hence,

PA proves: PRF(G, k),

PA proves: EyPRF(G, y),

PA proves: ~G

(see (1)). Therefore, if we had a PA-proof of G, then we could build also a PA-proof of ~G, i.e. PA would be inconsistent. Is PA consistent? I do not know. Still, if it is, then G cannot be proved in PA.

2. Now, let us assume that - on the contrary - PA proves ~G. Then PA proves EyPRF(G, y) (see (1)). Intuitively, EyPRF(G, y) says that there exists PA-proof of G, i.e. it seems that PA is inconsistent also in this case? Still, we must be careful: if PA proves EyPRF(G, y), does it mean that by substituting for y one by one all numbers 0, 1, 2, 3,... , and checking each case, we will find the proof of G?

We would like to think so, yet we are not able to prove that this is the case. If, by the above-mentioned substituting and checking we will really find a proof of G, then PA will be proved inconsistent. Still, what if we will never find a proof of G? Then we will have no direct contradiction in PA. Nevertheless, we will have an unpleasant situation: there is a formula C(y) (namely, PRF(G, y)) such that:

a) PA proves: EyC(y),

b) For each k, PA proves: ~C(k).

This is not a "direct" contradiction. To have a "direct" contradiction we must prove Ay~C(y). We have a separate proof of ~C(y) for each particular value of y. Are you able to replace this infinite sequence of particular PA-proofs by a single (finite!) PA-proof of Ay~C(y)? I am not. And Goedel was not, too. He was forced to introduce the notion of w-inconsistency (weak inconsistency, or omega-inconsistency) to designate the above unpleasant situation.

Exercise 5.5. Show that if PA is inconsistent, then it is also w-inconsistent.

Therefore, in the second part of our investigation (assuming that PA can prove ~G), we could have established only the w-inconsistency of PA.

Nevertheless, we have proved the famous

Goedel's Incompleteness Theorem (for PA). One can build a closed PA-formula G such that:

a) If PA proves G, then PA is inconsistent.

b) If PA proves ~G, then PA is w-inconsistent.

Why is this theorem considered one of the most revolutionary results in mathematical logic?

Let F be a closed formula of some formal theory T. If neither F, nor ~F can be proved by using the axioms of T, then F is called undecidable in T (or T-undecidable). I.e. F predicts some "absolutely definite" property of the "objects" of T, yet this prediction can be neither proved, nor refuted. A theory containing undecidable formulas is called incomplete theory. Hence the term "incompleteness theorem": if PA is w-consistent, then PA is incomplete.

Do not think, however, that we have proved the incompleteness of PA. We can prove the undecidability of Goedel's formula G only after we have proved that PA is w-consistent. Until this, we have proved only that PA is not perfect: PA is either w-inconsistent, or incomplete. I.e., when developing PA, we will run inevitably either into a w-contradiction, or into a natural number problem that cannot be solved by using the axioms of PA. (One of such problems might be expressed by the Goedel's formula G. It only seems that G is busy with its own provability, actually, as a closed PA-formula G asserts some property of natural numbers!)

If our axioms are not perfect, we can try to improve them. Perhaps, we have missed some essential axioms? Let us add these axioms to PA, and we will obtain... a perfect theory?

Unfortunately, this is impossible. Goedel's proof remains valid for any extensions of PA. An extension of PA is nevertheless some formal theory T (in the language of PA). I.e. by definition, the predicate

prf_T(x, y) = "y is a T-proof-number of the formula number x"

must be computable (a theory is called formal, iff we have a "mechanical" procedure for checking the proof correctness in this theory). Hence, we can build a formula PRF_T(x, y) expressing this predicate in PA. Let us apply, again, the Self-Reference Lemma, and we will have a closed formula G_T such that

PA proves: G_T <-> ~EyPRF_T (G_T, y),

i.e. G_T "asserts" its own unprovability in T.

Exercise 5.6. Prove that if T is an extension of PA (i.e. if T can prove all theorems of PA), then:

a) If T proves G_T, then T is inconsistent.

b) If T proves ~G_T, then T is w-inconsistent.

Therefore, Goedel's method allows to prove that a perfect axiom system of natural number arithmetic is impossible: any such system is either w-inconsistent, or it is insufficient to solve some natural number problems.

From the History

Summary of some facts about this first turning point in the history of mathematical logic:

Goedel K. [1931] Ueber formal unentscheidbare Saetze der Principia Mathematica und verwandter Systeme. "Monatshefte fuer Mathematik und Physik", 1931, Vol. 38, pp. 173-198 . See online English translation at http://home.ddc.net/ygg/etext/godel/index.htm (by Bernard Meltzer, 1962, published in Yggdrasil's WN Library).

(See also English translations in Davis [1965] or Heijenoort [1967], and online comments at http://thoralf2.uwaterloo.ca/htdocs/scav/goedel/goedel.html).

Since 1940 Goedel lived in the U.S., he died on January 14, 1978. See

John W.Dawson Jr. Max Dehn, Kurt Godel, and the Trans-Siberian Escape Route. Notices of the AMS, 2002, Vol.49, N9, pp1068-1075 (avaialable online at http://www.ams.org/notices/200209/fea-dawson.pdf).

About Goedel's contribution to Einstein's general relativity theory see http://www.ettnet.se/~egils/essay/essay.html.

How did Godel arrive at the Incompleteness Theorem during the summer 1930? See a brief account by Jeffrey Ketland in my Quotes of the Day

Wir muessen wissen -- wir werden wissen! David Hilbert's Radio Broadcast, Koenigsberg, 8 September 1930 (audio record published by James T.Smith, and translations in 7 languages published by Laurent Siebenmann). Could Goedel hear it? Yes: "...according to Gödel's biographer John Dawson, Hilbert and Gödel never discussed it, they never spoke to each other. The story is so dramatic that it resembles fiction. They were both at a meeting in Koenigsberg in September 1930. On September 7th Goedel off-handedly announced his epic results during a round-table discussion. Only von Neumann immediately grasped their significance... The very next day, September 8th, Hilbert delivered his famous lecture on ``Logic and the understanding of nature.'' As is touchingly described by Hilbert's biographer Constance Reid (see Reid [1996] - K.P.), this was the grand finale of Hilbert's career and his last major public appearance. Hilbert's lecture ended with his famous words: ``Wir muessen wissen. Wir werden wissen.'' We must know! We shall know!" (from a G.J.Chaitin's lecture, Buenos Aires, 1998).

"Historians and Mathematicians agree, 1930 was Goedel’s most profound year – if one was to include the latter part of 1929 as well. It is in this year that Goedel states he first heard of Hilbert’s proposed outline of a proof of the continuum hypotheses. In the summer, Goedel began work on trying to prove the relative consistency of analysis. Goedel soon discovered that truth in number theory is undefinable – he later went on to prove a combinational form of the Incompleteness Theorem.

In 1930, Goedel traveled several days to attend the Second Conference on Epistemology of the Exact Sciences (September 5-7). Towards the end of the Conference on the last day, Goedel spoke for the first time and, "criticized the formalist assumption that consistency of ‘transfinite’ axioms assures the nonderivability of any consequence that is ‘contentually false.’ He concluded, ‘For of no formal system can one affirm with certainty that all contentual considerations are representable in it.’ And then v. Neumann interjected, ‘It is not a foregone conclusion whether all rules of inference that are intuitionistically permissible may be formally reproduced.’" It was after this statement, that Goedel made the announcement of his incompleteness result, "Under the assumption of the consistency of classical mathematics, one can give examples of propositions…that are contentually true, but are unprovable in the formal system of classical mathematics." It was these events which preceded the formal 1931 publishing of Goedel’s article Uber formal unentscheidbare Saetze der Principia Mathematica und verwandter Systeme." (A fragment from Goedel, and his Incompleteness Theorem by Mark Wakim).

About this event, see also

John L. Casti. The One True Platonic Heaven: A Scientific Fiction of the Limits of Knowledge. Joseph Henry Press, 2003 (many interesting online fragments available at http://books.nap.edu/books/0309085470/html/1.html)

and

Paolo Mancosu. Between Vienna and Berlin: The Immediate Reception of Godel's Incompleteness Theorems. History and Philosophy of Logic, 1999, Vol.20, N1, pp.33-45.

Goedel's 1942 summer vacations in Blue Hill, Maine: "...Throughout the summer Louise Frederick received agitated telephone calls from people of the town. Who was this scowling man with a thick German accent walking alone at night along the shore? Many thought Goedel was a German spy, trying to signal ships and submarines in the bay..." (Peter Suber, "Kurt Goedel in Blue Hill").

See also interesting photos and biographical data in Kurt Goedel - Leben und Werk by Markus Krumpoeck.

The idea of "formal" modeling of paradoxes to generate "formally undecidable" statements was first used, perhaps, by Paul Finsler in 1926:

P.Finsler. Formale Beweise und die Entscheidbarkeit. "Mathematische Zeitschrift", 1926, Vol. 25, pp. 676-682 (see English translation in Heijenoort [1967], pp. 438- 445)

Emil Leon Post "... in the 1920s ...proved results similar to those which Goedel, Church and Turing discovered later, but he did not publish them. He reason he did not publish was because he felt that a 'complete analysis' was necessary to gain acceptance... In a postcard written to Goedel in 1938, just after they had met for the first time, Post wrote: ... As for any claims I might make perhaps the best I can say is that I would have proved Goedel's Theorem in 1921 - had I been Goedel." (according to MacTutor History of Mathematics archive).

Rosser's Version

In 1936 John Barkley Rosser (1907-1989, see also http://www.jmu.edu/finaid/scholarships/econ.shtml) improved Goedel's proof. He removed the notion of w-consistency from the formulation, replacing it by the (usual) consistency:

J.B.Rosser. Extensions of some theorems of Goedel and Church. "Journ. Symb. Logic", 1936, vol.1, N1, pp.87-91 (received September 8, 1936)

Goedel's Incompleteness Theorem (Rosser's version). If T is an extension of PA (i.e. if T can prove all theorems of PA), then one can build a closed PA-formula R_T (i.e. a formula asserting some property of natural numbers) such that if T proves R_T or T proves ~R_T, then T is inconsistent.

Proof. Immediately - from the extended version below.

Until now, all our versions of incompleteness theorems were bound to the specific language of PA. One could suspect, therefore, that the incompleteness phenomenon could be caused by an improper choice of the language and/or the logical system (axioms and rules of inference). Still, as will be established below, the incompleteness theorem can be proved for any fundamental formal theories - based on arbitrary languages and/or logical systems (first order, second order, or any other).

Recall (Section 3.2), that a formal theory T is called a fundamental formal theory, iff there is a translation algorithm Tr from PA into T such that, for all closed PA formulas F, G:

Fu₁) If PA proves F, then T proves Tr(F).

Fu₂) T proves Tr(~F), iff T proves ~Tr(F).

Fu₃) If T proves Tr(F), and T proves Tr(F->G), then T proves Tr(G).

Note. We will not need the condition Fu₃ in the proof below.

Goedel's Incompleteness Theorem (extended version). If T is a fundamental formal theory (only conditions Fu₁, Fu₂ are necessary), then one can build a closed PA-formula R_T (i.e. a formula asserting some property of natural numbers) such that if T proves Tr(R_T) or T proves ~Tr(R_T), then T is inconsistent.

Proof. We know from the Exercise 3.6 that any particular fundamental formal theory T can prove only an computably denumerable set of closed PA-formulas. Let us construct a Turing machine, which enumerates all these formulas:

F₀, F₁, F₂, F₃,... -------(1)

Thus, for all k, T proves Tr(F_k). The following predicate is computable:

prf_T(x, t) - "the formula number x appears in (1) as F_t".

Let the formula PRF_T(x, y) express this predicate in PA. The following predicate is computable, too (ref - refute):

ref_T(x, t) - "the negation of the formula number x appears in (1) as F_t".

Let the formula REF_T(x, y) express this predicate in PA.

Rosser's key idea was the following. Goedel's formula G_T asserts "I cannot be proved in T". Let us take, instead, a formula R_T asserting "I can be easier refuted than proved in T". If the "proof complexity measure" of formulas would be defined as their place numbers in (1), then the Rosser's formula could be obtained from Self Reference Lemma by taking the following formula as C(x):

At(PRF_T(x, t) -> Ez(z<t & REF_T(x, z)).

Then there is a PA-formula R_T such that

PA proves: R_T <-> At(PRF_T(R_T, t) -> Ez(z<t & REF_T(R_T, z)). --------(2)

1. Assume that T proves Tr(R_T). Then R_T appears in (1) as, for example, F_k. Hence,

PA proves: PRF_T(R_T, k). --------(3)

Let us take t=k in (2), then:

PA proves: R_T -> Ez(z<k & REF_T(R_T, z)). ---------(4)

If, indeed, ~R_T appears in (1) as F_m with m<k, then T proves Tr(~R_T), and, by Fu₂, T proves ~Tr(R_T), i.e. T is inconsistent. Otherwise,

PA proves: ~REF_T(R_T, 0)&~REF_T(R_T, 1)&...&~REF_T(R_T, k-1).

Hence,

PA proves: Az(z<k -> ~REF_T(R_T, z)),

and

PA proves: ~Ez(z<k & REF_T(R_T, z)),

and, by (4), PA proves ~R_T. Then, by Fu₁ and Fu₂, T proves Tr(~R_T) and ~Tr(R_T), i.e. T is inconsistent.

2. Assume now that T proves ~Tr(R_T), i.e., by Fu₂, T proves Tr(~R_T). Then ~R_T appears in (1) as, for example, F_k. Hence,

PA proves: REF_T(R_T, k),

and

PA proves: At(t>k -> Ez(z<t & REF_T(R_T, z))) -------(5)

(if t>k, then we can simply take z=k).

If R_T appears in (1) before ~R_T, then T proves Tr(R_T), and T is inconsistent. If R_T does not appear before ~R_T, then

PA proves: ~PRF_T(R_T, 0)&~PRF_T(R_T, 1) & ... & ~PRF_T(R_T, k-1)& ~PRF_T(R_T, k).

Hence,

PA proves: At(t<=k -> ~PRF_T(R_T, t)).

Together with (5) this means that

PA proves: At(~PRF_T(R_T, t) v Ez(z<t & REF_T(R_T, z))),

i.e.

PA proves: At(PRF_T(R_T, t) -> Ez(z<t & REF_T(R_T, z))).

According to (2), this means that PA proves R_T, and, by Fu₁, T proves Tr(R_T), i.e. T is inconsistent.

End of proof.

Now we can state the strongest possible form of the Goedel's "unperfectness principle": a fundamental theory cannot be perfect - either it is inconsistent, or it is insufficient for solving some of its problems.

The fundamentality (the possibility to prove the principal properties of natural numbers) is essential here, because some non-fundamental theories may be sufficient for solving all of their problems. As a non-trivial example of non-fundamental theories can serve the Presburger arithmetic (PA minus multiplication, see Section 3.1). In 1929 M. Presburger proved that this theory is both consistent and complete. After Goedel and Rosser, this means now that Presburger proved that his arithmetic is not a fundamental theory.

Non-standard Arithmetic

We know that if PA is consistent, then the formula G cannot be proved in PA, hence, the theory PA+{~G} is consistent, too. Since

PA proves: ~G <-> EyPRF(G, y),

the theory PA+{ EyPRF(G, y) } is also consistent. On the other hand, for each natural number k:

PA proves: ~PRF(G, k).

Let us denote PRF(G, y) by C(y). Hence, if PA is consistent, then there is a formula C(y) such that PA+{ EyC(y) } is a consistent theory, yet for each natural number k: PA proves ~C(k). Imagine, you wish to invetisgate the theory PA+{ EyC(y) }- why not? - it is "as consistent" as PA. In this theory the axiom EyC(y) says that there is a number y that does possess the property C. On the other hand, for each "standard" natural number k we can prove ~C(k), i.e. that k does not possess the property C. Hence, when working in the theory PA+{ EyC(y) }, we are forced to admit the existence of non-standard natural numbers.

Exercise 5.7 (for smart students). Prove in PA+{ EyC(y) }that there is some minimum number w₀ having the property C. On the other hand, consider a model of PA+{ EyC(y) }. Define standard numbers as interpretations of numerals 0, 1, 2, etc. Verify that: a) each standard number is less than any non-standard number, b) there is no maximum standard number, c) there is no minimum non-standard number, d) standard numbers cannot be defined by a formula in the language of PA.

Exercise 5.8. (inspired by the paper Mostowski [1961]) Return to the paradoxes stated by Albert of Saxony (Section 5.1). Which kind of incompleteness theorems could you derive by modeling these paradoxes in PA? You may find helpful the result of the Exercise 5.4. (Hint: Mostowski defines two closed formulas F, H as T-independent, iff none of the following conjunctions can be proved in T: F&H, F&~H, ~F&H, ~F&~H. Assume, T is w-consistent, and use the first Albert's paradox to build two T-independent formulas. Could you provide the "Rosserian" version of your proof?)

5.4. Goedel's Second Theorem

Pure mathematical contents of incompleteness theorems (without any attempt of "interpretation") are as follows: there are two algorithms due to Goedel and Rosser.

Algorithm 1. Given the axioms of a fundamental formal theory T this algorithm produces a closed PA-formula R_T. As a closed PA-formula, R_T asserts some property of the natural number system.

Algorithm 2. Given a T-proof of the formula Tr(R_T) or the formula ~Tr(R_T), this algorithm produces a T-proof of a contradiction.

Therefore, if T is a fundamental theory, then either T is inconsistent, or it can neither to prove, nor to refute the hypothesis R_T. A theory that is able neither to prove, nor to refute some closed formula in its language, is called incomplete. Hence, Goedel and Rosser have proved that each fundamental theory is either inconsistent, or incomplete.

Why is this theorem called incompleteness theorem? The two algorithms developed by Goedel and Rosser do not allow deciding whether T is inconsistent or incomplete (verify). Hence, to prove "via Goedel" the incompleteness of some theory T, we must prove that T is consistent. Still, as we already know (Section 1.5), in a reliable consistency proof we should not use questionable means of reasoning. The aim of Hilbert's program was to prove consistency of the entire mathematics by means as reliable as the ones containing in the first order arithmetic (i.e. PA). Hence, to prove the consistency of PA we must use... PA itself?

Let us formalize the problem. In the previous section, having a fundamental formal theory T we considered some enumeration of all PA-formulas that can be proved in T:

F₀, F₁, F₂, F₃,... ---------- (1)

From a Turing machine program generating (1) we derived a PA-formula PRF_T (x, y) expressing in PA the predicate

prf_T (x, y) = "the formula number x appears in (1) as F_y".

Then the formula EyPRF_T (x, y) asserts, that the formula number x is provable in T. If T is inconsistent, then in T all formulas are provable, i.e. 0=1 is also provable. And conversely, if we have proved that in T some formula (for example, 0=1) cannot be proved, then we have proved that T is consistent. Hence, the formula ~EyPRF_T (0=1, y), in a sense, asserts that T is a consistent theory. Let us denote this formula by Con(T).

Unexpectedly, the properties of Con(T) depend on the choice of the formula PRF_T (x, y). (I got to know about the experiment described below from the Appendix 1 written by A.S.Yessenin-Volpin for the 1957 Russian translation of Kleene [1952], see p.473 of the translation, see also p.37 of Feferman [1960]).

Having the formula PRF_T (x, y) let us introduce another formula PRF1_T (x, y):

PRF_T (x, y) & ~PRF_T (0=1, y).

If T is consistent, then 0=1 cannot be proved in T, hence, for all k:

PA proves: ~PRF_T ((0=1, k).

And hence, PRF1_T (x, y) - like as PRF_T(x, y) - expresses in PA the predicate prf_T (x, y). Now let us build the corresponding formula Con1(T) as ~EyPRF1_T (0=1, y), or:

~Ey(PRF_T (0=1, y)&~PRF_T (0=1, y).

This formula Con1(T) can be proved (almost) in the propositional calculus! Does it mean that the propositional calculus can prove the consistency of an arbitrary formal theory T? Yes, and even the consistency of inconsistent theories! Then, where is the trick? The trick is: we assumed that T is consistent before we started our "consistency proof". Only this assumption allows to prove that PRF1_T (x, y) expresses the predicate prf_T (x, y), and hence - that Con1(T) asserts the consistency of T. If we assume the consistency of T from the very beginning, then we can easily "prove" Con1(T) (an equivalent of our assumption!) by using the most elementary logical rules.

However, the lesson of this experiment is very useful. If we intend to discuss the means that are able (or not) to prove the formula Con(T), then we must check carefully the means that were used to establish that Con(T) asserts consistency of theory T.

If Con(T) is built in a "natural" way, i.e by using a formula PRF_T (x,y) obtained by direct modeling of an appropriate Turing machine program, then the "watched means" do not exceed PA. It would be hard to demonstrate this here directly, yet it is not surprising. When proving the Representation Theorem in Section 3.3, we used only elementary logical and arithmetical means of reasoning.

Now, what means of reasoning are necessary to prove the "natural" formula Con(T) - if theory T is "really" consistent? Let us assume we were successful to prove Con(T) in some way. What kind of consequences could be drawn from this proof? The most powerful means to draw consequences from the consistency proof of some theory would be, perhaps, ... the incompleteness theorems! Goedel's theorem says:

"If T is consistent, then the formula G_T cannot be proved in T".

And G_T says exactly that it cannot be proved in T. Hence, "if Con(T), then G_T". Or, formally:

Con(T) -> G_T.

This is the formal equivalent of Goedel's incompleteness theorem (the part one of it). What means of reasoning were used to prove this theorem? Return to the previous section, and you will see that there only (a fantastic combination of) elementary logical and arithmetical means were used. Hence, we can conclude that

PA proves: Con(T) -> G_T. -------- (2)

It would be hard to prove this here 100% directly, yet it is not surprising. As we know, the axioms of PA cover 100% of elementary logical and arithmetical means of reasoning.

Now, imagine that you were successful in proving Con(T) according to the standards of Hilbert's program, i.e. by using only the means formalized in PA, i.e.

PA proves: Con(T).

Add (2) to this, and you will have: PA proves G_T. If T is a fundamental theory, then T proves all theorems of PA, and hence, T also proves G_T. From Goedel's incompleteness theorem we know that, if T proves G_T, then T is inconsistent. Therefore, if PA proves Con(T), then T is inconsistent! And, if PA proves Con(PA), then PA is inconsistent!

Kurt Goedel first formulated this conclusion in the same famous 1931 paper, and now it is called Goedel's Second Theorem.

Goedel's Second Theorem shows that Hilbert's program cannot be 100% successful. Let us recall the two stages of this program:

a) Build a formal theory T covering the entire mathematics.

b) Using PA, prove the consistency of T.

The first stage was accomplished when the modern axiomatic set theories were formulated. Still, the difficulties in advancing the second stage appeared to be principal ones: using PA, it is impossible to prove even the consistency of PA itself!

Let us recall also the warning by Henri Poincare - his reaction to the first attempts by Russell and Hilbert to initiate rebuilding of the foundations of mathematics (see Poincare [1908], Volume II, Chapter IV):

Do not try justifying the induction principle by means of the induction principle. This would be a kind of vicious circle.

The induction principle builds up 99% of PA, hence, do not try to prove the consistency of PA by means of PA! And Goedel's Second Theorem says: of course, you can try, yet if you will succeed, then you will prove that PA is inconsistent!

The reaction by David Hilbert to the failure of his program was quite different from that by Frege and Cantor. The following elegant and extremely general version of Goedel's Second Theorem results, in fact, from an analysis of Goedel's proof performed by Hilbert and Paul Bernays (see Hilbert, Bernays [1934, 1939], Volume II, Chapter V).

Recall (Section 3.2), that a formal theory T is called a fundamental formal theory, iff there is a translation algorithm Tr from PA into T such that, for all closed PA formulas F, G: Fu₁) if PA proves F, then T proves Tr(F); Fu₂) T proves Tr(~F), iff T proves ~Tr(F); Fu₃) If T proves Tr(F), and T proves Tr(F->G), then T proves Tr(G). Thus, fundamental formal theories may be based on arbitrary languages and/or logical systems (first order, second order, or any other).

Instead of the formula PRF_T(x, y) expressing the predicate prf_T(x, y), let us concentrate on the formula EyPRF_T (x, y). Let us denote it by PR_T (x). This formula asserts: "T proves the formula number x", or more precisely, "T proves the T-translation of the PA-formula number x".

Now, let us forget about the origin of PR_T(x) - for the rest of this Section, PR_T(x) can be any PA-formula having exactly one free variable x.

As Goedel's formula G_T we can use any formula having the following property (such formulas do exist by the Self-Reference Lemma):

PA proves: G_T <-> ~PR_T(G_T).

Let us define the formula ACon(T) as ~PR_T(0=1).

Why ACon? Because ~PR_T(0=1) asserts only the consistency of the "arithmetical part" of T. Indeed, if, for some closed PA-formula B, T proves Tr(B), and T proves ~Tr(B), then, since PA proves ~B->(B->0=1), by Fu₁, Fu₂ and Fu₃, T proves Tr(0=1). The formula ~PR_T(0=1) asserts that T does not prove 0=1, hence, it implies that T cannot simultaneously prove and disprove Tr(B) for a closed PA-formula B.

Thus, let us say that a fundamental theory T is arithmetically consistent, iff, for all closed PA-formulas B, T does not prove Tr(B) and ~Tr(B) simultaneously. The formula ACon(T) asserts the arithmetical consitncy of T.

Of course, if T is consistent, then T is arithmetically consistent. The converse, in general, is not true. Indeed, in general, T may be simultaneously inconsistent and arithmetically consistent, i.e. T may prove C and ~C, where C is not a translation of a PA-formula. Only, if T is using the traditional logical system (which includes the axiom ~C->(C->B)), from any contradiction in T we can derive an arithmetical contradiction in T.

Let us say that the theory T "knows", that the formula ACon(T) asserts the arithmetical consistency of T, iff the following three Hilbert-Bernays-Löb derivability conditions hold for each pair of closed PA-formulas B, C:

H₁: If T proves Tr(B), then T proves Tr(PR_T(B)).

H₂: T proves: Tr[PR_T(B)) -> PR_T(PR_T(B))].

H₃: T proves: Tr[PR_T (B) -> (PR_T(B->C) -> PR_T(C))].

Conditions H₁ and H₂ say that T "knows" that the formula PR_T (x) "expresses" the notion T-provability. The condition H₃ says that T "knows" that the set of (arithmetical) theorems of T is closed under MODUS PONENS. Hence, if H₁, H₂, H₃ hold, we may, indeed, say that T "knows", that ACon(T) (i.e.~PR_T(0=1)) asserts the arithmetical consistency of T.

Note. The first version of derivability conditions was introduced in Hilbert, Bernays [1934, 1939] ( Volume II, Chapter V). The above more elegant version was proposed in 1955 by M.H.Löb:

M.H.Löb. Solution of a problem of Leon Henkin. "J. Symbolic Logic", 1955, vol.20, pp. 115-118.

Goedel's Second Theorem (extended version). If a fundamental formal theory T "knows" that the formula ACon(T) asserts the arithmetical consistency of T, then either T is arithmetically inconsistent, or Tr(ACon(T)) cannot be proved in T.

Note. One could suspect, that this phenomenon could be caused by an improper choice of the language and/or the logical system. Still, as is stated above, Goedel's second incompleteness theorem can be proved for any fundamental formal theories - based on arbitrary languages and/or logical systems (first order, second order, or any other).

Lemma 1 (formalized part-one of the first incompleteness theorem). If a fundamental formal theory T "knows" that the formula ACon(T) asserts the arithmetical consistency of T, then T proves Tr[PR_T(G_T)->PR_T(~G_T)].

Lemma 2. If a fundamental formal theory T "knows" that the formula ACon(T) asserts the arithmetical consistency of T, then T proves Tr(ACon(T) -> G_T).

Proof of Goedel's Theorem. By Lemma 2, T proves Tr(ACon(T) -> G_T). Let us assume that T proves Tr(ACon(T)).

Then, by Fu₃, T proves Tr(G_T), and, by H₁, T proves Tr(PR_T(G_T)).

Since PA proves PR_T(G_T)->~G_T, by Fu₁, T proves Tr(PR_T(G_T)->~G_T). Then, by Fu₃, T proves Tr(~G_T), and, by Fu₂, T proves ~Tr(G_T), i.e. T is arithmetically inconsistent. Q.E.D.

Proof of Lemma 1. First, let us formalize in T the proof of the (part one of) Goedel's incompleteness theorem: if T proves Tr(G_T), then T proves Tr(~G_T).

Since PA proves PR_T(G_T)->~G_T, by Fu₁, T proves Tr(PR_T(G_T)->~G_T). Then, by H₁, T proves Tr(PR_T(PR_T(G_T)->~G_T)). By H₃,

T proves: Tr[PR_T(PR_T(G_T))->(PR_T(PR_T(G_T)->~G_T)->PR_T(~G_T)].

By H₂, T proves Tr[PR_T(G_T)->PR_T(PR_T(G_T))].

Thus, we have the following situation. Let us denote PR_T(G_T) - by A, PR_T(PR_T(G_T)) - by B, PR_T(PR_T(G_T)->~G_T) - by C, and PR_T(~G_T) - by D. We know that:

T proves Tr(C),
T proves Tr(B->(C->D)),
T proves Tr(A->B).

By Exercise 3.5a, Fu₁ and Fu₃ imply that then T proves Tr(A->D), i.e. T proves Tr[PR_T(G_T)->PR_T(~G_T)]. Q.E.D.

Proof of Lemma 2. We must verify that T proves Tr(ACon(T)->G_T). We could derive this fact from

T proves: Tr(PR_T(G_T)->PR_T(0=1)). ------- (3)

Indeed, by Exercise 3.5a, Fu₁ and Fu₃ imply that if T proves Tr(A->B), then T proves Tr(~B->~A). Hence, from (3) we can derive that T proves Tr(~PR_T(0=1)->~PR_T(G_T)), i.e. T proves Tr(ACon(T)->~PR_T(G_T)).

Since PA proves ~PR_T(G_T)->G_T, by Fu₁, T proves Tr( ~PR_T(G_T)->G_T). Hence, by Exercise 3.5a, Fu₁ and Fu₃ imply that T proves Tr(ACon(T)->G_T).

So, let us prove (3). Since PA proves ~G_T->(G_T->0=1), by Fu₁, T proves Tr(~G_T->(G_T->0=1)). Then, by H₁, T proves Tr(PR_T(~G_T->(G_T->0=1))). By H₃,

T proves: Tr[PR_T(~G_T)->(PR_T(~G_T->(G_T->0=1))->PR_T(G_T->0=1))].

By Lemma 1, T proves Tr[PR_T(G_T)->PR_T(~G_T)].

Thus, we have the following situation. Let us denote PR_T(G_T) - by A, PR_T(~G_T) - by B, PR_T(~G_T->(G_T->0=1)) - by C, and PR_T(G_T->0=1) - by D. We know that:

T proves Tr(C),
T proves Tr(B->(C->D)),
T proves Tr(A->B).

By Exercise 3.5a, Fu₁ and Fu₃ imply that then T proves Tr(A->D), i.e. T proves Tr[PR_T(G_T)->PR_T(G_T->0=1)]. By H₃,

T proves: Tr[PR_T(G_T)->(PR_T(G_T->0=1)->PR_T(0=1))].

Thus, we have the following situation. Let us denote PR_T(0=1) by E. We know that:

T proves Tr(A->D),
T proves Tr(A->(D->E)).

By Exercise 3.5a, Fu₁ and Fu₃ imply that then T proves Tr(A->E), i.e. (3). Q.E.D.

Let us return to the above "abnormal" formula Con1(T) that could be proved almost in the propositional calculus. If Hilbert-Bernays-Loeb conditions were true for the corresponding formula PR1_T(x), then, according to Goedel's Second Theorem, T would be an inconsistent thenory. Hence, if T is consistent, then Hilbert-Bernays-Loeb conditions do not hold for PR1_T(x), and we can say that T does not "know" that Con1(T) asserts its consistency. Proves Con1(T), but does not "know" it!

On the other hand, it appears that Hilbert-Bernays-Loeb conditions hold for all formulas Con(T) obtained in a "natural" way, i.e. by direct formal modeling of an appropriate Turing machine program. To prove this for a particular formula - it is not a hard work, but nevertheless, an extensive one. Accordingly, for these "natural" formulas Goedel's Second Theorem holds: any fundamental theory T is either arithmetical inconsistent, or it cannot prove ACon(T).

If, in order to justify the axioms of some theory the consistency proof is required, then we can say that a fundamental theory cannot justify itself.

Still, how about non-fundamental theories? Some of them are not able even to formulate their own consistency problem. Either their languages do not allow to write formulas like PR_T(x) and ACon(T), or their axioms do not allow to prove Hilbert-Bernays-Loeb derivability conditions.

However, it appears that some "stronger" theories are able to prove consistency of some "weaker" theories. For example, in the set theory ZF you can prove consistency of the first order arithmetic PA (the set w appears to be a model where all the axioms of PA are true, see Appendix 1). If PA is consistent, then the formula Con(PA) cannot be proved in PA, yet its translation into the language of set theory can be proved in ZF. On the other hand, as a closed PA-formula Con(PA) asserts some property of natural numbers. This property can be proved in ZF, but not in PA (if PA is consistent). Thus we have obtained a positive answer to question stated in the Section 3.2: yes, there are statements which involve only the notion of natural numbers (i.e. you can formulate them in the language of the first order arithmetic), but which can be proved only by using more powerful concepts, for example, of set theory.

In other words: arithmetic contained in set theory is more powerful than the first order arithmetic. And in 1873, when Georg Cantor invented set theory, he extended also the concept of natural numbers used in mathematics. If the statement of Con(PA) seems "artificial" to prove this conclusion, see more striking examples in Section 6.5 and in Appendix 2. And finally, would you be surprised, if the twin prime conjecture appeared to be provable in ZFC, but not in PA - or not provable/disprovable at all?

Note. For a complete analysis of mathematical problems from around the incompleteness theorems - see Feferman [1960] and the chapter about incompleteness theorems written by C.Smorynski in Barwise [1977].

Back to title page.

Goedel, incompleteness theorem, liar paradox, liar, self reference, second, incompleteness, paradox, theorem, Rosser, Godel, Bernays