fGoedel, incompleteness theorem, liar paradox, Gödel, liar, self reference, second, incompleteness, paradox, theorem, Rosser, Godel, Bernays

Back to title page.

Left |
Adjust your browser window |
Right |

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)

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-- + -- * -- = -- ( -- ) -- ~
-- ∧ -- ∨ -- ⇒ -- 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.

**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_{1}(x): C(sub(x,
x)). Or more precisely (since we do not have in PA the function
symbol sub):

∀z (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. C_{1}(**k**), or

∀z (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 ∀z (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_{2}(x, y, z) - define the
value sub_{2}(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_{2}(x, y,
z)=n. After this, consider B(sub_{2}(x, x, y), sub_{2}(y,
x, y)) and C(sub_{2}(x, x, y), sub_{2}(y, x, y)),
etc.).

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

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 ∃yPRF(x, y) as a formula asserting "the formula number x can be proved in PA". By applying Self-Reference Lemma to the formula ~∃yPRF(x, y) we obtain Goedel's formula G such that

PA proves: G ⇔ ~∃yPRF(**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: ∃yPRF(**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 ∃yPRF(**G**, y) (see (1)). Intuitively, ∃yPRF(**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 ∃yPRF(**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: ∃yC(y),

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

This is not a "direct" contradiction. To have a
"direct" contradiction we must prove ∀y~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 ∀y~C(y)? I am not. And
Goedel was not, too. He was forced to introduce the notion of **ω-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 ω-inconsistent.

Therefore, in the second part of our investigation (assuming that PA can prove ~G), we could have established only the ω-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 ω-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 ω-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 ω-consistent.
Until this, we have proved only that PA **is not ****perfect**:
PA is either ω-inconsistent, or incomplete. I.e., when developing
PA, we will run inevitably either into a ω-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} ⇔ ~∃yPRF_{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 ω-inconsistent.

Therefore, Goedel's method allows to prove that a perfect axiom system of natural number arithmetic is impossible: any such system is either ω-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:

April 28, 1906 | Goedel, Kurt born |

September 7, 1930 | ... at a meeting in Königsberg...Gödel off-handedly announced his epic results during a round-table discussion. Only von Neumann immediately grasped their significance... (from a G.J.Chaitin's lecture, Buenos Aires, 1998). |

October 23, 1930 | Goedel presented the incompleteness theorem at a section meeting of the Vienna Academy of Sciences. |

November 17, 1930 | Goedel's famous 1931 paper received at "Monatshefte fuer Mathematik und Physik". |

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://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 1938 Goedel lived in the 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.

**Wir müssen wissen -- wir werden wissen!****David Hilbert's Radio Broadcast, **** Königsberg,
8 September 1930** (see audio record published by James T.Smith, and translations in 7 languages
published by Laurent Siebenmann).

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

In 1930, Gödel 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, Gödel 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 Gödel
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 Gödel’s article* Uber formal
unentscheidbare Sätze der *__Principia Mathematica__*
und verwandter Systeme." (*A fragment from Gö*del,
and his Incompleteness Theorem** *by Mark Wakim).

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 Gödel was a German spy, trying to signal ships and submarines in the bay..." (Peter Suber, "Kurt Gödel in Blue Hill").

See also exciting photos and biographical data in Kurt Gödel - Leben und Werk by Markus Krumpöck.

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 Gödel, 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 Gödel 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 *Gödel*'s Theorem in *1921* - had I been *Gödel."
(according to MacTutor
History of Mathematics archive).

**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 ⇔ ∃yPRF(**G**, y),

the theory PA+{ ∃yPRF(**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+{ ∃yC(y) }
is a consistent theory, yet for each natural number k: PA proves
~C(**k**). Imagine, you wish to invetisgate the theory PA+{
∃yC(y) }- why not? - it is "as consistent" as PA. In
this theory the axiom ∃yC(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+{ ∃yC(y) }, we are forced to admit the existence
of **non-standard natural numbers**.

**Exercise 5.7.** Prove in PA+{ ∃yC(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.

**Rosser's Version**

In 1936 Barkley Rosser improved the Goedel's proof. He removed the notion of ω-consistency from the formulation, replacing it by the (usual) consistency:

**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_{1}) If PA proves F, then T proves Tr(F).

Fu_{2}) T proves Tr(~F), iff T proves ~Tr(F).

Fu_{3}) If T proves Tr(F), and T proves Tr(F ⇒ G),
then T proves Tr(G).

**Note.** We will not need the condition Fu_{3}
in the proof below.

**Goedel's Incompleteness Theorem (extended version)**. If
T is a fundamental formal theory (only conditions Fu_{1},
Fu_{2} 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 these formulas:

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

∀t(PRF_{T}(x, t) ⇒ ∃z (z<t ∧
REF_{T}(x, z)).

Then there is a PA-formula R_{T} such that

PA proves: R_{T} ⇔ ∀t(PRF_{T}(**R**_{T},
t) ⇒ ∃z (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)

From (2) and (3) we obtain:

PA proves: ∃z (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_{2},
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: ~∃z (z<**k** ∧ REF_{T}(**R**_{T},
z)).

This contradicts (4), i.e. PA is inconsistent, and, by Fu_{1}
and Fu_{2}, so is T. Indeed, if PA proves B, and PA
proves ~B, then (by Fu_{1}) T proves Tr(B), and T proves
Tr(~B), i.e. (by Fu_{2}) T proves ~Tr(B).

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

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

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**).

Hence,

PA proves ~∃z (z<**k** ∧ PRF_{T}(**R**_{T},
z)). --------(6)

From (5) we have:

PA proves: ∀t(t>**k** ⇒ (PRF_{T}(**R**_{T},
t) ⇒ ∃z (z<t ∧ REF_{T}(**R**_{T},
z)))

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

PA proves: ∀t(PRF_{T}(**R**_{T},
t) ⇒ ∃z (z<t ∧ REF_{T}(**R**_{T},
z))).

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

**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 ω-consistent, and use the first
Albert's paradox to build two T-independent formulas. Could you
provide the "Rosserian" version of your proof?)

**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_{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 ∃yPRF_{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 ~∃yPRF_{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 ~∃yPRF1_{T}
(**0=1**, y), or:

~∃y [ 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 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 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_{1}) if PA proves F,
then T proves Tr(F); Fu_{2}) T proves Tr(~F), iff T
proves ~Tr(F); Fu_{3}) 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 ∃yPRF_{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_{1},
Fu_{2} and Fu_{3}, 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-Loeb derivability
conditions** hold for each pair of closed PA-formulas B, C:

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

**H**_{2}**:** T proves: Tr[PR_{T}(**B**))
⇒ PR_{T}(**PR**_{T}**(B)**)].

**H**_{3}**:** T proves: Tr[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. Hence, if H_{1},
H_{2}, H_{3} 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.Loeb:

**M.H.Loeb.** 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_{3}, T proves Tr(G_{T}), and, by H_{1},
T proves Tr(PR_{T}(**G**_{T})).

Since PA proves PR_{T}(**G**_{T}) ⇒ ~G_{T},
by Fu_{1}, T proves Tr(PR_{T}(**G**_{T}) ⇒ ~G_{T}).
Then, by Fu_{3}, T proves Tr(~G_{T}), and, by Fu_{2},
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_{1}, T proves Tr(PR_{T}(**G**_{T}) ⇒ ~G_{T}).
Then, by H_{1}, T proves Tr(PR_{T}(**PR**_{T}**(G**_{T}**) ⇒ ~G**_{T})).
By H_{3},

T proves: Tr[PR_{T}(**PR**_{T}**(G**_{T}**)**) ⇒ (PR_{T}(**PR**_{T}**(G**_{T}**) ⇒ ~G**_{T}) ⇒ PR_{T}(~**G**_{T})].

By H_{2}, 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_{1}
and Fu_{3} 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_{1} and Fu_{3} 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_{1}, T proves Tr( ~PR_{T}(**G**_{T}) ⇒ G_{T}).
Hence, by Exercise 3.5a, Fu_{1}
and Fu_{3} 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_{1}, T proves Tr(~G_{T} ⇒ (G_{T} ⇒ 0=1)).
Then, by H_{1}, T proves Tr(PR_{T}(**~G**_{T}** ⇒ (G**_{T}** ⇒ 0=1)**)).
By H_{3},

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_{1}
and Fu_{3} 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_{3},

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_{1}
and Fu_{3} 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 ω 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, Gödel, liar, self reference, second, incompleteness, paradox, theorem, Rosser, Godel, Bernays