Goedel, incompleteness theorem, Gödel, liar, paradox, self reference, second, theorem, Rosser, Godel, incompleteness
Back to title page.
Epimenides (VI century BC) was a Cretan angry with his fellow-citizens who suggested that "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?
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)2+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.
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).
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 C1(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 C1(x)? Literally, the following: "Take the number x, restore from x the formula Fx(u, v, w,...) having this number, substitute x (i.e. the number of Fx itself) for all free variables of Fx, then you will obtain the formula Fx (x, x, x,...) that possess the property C".
Second step. Let us try to apply this operation to the formula C1(x) itself! I.e., if k is the number of C1(x), let us denote by B the formula C1(k). What is the "assertion" of B? "If you take the formula having the number k (i.e. the formula C1(x)), and substitute its number k for x, then you will obtain a formula (in fact, the formula C1(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. C1(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 (A.Mostowski, 1961). 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.
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 where the formula number x is proved".
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 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?
I am sorry, 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
prfT(x, y) = "y is a T-proof-number where the formula number x is proved"
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 PRFT(x, y) expressing this predicate in PA. Let us apply Self Reference lemma, and we will have a closed formula GT such that
PA proves: GT <-> ~EyPRFT (GT, y),
i.e. GT "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 GT, then T is inconsistent.
b) If T proves ~GT, 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 numbers problems.
Kurt Goedel was born on April 28, 1906. He presented the above incompleteness theorem on October 23, 1930 at a section meeting of the Vienna Academy of Sciences. The corresponding paper was received on November 17, and was published in 1931.
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 also "Akademie der Wissenschaften in Wien, Mathematisch-Naturwissenschaftliche Klasse, Anzeiger", 1930, N 76, pp.214-215). See online English translation at http://www.ddc.net/ygg/etext/godel/index.htm.
(See also English translations in Davis [1965] or Heijenoort [1967], and online comments at http://thoralf2.uwaterloo.ca/htdocs/scav/goedel/goedel.html).
Since 1938 Goedel lived in U.S., he died on January 14, 1978.
About Goedel's contribution to Einstein's general relativity theory see http://www.ettnet.se/~egils/essay/essay.html.
Goedel in the U.S., 1942: "...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 Gödel was a German spy, trying to signal ships and submarines in the bay..." (Peter Suber, "Kurt Goedel in Blue Hill").
See also a collection of Goedel web-sites at www.geometry.net.
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)
Exercise 5.7. Return to the paradoxes stated by Albert of Saxony (Section 5.1). What kind of incompleteness theorems could you derive by modeling these paradoxes in PA? You may find helpful the result of the Exercise 5.4.
Non-standard arithmetic
We know that if PA is consistent, then 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 develop the theory PA+{ EyC(y) }that is "as consistent" as PA. In this theory its axiom EyC(y) says that there is a number y that 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 have the property C. Hence, we are forced to admit the existence of non-standard natural numbers (when working in the theory PA+{ EyC(y) }).
Exercise 5.8. Prove in PA+{ EyC(y) }that there is some minimum number w0 having the property C. On the other hand, prove that there is no minimum non-standard number.
In 1936 Barkley Rosser improved the Goedel's proof. He removed the notion of w-consistency from the formulation.
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 a fundamental formal theory, then one can build a closed formula RT that asserts some property of natural numbers, yet if T proves RT or T proves ~RT, then T is inconsistent.
Note. This statement contains two improvements of our previous version of the incompleteness theorem. The first one is due to Rosser (w-consistency removed). The second one is from the original Goedel's proof. Our previous version was 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. Still, as is stated above, the incompleteness theorem can be proved for fundamental theories having arbitrary languages.
Proof. We know from the Exercise 1.4 that any particular fundamental theory T can prove only an effectively enumerable set of PA-formulas. Let us construct a Turing machine, which enumerates these formulas:
F0, F1, F2, F3,... -------(1)
(Therefore, T proves Tr(Fk) for all k, where Tr is the translation procedure from PA into T, see Section 3.2). The following predicate is computable:
prfT(x, t) - "the formula number x appears in (1) as Ft".
Let the formula PRFT(x, y) express this predicate in PA. The following predicate is computable, too (ref - refute):
refT(x, t) - "the negation of the formula number x appears in (1) as Ft".
Let the formula REFT(x, y) express this predicate in PA.
Rosser's key idea was the following. Goedel's formula GT asserts "I cannot be proved in T". Let us take, instead, a formula RT 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(PRFT (x, t) -> Ez(z<t & REFT (x, z)).
Then there is a PA-formula QT such that
PA proves: QT <-> At(PRFT (QT, t) -> Ez(z<t & REFT (QT, z)). --------(2)
Let us prove that as our target T-formula RT we can take Tr(QT) (QT is PA-formula!).
1. Assume that T proves RT. Then QT appears in (1) as, for example, Fk. Hence,
PA proves: PRFT (QT, k). --------(3)
From (2) and (3) we obtain:
PA proves: Ez(z<k & REFT (QT, z)). ---------(4)
If, indeed, ~QT appears in (1) as Fm with m<k, then T proves ~RT and T is inconsistent. If not, then
PA proves: ~REFT (QT, 0)&~REFT (QT, 1)&...&~REFT (QT, k-1).
Hence,
PA proves ~Ez(z<k & REFT (QT, z)).
This contradicts (4), i.e. PA is inconsistent, and so is T.
2. Assume now that T proves ~RT. Then ~QT appears in (1) as, for example, Fk. Hence,
PA proves: REFT (QT, k). -------(5)
If QT appears in (1) before ~QT, then T proves RT, and T is inconsistent. If QT does not appear before ~QT, then
PA proves: ~PRFT (QT, 0)&~PRFT (QT, 1)&...&~PRFT (QT, k-1).
Hence,
PA proves ~Ez(z<k & PRFT (QT, z)). --------(6)
From (5) we have:
PA proves: At(t>k -> (PRFT (QT, t) -> Ez(z<t & REFT (QT, z)))
(if t>k, then we can simply take z=k). Add (6) to this, and you will have:
PA proves: At(PRFT (QT, t) -> Ez(z<t & REFT (QT, z))).
According to (2) this means that PA proves QT, and T proves RT, 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 to solve 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 to solve 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 has proved that his arithmetic is not fundamental.
Pure mathematical contents of incompleteness theorems (without any attempt to "judge") 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 builds a closed PA-formula RT. As a closed PA-formula, RT asserts some property of the natural number system.
Algorithm 2. Given a T-proof of the formula RT or the formula ~RT this algorithm builds 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 RT. 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. 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 of reasoning as reliable as the ones containing in the first order arithmetic (i.e. PA). Hence, to prove 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:
F0, F1, F2, F3,... ----------(1)
From a Turing machine program generating (1) we derived a PA-formula PRFT (x, y) expressing in PA the predicate
prfT (x, y) = "the formula number x appears in (1) as Fy".
Then the formula EyPRFT (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 ~EyPRFT (0=1, y) 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 PRFT (x, y). (I got to know about the experiment described below from the Appendix 1 written by A.Yesenin-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 PRFT (x, y) let us introduce another formula PRF1T (x, y):
PRFT (x, y) & ~PRFT (0=1, y).
If T is consistent, then 0=1 cannot be proved in T, hence, for all k:
PA proves: ~PRFT ((0=1, k).
And hence, PRF1T (x, y) - like as PRFT(x, y) - expresses in PA the predicate prfT (x, y). Now let us build the corresponding formula Con1(T) as ~EyPRF1T (0=1, y), or:
~Ey(PRFT (0=1, y)&~PRFT (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 PRF1T (x, y) expresses the predicate prfT (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 watch 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 PRFT (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 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 GT cannot be proved in T".
And GT says exactly that it cannot be proved in T. Hence, "if Con(T), then GT". Or, formally:
Con(T) -> GT.
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) -> GT. --------(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 than 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 GT. If T is a fundamental theory, then T proves all theorems of PA, and hence, T also proves GT. From Goedel's incompleteness theorem we know that, if T proves GT, then T is inconsistent. Therefore, if PA proves Con(T), then T is inconsistent! And, if PA proves Con(PA), then PA is inconsistent!
This conclusion was first formulated in the same famous 1931 paper by Kurt Goedel, and now it is called Goedel's second theorem.
Goedel's second theorem shows that Hilbert's program (see Section 1.5) 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 rebuild the foundations of mathematics (see Poincare [1908], Volume II, Chapter IV, Section V):
Do not try to justify 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 be successful, you will prove that PA is inconsistent!
The reaction by David Hilbert to the failure of his program was quite different from that by Dedekind, Frege and Cantor. The following elegant version of Goedel's second theorem results from a profound analysis of Goedel's proof performed by Hilbert and Paul Bernays (see Hilbert, Bernays [1934]).
Instead of the formula PRFT(x, y) expressing the predicate prfT(x, y), let us consider the formula EyPRFT (x, y). Let us denote it by PRT (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 the origin of PRT(x). As Goedel's formula GT we will use any formula having the following property:
T proves: GT <-> ~PRT(GT),
and the formula Con(T) we define as ~PRT (0=1).
Let us say that the theory T "knows", that Con(T) asserts the consistency of T, iff the following three Hilbert-Bernays conditions hold for each pair of PA-formulas B, C:
H1: If T proves B, then T proves PRT(B).
H2: T proves: PRT(B) -> PRT(PRT(B)).
H3: T proves: PRT (B) & PRT(B->C) -> PRT(C).
Conditions H1 and H2 say that T "knows" that the formula PRT (x) "expresses" the notion T-provability. The condition H3 says that T "knows" that the set of (arithmetical) theorems of T is closed under MODUS PONENS.
Goedel's Second Theorem. If a fundamental formal theory T "knows" that the formula Con(T) asserts the consistency of T, then either T is inconsistent, or Con(T) cannot be proved in T.
Proof. Let us formalize in T the proof of the (part one of) Goedel's incompleteness theorem: if T proves GT, then T is inconsistent. I.e. we will prove that
T proves: PRT(GT) -> PRT(0=1). --------(3)
Since T proves: GT <-> ~PRT(GT), this will mean that T proves: Con(T)->GT. Hence, if T proves Con(T), then T proves GT, and T is inconsistent (the last conclusion needs H1, having this property of PRT (x), we can repeat the first part of Goedel's proof from the previous section).
So, let us prove (3). Let us assume PRT(GT). By H2 we have:
T proves: PRT(GT) -> PRT(PRT(GT)).
Hence, under our assumption we have PRT(PRT(GT)). Since T proves: PRT(GT)->~GT, by H1 we have:
T proves: PRT(PRT(GT)->~GT).
By H3 we have:
T proves: PRT(PRT(GT)) & PRT(PRT(GT)->~GT) -> PRT(~GT).
Hence, under our assumption we have PRT (~GT). Together with the assumption PRT (GT) itself we can now use the logical axiom ~GT->(GT->0=1). I.e. we can repeat the above manipulation with H3 to obtain the formula PRT (0=1). Hence, by the Deduction theorem we have (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 conditions were true for the corresponding formula PR1T(x), then according to Goedel's second theorem theory T would be inconsistent Hence, if T is consistent, then Hilbert-Bernays conditions do not hold for PR1T(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 conditions hold for all formulas Con(T) obtained in a "natural" way, i.e. by 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 inconsistent, or it cannot prove Con(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? They are not able even to formulate their own consistency problem. Either their languages do not allow to write formulas like PRT(x) and Con(T), or their axioms do not allow to prove Hilbert-Bernays conditions.
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 ZF, but not in PA - or not provable at all?
Note. For an in-depth, best and final analysis of mathematical problems from around the incompleteness theorems - see Feferman [1960] and the chapter about incompleteness theorems in Barwise [1977].
Goedel, incompleteness theorem, Gödel, liar, paradox, self reference, second, theorem, Rosser, Godel, incompleteness
Back to title page.