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 C_{1}(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_{1}(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_{1}(x) itself! I.e., if k is the number of C_{1}(x),
let us denote by B the formula C_{1}(**k**). What is
the "assertion" of B? "If you take the formula
having the number k (i.e. the formula C_{1}(x)), and
substitute its number k for x, then you will obtain a formula (in
fact, the formula C_{1}(**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

prf_{T}(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 PRF_{T}(x,
y) expressing this predicate in PA. Let us apply 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 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 w_{0} 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 R_{T }that asserts some property of natural
numbers, yet if T proves R_{T} or T proves ~R_{T},
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:

F_{0}, F_{1}, F_{2}, F_{3},...
-------(1)

(Therefore, T proves Tr(**F**_{k}) for all
k, where Tr is the translation procedure from PA into T, see Section 3.2). 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 Q_{T} such that

PA proves: Q_{T} <-> At(PRF_{T}
(**Q**_{T}, t) -> Ez(z<t & REF_{T}
(**Q**_{T}, z)). --------(2)

Let us prove that as our target T-formula R_{T} we can
take Tr(**Q**_{T}) (Q_{T} is
PA-formula!).

1. Assume that T proves R_{T}. Then Q_{T}
appears in (1) as, for example, F_{k}. Hence,

PA proves: PRF_{T} (**Q**_{T},
**k**). --------(3)

From (2) and (3) we obtain:

PA proves: Ez(z<**k** & REF_{T}
(**Q**_{T}, z)). ---------(4)

If, indeed, ~Q_{T} appears in (1) as F_{m}
with m<k, then T proves ~R_{T} and T is inconsistent.
If not, then

PA proves: ~REF_{T} (**Q**_{T},
**0**)&~REF_{T} (**Q**_{T}, **1**)&...&~REF_{T}
(**Q**_{T}, **k-1**).

Hence,

PA proves ~Ez(z<**k** & REF_{T}
(**Q**_{T}, z)).

This contradicts (4), i.e. PA is inconsistent, and so is T.

2. Assume now that T proves ~R_{T}. Then ~Q_{T}
appears in (1) as, for example, F_{k}. Hence,

PA proves: REF_{T} (**Q**_{T},
**k**). -------(5)

If Q_{T} appears in (1) before ~Q_{T}, then T
proves R_{T}, and T is inconsistent. If Q_{T}
does not appear before ~Q_{T}, then

PA proves: ~PRF_{T} (**Q**_{T},
**0**)&~PRF_{T} (**Q**_{T}, **1**)&...&~PRF_{T}
(**Q**_{T}, **k-1**).

Hence,

PA proves ~Ez(z<**k** & PRF_{T}
(**Q**_{T}, z)). --------(6)

From (5) we have:

PA proves: At(t>**k** -> (PRF_{T}
(**Q**_{T}, t) -> Ez(z<t & REF_{T}
(**Q**_{T}, z)))

(if t>k, then we can simply take z=k). Add (6) to this, and you will have:

PA proves: At(PRF_{T} (**Q**_{T},
t) -> Ez(z<t & REF_{T} (**Q**_{T},
z))).

According to (2) this means that PA proves Q_{T}, and
T proves 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 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 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 R_{T} or
the formula ~R_{T} 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 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. 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:

F_{0}, F_{1}, F_{2}, F_{3},...
----------(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)
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.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 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 **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 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
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 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 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!

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 PRF_{T}(x, y) expressing the
predicate prf_{T}(x, y), let us consider 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 the origin of PR_{T}(x).
As Goedel's formula G_{T} we will use any formula having
the following property:

T proves: G_{T} <-> ~PR_{T}(**G**_{T}),

and the formula Con(T) we define as ~PR_{T} (**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:

**H**_{1}**:** If T proves B, then T
proves PR_{T}(**B**).

**H**_{2}**:** T proves: PR_{T}(**B**)
-> PR_{T}(**PR**_{T}**(B)**).

**H**_{3}**:** T proves: PR_{T} (**B**)
& PR_{T}(**B->C**) -> PR_{T}(**C**).

Conditions H_{1} and H_{2} say that T
"knows" that the formula PR_{T} (x)
"expresses" the notion T-provability. The condition H_{3}
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 G_{T},
then T is inconsistent. I.e. we will prove that

T proves: PR_{T}(**G**_{T})
-> PR_{T}(**0=1**). --------(3)

Since T proves: G_{T} <-> ~PR_{T}(**G**_{T}),
this will mean that T proves: Con(T)->G_{T}. Hence, if
T proves Con(T), then T proves G_{T}, and T is
inconsistent (the last conclusion needs H_{1}, having
this property of PR_{T} (x), we can repeat the first part
of Goedel's proof from the previous section).

So, let us prove (3). Let us assume PR_{T}(**G**_{T}).
By H_{2} we have:

T proves: PR_{T}(**G**_{T})
-> PR_{T}(**PR**_{T}**(G**_{T}**)**).

Hence, under our assumption we have PR_{T}(**PR**_{T}**(G**_{T}**)**).
Since T proves: PR_{T}(**G**_{T})->~G_{T},
by H_{1} we have:

T proves: PR_{T}(**PR**_{T}**(G**_{T}**)->~G**_{T}).

By H_{3} we have:

T proves: PR_{T}(**PR**_{T}**(G**_{T}**)**)
& PR_{T}(**PR**_{T}**(G**_{T}**)->~G**_{T})
-> PR_{T}(**~G**_{T}).

Hence, under our assumption we have PR_{T} (**~G**_{T}).
Together with the assumption PR_{T} (**G**_{T})
itself we can now use the logical axiom ~G_{T}->(G_{T}->0=1).
I.e. we can repeat the above manipulation with H_{3} to
obtain the formula PR_{T} (**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 PR1_{T}(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
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 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 PR_{T}(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.