Goedel, incompleteness theorem, Gödel, theorem, incompleteness, significance, size of proofs, Loeb, Kronecker, Löb, lieber Gott

Back to title page.

Some people derive from incompleteness theorems the thesis about superiority of the "alive, informal, creative, human thinking" over axiomatic theories. Or, about the impossibility to cover "all the riches of the informal mathematics" by a stable set of axioms. I could agree with this, when the above-mentioned "superiority" would not be understood as the ability of the "informal thinking" to find out unmistakably (i.e. on the first trial) some "true" assertions that cannot be proved in a given axiomatic theory. Some of the enthusiasts of this opinion draw the following picture.

Let us consider any formal theory T that contains a
full-fledged concept of natural numbers (i.e. - in my terms - a
fundamental theory). Let us build for T Goedel's formula G_{T}
asserting "I am not provable in T". Goedel proved that,
indeed, G_{T} cannot be proved in T, i.e Goedel proved
that G_{T} is a true formula (and - as a formula of PA -
it is talking about properties of natural numbers). Therefore, if
we choose an arbitrary formal theory T, then Kurt Goedel - by
using his "informal, creative thinking" - proves
immediately some assertion G_{T} about properties of
natural numbers, which cannot be proved in T. Hence, none of
formal theories can express 100% of the "informal,
human" concept of natural numbers. If you fix some
particular formal theory, my "creative mind" will **unmistakably**
find out a true assertion G_{T} overcoming all what can
be proved in T.

The analysis of Goedel's proof presented in the previous
section forces us to revise this picture. One can prove that G_{T}
is a true formula (i.e. that G_{T} cannot be proved in T)
only by **postulating consistency** of T. Indeed, if G_{T}
is proved to be true, then also consistency of T is proved (G_{T}
asserts its own unprovability, and the unprovability of at least
one formula means consistency of T). Hence, if we do not know,
whether T is consistent or not, we can say nothing about the
truth or falsity of G_{T}. What could think the
enthusiasts of the above picture about the consistency problem?

First of all, they cannot think, that **any** formal theory
is consistent. Just add to PA the formula 0=1 as an axiom, and
you will obtain an example of an inconsistent theory. Of course,
such artificial examples cannot be taken seriously. Still, the
following fact has to be taken absolutely seriously: there is no
algorithm that could detect exploring the axioms and rules of a
formal theory, is this theory consistent or not.

**Exercise 6.1.** Let us assume that PA is consistent. Show
(using the techniques of Section 6.3) that
there is no algorithm detecting for a given closed formula F,
whether the theory PA+F is consistent or not.

Hence, the consistency problem cannot be solved mechanically,
by applying some uniform method to all theories. Serious theories
are complicated enough to require **individual investigation**
of this problem.

And finally, we must return to the history of those mathematical theories which were considered as "absolutely reliable" by their creators, but which were proved inconsistent some time later.

The first of these unhappy theories was the first serious formal system of mathematics developed by Gottlob Frege.

**G. Frege. **Die Grundlagen der Arithmetik. Eine
logisch-mathematische Untersuchung ueber den Begriff der Zahl.
1884, Breslau, 119 pp.

**G. Frege. **Grundgesetze der Arithmetik,
begriffsschriftlich abgeleitet. Jena, Vol. I, 1893, 254 pp., Vol.
II, 1903, 265 pp. (see also online comments at http://thoralf2.uwaterloo.ca/htdocs/scav/frege/frege.html)

See also the online paper Frege's Logic, Theorem, and Foundations for Arithmetic in the Stanford Encyclopedia of Philosophy.

In 1902, when the second (final!) volume of Frege's book was ready to print, B.Russell established that from Frege's principles a contradiction can be derived (see Russell's paradox in Section 2.2). Frege died in 1925, yet after 1902 he published nothing comparable with his outstanding works of the previous period. Russell's paradox was for him a dreadful blow because of the contrast between the 20 years long impression of absolute reliability of his formal system, and the suddenly following "absolutely trivial" inference of a contradiction. Frege considered the situation as his personal failure. Was it really? Even today, reading Frege's book without prejudice, you have the same impression of absolute reliability. Hence, the Russell's paradox was not Frege's personal failure, it was failure of the entire old way of mathematical thinking.

Some years before Frege a similar unhappy situation appeared in another excellent work of XIX century - in the set theory created by Georg Cantor. Read Cantor's works without prejudice, and you will get again the impression of absolute reliability (if you do not read in German, please, read once more Section 2.2). Cantor developed the principles of the old mathematical thinking up to their natural logical limits - the concept of static infinite sets. Leider, in 1895 Cantor established himself that from his principles a contradiction can be derived.

Since the lifetime of Frege and Cantor formal mathematical theories have been improved significantly. No contradictions have been found so far in the improved theories. Still, from the unhappy experience of these extraordinary people we must learn at least the following: our "feeling", our impression of absolute reliability of our premises, no matter how many people share this "feeling", cannot serve as an absolute warranty against contradictions.

Truth or falsity of the assertions proposed so far as
"true statements" unprovable in a particular formal
theory depends on the consistency of this theory. Hence, we
cannot speak here about a general method that allows to obtain
unmistakably "true statements" that overcome a given
formal theory. What, if the theory T that we intend to overcome
will be proved inconsistent? Then, Goedel's formula G_{T}
will be false. And this we must call a "superior true
statement"?

Perhaps, the best way to demonstrate the absurdity of the position I'm trying to criticize may be the following "syllogism":

a) To overcome "a la Goedel" some formal theory T,
we must prove the formula G_{T}.

b) To prove the formula G_{T}, we must prove
consistency of T.

c) To prove consistency of T, we must use postulates from outside of T (Goedel's second theorem).

Hence, to overcome "a la Goedel" some formal theory T, we must use postulates from outside of T. Is this absolutely trivial or not?

If we are not able to prove the consistency of our favorite
theory, yet our feeling says that "this is the case",
then we may try to adopt the consistency conjecture as an
additional axiom, and try to draw consequences from this axiom.
This approach is not completely novel for mathematics. For
example, in number theory the consequences of Riemann's
hypothesis are studied etc. Note, however, that we are talking
here about **hypotheses**. The consistency conjecture of our
favorite theory is no more than a hypothesis, and adopting this
hypothesis as an axiom is **postulating**, i.e. adoption
without sufficient arguments. Drawing consequences from a
hypothesis we may come to contradictions, and then we will be
forced to reject it.

Our final conclusion may be formulated as follows: incompleteness theorems do not yield a general method that allowed to overcome unmistakably (i.e. on the first trial) any given formal theory. It seems that such a general method does not exist at all: serious theories are too complicated, hence, to overcome a particular serious theory we must, perhaps, invent a particular method.

The true methodological significance of incompleteness
theorems is completely different: **any fundamental theory is
either inconsistent, or it is insufficient to solve some of its
problems.** We know already that the methods developed by
Goedel and his followers do not allow deciding is a given theory
inconsistent or incomplete. Hence, it would be more exactly to
say not "incompleteness theorems", but rather
"imperfectness theorems". A fundamental theory cannot
be perfect - it is either inconsistent, or it is insufficient to
solve some of its problems.

An imperfect theory must be and can be improved. Contradictions can be removed by improving axioms. The problems that are proved (or are suspected) to be undecidable we can try to solve by adopting additional powerful (maybe, unreliable!) axioms.

From a methodological point of view formal theories are models
of **stable (self-contained) systems of reasoning**. Hence, we
can reformulate our main conclusion as follows: any fundamental
stable (self-contained) system of reasoning is either
inconsistent or there are some problems that cannot be solved by
using this (stable, self-contained!) system. **The crucial
evidence of inherent imperfectness of any stable (self-contained)
system of reasoning - here is the true methodological
significance of Goedel's results.** Mathematical theories
cannot be perfect **because** they are stable
(self-contained)! Only relatively weak (i.e. non-fundamental)
theories can be both consistent and complete. Powerful (i.e.
fundamental) theories inevitably are either inconsistent, or
incomplete.

**Note. **Do not conclude from this that mathematics must
turn to variable (i.e. non-self-contained) systems of reasoning -
then this will be no mathematics!

**Note.** In the so-called model theory (a branch of
mathematical logic, see Appendix 1)
theories are defined as arbitrary sets of formulas (sets of
theorems). This is a very abstract point of view to be useful in
discussions about foundations of mathematics. A real theory
should be defined as a sufficiently definite system of reasoning
(and formal theories are models of absolutely definite, i.e.
stable, self-contained systems of reasoning). The set of theorems
is only a secondary aspect of a real theory: it is the set of
assertions that can be proved by using the axioms and rules of
theory. If theories are viewed as sets of theorems, then
inconsistent theories seem to be "empty" (in these
theories all formulas are provable, i.e. they do not make
difference between true and false formulas). And, when we manage
to remove inconsistencies by improving axioms of our theory, then
have we "improved" an empty set of theorems? If
theories are viewed as systems of reasoning, then inconsistent
theories simply are some kind of imperfect systems that can be
improved.

Paul Levy discussed the possibility of the double incompleteness phenomenon in 1926 (see Levy [1926]). He proposed the following conjecture:

"... il est possible que le theoreme de Fermat soit indemontrable, mais on ne demontrera jamais qu'il est indemontrable.Au contraire, il n'est pas absurde d'imaginer qu'on demontre qu'on ne soura jamais si la constante d'Euler est algebrique ou transcendente."

The undecidability of Rosser's formula R_{T} in theory
T could be derived from the consistency conjecture of T.
Otherwise, Rosser's judgement remains within PA (first order
arithmetic). Hence, the proof of undecidability of R_{T}
can be formalized in the theory PA+Con(T), i.e. in the theory PA
plus the consistency conjecture of T. A theory that is used to
discuss properties of some other theory is called a **metatheory**.
Hence, the undecidability of R_{T} can be established in
the metatheory PA+Con(T). Perhaps, this metatheory can establish
also T-undecidability of some other formulas. Still, maybe, there
are formulas, whose undecidability cannot be established in
PA+Con(T), i.e. the consistency conjecture of T may appear
insufficient for this purpose?

The answer can be obtained by modeling the Extended Liar's paradox (see Section 5.1):

**q: (q is false) or (q is undecidable).**

All the three possible alternatives (q is true, q is false, q is undecidable) lead to contradictions. If theory T is discussed in metatheory M, then we can try to obtain a formula H, which will assert that

"H is refutable in T, or M proves T-undecidability of H".

This can be done, indeed, and as a result, we would obtain the first ("Goedelian") version of the double incompleteness theorem: if theories T, M are both w-consistent, then the formula H is undecidable it T, yet this cannot be established in M (see Podnieks [1975]). Hence the term "double incompleteness theorem". We will prove here the extended ("Rosserian") version of this theorem (Podnieks [1976]).

First, we must define the relationship "M is metatheory
for T" precisely. Let T and M be two fundamental theories,
i.e. theories containing first order arithmetic PA. Let us denote
by (N_{T}, Tr_{T}) and (N_{M}, Tr_{M})
the interpretations of PA in T and M respectively (see Section 3.2). Let us say that M **is a
metatheory of** T, if we have PA-formulas PR_{T}(x) and
RF_{T}(x) such that for all PA-formulas F:

a) If T proves Tr_{T}(F), then M proves Tr_{M}(PR_{T}(**F**)).

b) If T proves Tr_{T}(~F), then M proves Tr_{M}(RF_{T}(**F**)).

Thus, the theory M "knows" something about the arithmetical statements that can be proved or refuted in T. For simplicity of notation let us write simply

T proves F, T proves ~F, M proves PR_{T}(**F**),
M proves RF_{T}(**F**)

instead of

T proves Tr_{T}(F), M proves Tr_{M}(PR_{T}(**F**))
etc.

**Double Incompleteness Theorem.** Let T and M be two
fundamental theories, and M is metatheory for T. Then there is a
PA-formula H such that if T and M are both consistent, then H is
undecidable in T, yet M cannot prove neither ~PR_{T}(**H**),
nor ~RF_{T}(**H**) (i.e. the metatheory M cannot prove
neither the T-unprovability, nor the T-unrefutability of the
formula H).

**Proof.** Since the set of all theorems of a formal theory
is effectively enumerable, let an appropriate Turing machine
enumerate all arithmetical theorems of T and M:

(T, A_{0}), (M, A_{1}), (T, A_{2}),
(M, A_{3}), ... -----------(1)

The appearance of the pair (T, A) means that T proves A, the appearance of (M, A) - that M proves A. Our aim is to obtain a formula H such that none of the following four assertions can hold:

T proves H, T proves ~H, M proves ~PR_{T}(**H**),
M proves ~RF_{T}(**H**). ----------(2)

Therefore, let us call a formula Q **positive**, if in the
enumeration (1) one of the pairs (T, Q) or (M. ~RF_{T}(**Q**))
appears first, and let us call Q **negative**, if first
appears (T, ~Q) or (M, ~PR_{T}(**Q**)). Our target
formula H must be neither positive, nor negative. The enumeration
index of the first pair appeared we call (respectively) the
positive or negative index of the formula Q. The following two
predicates are effectively solvable:

a(x,y) = " y is the positive index of the formula number x",

b(x,y) = " y is the negative index of the formula number x".

Let formulas A(x,y), B(x, y) express these predicates in PA. Now, following the Rosser's proof method, let us take the formula

Ay (A(x,y) -> Ez<y B(x,z))

and let us apply the self-referential lemma. In this way we obtain a PA-formula H such that

PA proves: H <-> Ay (A(**H**, y) ->
Ez<y B(**H**,z)),

i.e. H asserts: "if I am positive, then I am negative, and my negative index is less than my positive index".

**Exercise 6.2.** Following the Rosser's proof (see Section 5.3), derive from either of the
assertions (2) a contradiction in T or M.

This completes the proof of the double incompleteness theorem.

If we take M = PA+Con(T), i.e. if we discuss a theory T by means of PA using only the consistency conjecture of T, then there are T-undecidable formulas, whose undecidability cannot be proved by using this conjecture only. To prove the undecidability of these formulas (obtained from the double incompleteness theorem) the conjecture Con(PA+Con(T)) is needed. This is the answer to the question posed at the beginning of this section.

The incompleteness phenomenon allows a new method of
developing mathematical theories. If in some theory T we are not
able to prove or disprove an assertion F, then we may try to
adopt F (or ~F) as an additional axiom. However, this approach is
somewhat dangerous: maybe, in the **future** the assertion F
will be proved (then our attempt to develop the theory T+~F will
cause unwelcome aftereffects) or disproved (then similar
aftereffects will cause our attempt to develop T+F). Therefore,
it would be nice, before adopting a new axiom F, to obtain some
guarantee that this way does not lead to contradictions. I.e. it
would be nice to prove the consistency of our intended new theory
T+F. From Goedel's second theorem we know that an **absolute **consistency
proof is impossible. Such proof must involve assertions from
outside of T+F, i.e. assertions that may be even more dangerous
than F itself. Hence, we cannot obtain an absolute guarantee.
Still, it is possible to obtain a **relative guarantee** - we
can try to prove that the adoption of the new axiom F does not
generate "new" contradictions (except the
"old" ones which - maybe - are already contained in our
initial theory T).

The possibility of this approach was realized long before Goedel - at the beginning of the XIX century, when the non-Euclidean geometry was invented. Let us denote: A - the so-called absolute geometry, P - Euclid's fifth postulate. Then A+P is the classical Euclidean geometry. In 1820's J.Bolyai and N.Lobachevsky established that developing the theory A+~P for a long time no contradictions can be obtained. And in 1871 F. Klein proved that

Con(A+P) -> Con(A+~P),

i.e. that we can develop non-Euclidian
geometry safely, if the safety of developing A+P (Euclidean
geometry) is not questioned. Thus the possiblity of developing **alternative**
mathematical theories was discovered (or, invented?).

The "normal" way of doing mathematics is deriving consequences from a stable list of axioms. Incompleteness theorems were additional evidence that no stable list of axioms can be sufficient to solve all problems that can appear in mathematical theories. Since incompleteness is inevitable, one could adopt a more flexible way of doing mathematics: if, doing a theory T we cannot prove the assertion F, let us try to prove that

Con(T) -> Con(T+F),

then, adopt F as an additional axiom, and continue developing
T+F (instead of T) safely. Thus, instead of the old **principle
of stable axioms** a new **principle of stable safety**
could be adopted.

The double incompleteness theorem shows that the principle of
stable safety also is incomplete. Really, by taking M = T+Con(T)
we obtain from this theorem a formula H that is undecidable in T,
yet in M we cannot prove neither ~PR_{T}(**H**) (i.e.
consistency of T+~H), nor ~RF_{T} (**H**) (i.e.
consistency of T+H). Thus, neither of the safety conditions

Con(T) -> Con(T+F),

Con(T) -> Con(T+~F)

can be proved within theory T. The axiom of determinateness (AD, see Section 2.4) could be an example of such a dangerous postulate: perhaps,

Con(ZF) -> Con(ZF+AD)

will never be proved in ZF? This is an open problem. However, one can prove in PA that

Con(ZF) -> Con(ZF+ ~AD).

**Open problem?** All the well-known "powerful"
set-theoretic hypotheses H have the following property:

PA proves: Con(ZFC) -> Con(ZFC+ ~H),

yet Con(ZFC) -> Con(ZFC+H) cannot be proved (sometimes, even in ZFC+H).

Or, the same property with ZF instead of ZFC. Among the set-theoretic hypotheses considered as interesting ones, is there some hypothesis H such that neither

Con(ZF) -> Con(ZF+H) (or Con(ZFC+H)),

nor

Con(ZF) -> Con(ZF+ not H) (or Con(ZFC+ ~H))

can be proved (in PA, in ZF etc.)?

In mathematics all theorems are proved by using a stable list of axioms (for example, the axioms of ZFC). Sometimes this thesis is put as follows: all the results you can obtain in mathematics are already contained in axioms. Hence, doing mathematics, "nothing new" can appear?

Really? If you define as "new" only those principles of reasoning that you cannot justify by referring to commonly acknowledged axioms, then the above thesis becomes a truism (i.e. it contains "nothing new"). And then the only "new" things described in this book, are those that cannot be derived from the axioms of ZFC (or ZF): continuum hypothesis, axiom of constructibility and axiom of determinateness!

Q.E.D., if you agree that the distinctive character of a mathematical theory is a stable (i.e. self-contained) system of basic principles. All theorems of set theory really are (in a sense) "contained" in the axioms of ZFC. As we know, the set of all theorems of ZFC is effectively enumerable. I.e. you can write a computer program that will work printing out the (infinite) sequence of all theorems of ZFC:

F_{0}, F_{1}, F_{2}, F_{3},
F_{4}, ...

Thus, any theorem of ZFC will be printed out by this program - maybe, this will happen within the next 100 years, maybe, some time later. Still, does it mean that when doing set theory "nothing new" can appear?

Imagine, you are solving some mathematical problem, and you are arrived at a hypothesis H, and you would like to know, is this hypothesis "true" (i.e. provable in ZFC) or "false" (i.e. disprovable in ZFC)? Could you use for this purpose the above computer program? Having bought enough beer we could sit very long by the paper tape of our computer waiting for the formula H printed (this will mean that ZFC proves H) or the formula ~H printed (this will mean that ZFC disproves H). Still, as we know from incompleteness theorems, formula H may be undecidable for ZFC - in this case neither H, nor ~H will be printed ad infinitum, and we will never be able to decide - wait another 100 years or drop waiting immediately.

Hence, the obvious enumerating program for ZFC does not help
doing mathematics. What would really help, is called **decision
procedures**. We could say, that mathematics is (in a sense) a
purely "mechanical art", only when we had an algorithm
determining for each closed formula H, whether

a) ZFC proves H, or

b) ZFC refutes H, or

c) H is undecidable for ZFC.

**Exercise 6.3.** Traditionally, **decision procedure**
for some theory T is defined as an algorithm determining is an
arbitrary closed formula provable in T or not. Verify that a
decision procedure exists, iff there is an algorithm determining
membership of formulas in classes a), b), c).

If ZFC would be inconsistent, then all formulas would be provable in ZFC, i.e. in this case the classes a) and b) would coincide, and the class c) would be empty. Hence, after a contradiction has been found in some theory, it becomes a purely "mechanical art" (in the sense of the above definition).

Thus, we can discuss seriously the existence of an algorithm separating the classes a), b) and c) for some theory T only under the assumption that this theory is consistent. So, let T be any consistent fundamental theory (see Section 3.2). We will prove that there is no algorithm determining whether an arbitrary closed formula is provable in T, refutable in T, or undecidable for T.

We will prove this in a somewhat stronger form. Let us say
that the class of all T-provable formulas is **effectively
separable** from the class of all T-refutable formulas, iff
there is an algorithm A transforming each T-formula into 0 or 1
in such a way that:

a) If T proves F, then the algorithm A returns 1.

b) If T refutes F, then the algorithm A returns 0.

c) If F is undecidable for T, then A returns 0 or 1.

Thus, the algorithm A does not recognize exactly neither T-provable, nor T-refutable formulas, yet it knows how to "separate" the first class from the second one. We will prove that even such algorithm does not exist, if T is a consistent fundamental theory. Moreover, we will prove that the class of all T-provable PA formulas (i.e. first order arithmetical formulas) is not effectively separable from the class of all T-refutable PA formulas. As you know, the class of all T-provable formulas, and the class of all T-refutable formulas both are effectively enumerable. It follows from our theorem that neither of these classes can be effectively decidable, and that the class of all T-undecidable formulas is not even effectively enumerable.

**Unsolvability Theorem.** Let T be a consistent
fundamental theory. Then the class of all T-provable PA formulas
is not effectively separable from the class of all T-refutable PA
formulas. Hence, there is no decision procedure for T.

**Note.** The Unsolvability theorem was proved in the
famous 1936 papers by Church and Turing (see Church [1936] and Turing [1936], and improved by
Rosser (see Rosser [1936]).

**Proof.** Let us assume the opposite - that there is an
algorithm separating T-provable PA formulas from T-refutable PA
formulas. Then there is a Turing machine M computing the
following function s(x):

1) If n is a Goedel number (see Section 5.2) of (the T-translation of) a T-provable PA formula, then s(n)=1.

2) If n is a Goedel number of (the T-translation of) a T-refutable PA formula, then s(n)=0.

3) Otherwise, s(n)=0 or s(n)=1.

Let the formulas C_{0}(x, t), C_{1}(x, t)
express in PA the following (efectively decidable) predicates:

"the machine M working on the argument value x stops after t steps and issues the result 0",

"the machine M working on the argument value x stops after t steps and issues the result 1".

Following Rosser's idea from Section 5.3 we can obtain from the Self-reference lemma a closed formula E such that

PA proves: E <-> At(C_{1}(**E**,
t) -> (Ez<t)C_{0}(**E**, z)).

**Exercise 6.4.** Following the Rosser's proof (Section 5.3) show that, if s(**E**)=1,
then PA proves ~E, and if s(**E**)=0, then PA proves E.

Since T proves all theorems of PA, and T is consistent, this
means that, if s(**E**)=1, then s(**E**)=0, and if s(**E**)=0,
then s(**E**)=1. This is impossible. Hence, algorithms
separating T-provable PA formulas from T-refutable PA formulas do
not exist. Q.E.D.

The Unsolvability theorem has important "practical"
consequences. Imagine, you are solving some mathematical problem,
and you are arrived at a hypothesis H, and you would like to
know, is this hypothesis "true" (i.e. provable in the
theory T you are working in) or "false" (i.e.
disprovable in T)? If T is a consistent fundamental theory, then
there is no decision procedure for T, i.e. there is no **general
method **for deciding is H provable in T or not. Hence, to
solve your problem you must find some **specific features** of
your hypothesis H that are making it provable, disprovable (or
undecidable?) in your theory T. Since there is no general method
of doing this, your theory T should be qualified as an
"extremely creative environment". If you will succeed
in finding the specific features of the hypothesis H that make it
true, it will not mean that your ideas will be applicable to your
next hypothesis H2 etc.

**Note.** This part of our "creativity
philosophy" is applicable only to consistent theories.
Still, maybe, our theory is inconsistent? **Finding a
contradiction in a serious mathematical theory should be
qualified as a first class creative act!** See, for example,
the story of Russell's paradox in Section
2.2. And as we know from the Exercise 6.2, there is no
general method for deciding is a given theory consistent or not.
Hence, mathematics is "creative on both sides".

**Note.** The mere existence of a decision procedure does
not mean automatically that your theory becomes a purely
"mechanical art". Return, for example, to Presburger
arithmetic in Section 3.1. If any
decision procedure of your theory necessarily takes 2**2**Cn
steps ('**' stands for exponentiation) to decide about formulas
consisting of n characters, then - from a practical point of view
- you may think as well that your theory has no decision
procedure.

Working mathematicians can view formal theories as
mathematical models of traditional (purely intuitive,
semi-axiomatic etc.) mathematical theories. Formal theories can
be investigated themselves as mathematical objects. The
Unsolvability theorem establishes for formal theories essentially
the same phenomenon that is well known from the history of (the
traditional) mathematics: **no particular set of ideas and/or
methods allows to solve all problems that arise in mathematics**
(even when our axioms remain stable and "sufficient").
To solve new problems - as a rule - new ideas and new methods are
necessary. Thus, mathematics is a kind of perpetuum mobile - an
infinite challenge, an infinite source of new ideas.

As number theorists have noticed long ago, the famous Riemann's
hypothesis allows not only proving of new (stronger) theorems
about prime numbers. Assuming this hypothesis we can also obtain **simpler
proofs** of some well-known theorems. These theorems can be
proved without Riemann's hypothesis, yet these
"puristic" proofs are much more complicated.

How looks this phenomenon at the level of formal theories? If we add to our theory T a new axiom - some hypothesis H that is undecidable for T, then we obtain a new "stronger" theory T+H. And small wonder, if in T+H not only new theorems can be proved (that were unprovable in T), yet also some hard theorems of T allow much simpler proofs in T+H?

Kurt Goedel proved in 1936 that this is really the case:

**K.Goedel.** Ueber die Laenge von Beweisen.
"Ergebnisse eines mathematischen Kolloquiums (herausgegeben
von K.Menger)", 1936, Heft 7, pp,23-34

Let us denote by min_proof_{T}(K) the size of shortest
T-proof of the formula K (the exact definition will follow). For
a better understanding of the theorem you may take at first f(x)
= x/100.

**Theorem on the Size of Proofs.** If T is a fundamental
formal theory, and a closed formula H is not provable in T, then
for each computable function f(x) which grows to infinity there
is a theorem K of T such that

min_proof_{T+H}(K) < f(min_proof_{T}(K)).

For example, let use take f(x) = x/100. There is a theorem K_{1}
of the theory T such that its proof in the extended theory T+H is
at least 100 times shorter than its shortest proof in T. You can
take also f(x) = x/1000, or sqrt(x), or log_{10}(x) etc.

The above theorem holds for any method of measuring the size of proofs that satisfies the following two conditions:

a) The size of a proof is computable from the text of it.

b) For any number t there is only a finite set of proofs having sizes <=t. More precisely, there is an algorithm that (given a number t) prints out all proofs having sizes <=t, and halts.

The simplest method of measuring the size of proofs (by the
number of characters, i.e. the length of the text) satisfies
these conditions. Indeed, for a theory T each T-proof is a
sequence of formulas in the language of T. If the alphabet of the
language is finite, i.e. it consists of some s characters
(variable names are generated, for example, as x, xa, xaa, xaaa,
etc.), then there are no more than s^{t} proofs having
sizes <=t.

**Proof of the theorem.** Let us assume the opposite: there
is a computable function f(x) which grows to infinity such that
for all theorems K of the theory T:

min_proof_{T+H}(K) >= f(min_proof_{T}(K)).
------------(1)

We will derive from this assumption a **decision procedure**
for the theory T+~H. Since formula H is not provable in T, theory
T+~H is a consistent fundamental theory, hence, such decision
procedure cannot exist (see the Unsolvability theorem in Section 6.3).

So, let use (1) to build a decision procedure for T+~H. If some formula K is provable in T+~H, then T proves the formula ~H->K. Then (1) yields that

f(min_proof_{T}(~H->K)) <=
min_proof_{T+H}(~H->K).

Now let us note that the formula ~H->K has a **very short
proof** in T+H. Indeed, by means of propositional calculus we
can prove the formula H->(~H->K), and since H is axiom of
T+H, we obtain ~H->K immediately. Imagine we have this proof
in its entirety:

...

...

H->(~H->K) ------- up to this place - a fixed proof schema in propositional calculus

H ----------- axiom of T+H

~H->K ------------ by MODUS PONENS

Thus, the entire proof is a proof schema with "parameters" H, K. Hence, its size is a computable function g(H, K) (see the condition a) above). Thus we have:

min_proof_{T+H}(~H->K) <= g(H,
K),

and

f(min_proof_{T}(~H->K)) <= g(H,
K). ----------(2)

I.e. if K is provable in T+~H, then T proves ~H->K and (2) holds. Since f and g are computable functions, and since f is growing to infinity, we can obtain another computable function h(H, K) such that, if K is provable in T+~H, then

min_proof_{T} (~H->K) <= h(H, K).

**Exercise 6.5.** Show that this is the case. How would you
compute h(H, K)?

Having the function h we can propose the following procedure for solving is an arbitrary formula K provable in T+~H, or not. If T+~H proves K, then T proves ~H->K, and one of these proofs is of size <=h(H, K). So, let us compute h(H, K), and let us examine the (finite) list of all proofs of sizes <=h(H, K) (see the condition b) above). If one of these proofs is proving ~H->K in T, then T+~H proves K. If there is no such proof in the list, then T+~H cannot prove K. Q.E.D.

Maybe, the above-mentioned method of measuring size of proofs seems "unnatural" to you. Maybe, you would like to have in the alphabet of the language an infinite set of letters for variables, and a finite set of other characters? Then, by replacing variable letters in some proof, you can obtain an infinite number of equivalent proofs having the same size (i.e. the length of text measured in characters). Hence, for your "method" the condition b) does not hold. Still, how would you display your infinite characters set on screens, and how would you print them out? I.e. having an infinite alphabet, you must introduce some method for measuring size ... of characters (in pixels or dots of a fixed size). And the condition: c) for any number t there is only a finite set of characters having sizes <=t. And respectively, you must measure size of proofs in pixels or dots, not in characters. And for this elaborate method the condition b) will hold!

How would we prove Goedel's incompleteness theorem knowing that for each effectively enumerable set we can build a Diophantine representation (see Section 4.1)? For a precedent of such "Diophantine incompleteness theorems" see Davis, Putnam, Robinson [1961] (Corollary 2a).

Let T be a fundamental theory. The following predicate is effectively enumerable:

pr_{T}(x) = "T proves the
T-translation of the PA-formula number x".

Let us denote by

Ez_{1}...Ez_{k} P_{T}(x,
z_{1},... , z_{k})=0

the Diophantine representation of pr_{T}(x). Here: P_{T
}is a polynomial with integer coefficients, the numbers k of
variables may depend on T (still, we can take for granted that it
never exceeds 13, see Matiyasevich,
Robinson [1975]). Each PA-formula F is provable in T, iff the
Diophantine equation P_{T}(**F**, z_{1},... ,
z_{k})=0 has solutions in natural numbers (**F**
is Goedel number of F). By applying Self-Referential lemma we
obtain a closed PA-formula D_{T} such that

PA proves: D_{T} <-> ~Ez_{1}...Ez_{k}
P_{T}(**D**_{T}, z_{1},... , z_{k})=0.
--------(1)

Thus D_{T} is a Diophantine version of the Goedel's
formula G_{T}.

Let us assume that T proves D_{T}. Then pr_{T}
(**D**_{T}) is true, and hence, the equation

P_{T}(**D**_{T}, z_{1},...
, z_{k})=0 -----------(2)

has solutions in natural numbers. Denote one of these
solutions by (b_{1},... , b_{k}), then

PA proves: P_{T}(**D**_{T},
b_{1},... , b_{k})=0

as a numerical equality that does not contain variables (see Exercise 3.4). Hence,

PA proves: Ez_{1}...Ez_{k} P_{T}(**D**_{T},
z_{1},... , z_{k})=0,

and by (1) we have established that PA (and T) proves ~D_{T}.
I.e., if T proves D_{T}, then T is inconsistent.

On the other hand, if T is consistent, then T cannot prove D_{T}.
Hence, pr_{T}(**D**_{T}) is false, and
the equation (2) has no solutions in natural numbers.
Nevertheless, the corresponding formula

~Ez_{1}...Ez_{k} P_{T}(**D**_{T},
z_{1},... , z_{k})=0

that asserts this unsolvability cannot be proved in T (because
it is equivalent to D_{T}).

Thus we have established the following

**Diophantine Incompleteness Theorem. **Let T be a
fundamental theory. Then there is a Diophantine equation Q_{T}(x_{1},
... , x_{n})=0 such that: a) If T is inconsistent, then
the equation **has** solutions in natural numbers. b) If T is
consistent, then the equation **has no** solutions in natural
numbers, yet this cannot be proved it T.

Let us consider the Diophantine equation Q_{PA}=0. If
we will find some its solution in natural numbers, then we will
find a contradiction in PA. Still, if Q_{PA}=0 has no
solutions in natural numbers, then this cannot be proved in PA.
I.e. PA cannot solve some problems in the area of Diophantine
equations. Since the set theory ZF proves the consistency of PA,
then ZF proves also the unsolvability of the equation Q_{PA}=0.
I.e. in set theory we can solve some problems in the area of
Diophantine equations that cannot be solved in first order
arithmetic. This contradicts the widely believed thesis about the
"primary nature" of natural numbers in mathematics.
Some people believe that the notion of natural numbers does not
depend on more complicated mathematical notions (for example, on
the notion of real numbers, or Cantor's notion of arbitrary
infinite sets). A striking expression of this belief is due to Leopold
Kronecker:

**Die ganzen Zahlen hat der liebe Gott gemacht, alles andere
ist Menschenwerk. **

(God created the integers, all else is the work of men.)**
**As we have seen, this cannot be true: there are even
some problems in the area of Diophantine equations (i.e. very
"intrinsic" problems of natural number system) that can
be solved only by using more complicated notions than the initial
(first order) notion of natural numbers.

The second conclusion: **the notion of natural numbers is
evolving**. When Georg Cantor invented in 1873 the set theory, **he
extended also the notion of natural numbers** by adding new
features to it. For example, before 1873 the unsolvability of the
above equation Q_{PA}=0 could not be proved, but now we
can prove it. See a much more striking example in Appendix 2.

**Note.** The following remarks about Kronecker's famous
sentence appeared on the mailing list Historia-Mathematica:

-----Original Message-----

From: Walter Felscher <walter.felscher@uni-tuebingen.de>

To: Bill Everdell <Everdell@aol.com>

Cc: historia-matematica@chasque.apc.org <historia-matematica@chasque.apc.org>

Date: 1999. May 27. 9:36

Subject: [HM] Die ganzen Zahlen hat der liebe Gott gemacht

The earliest reference to Kronecker's dictum, appearing in the
subject, seems to be the necrologue

Heinrich Weber: Leopold Kronecker. Jahresberichte D.M.V 2 (1893)
5-31

where Weber writes about Kronecker

Mancher von Ihnen wird sich des Ausspruchs erinnern, den er in
einem Vortrag bei der Berliner Naturforscher-Versammlung im Jahre
1886 tat "Die ganzen Zahlen hat der liebe Gott gemacht,
alles andere ist Menschenwerk".

It is important not to omit in this dictum the adjective
"liebe" in "liebe Gott".

Because "lieber Gott" is a colloquial phrase usually
used only when speaking to children or illiterati. Adressing
grownups with it contains a taste of being unserious, if not
descending (and not towards the audience, but towards the object
of substantive "Gott") ; no priest, pastor, theologian
or philosopher would use it when expressing himself seriously.
There is the well known joke of Helmut Hasse who, having quoted
Kronecker's dictum on page 1 of his yellow "Vorlesungen
ueber Zahlentheorie" 1950, added to the index of names at
the book's end under the letter "L" the entry
"Lieber Gott ........ p.1 "

As Kronecker's dictum is related, it appears as nothing but a
witticism: "About the integers let us not ask, but all the
rest came about by men - namely so ... "

Would Kronecker have wanted to make a theologico-philosophical
statement, he would have omitted the Children's language:
"Die Zahlen kommen von Gott, der Rest ist menschliche
Erfindung."

I doubt that Kronecker's dictum can be construed to express a
distinction between a Kroneckerian viewpoint of a divine,
pre-human origin of the integers, and Dedekind's viewpoint that
also the integers are man-made (i.e. man-invented) .

W.F.

In his proof of the incompleteness theorem K.Goedel used a
formula asserting "I am unprovable in the theory T",
i.e. formula G_{T} such that

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

If T is a consistent theory, then, indeed, G_{T} is
unprovable in T.

Now let us imagine a formula asserting just the opposite -
"I am provable in T", i.e. a formula H_{T} such
that

PA proves: H_{T} <-> PR_{T}(**H**_{T}).

Will such a formula really be provable in T - "as it wants to be"? Leon Henkin asked this question in 1952. The answer is "yes" - as M.H.Loeb proved in 1955:

**M.H.Loeb.** Solution of a problem of Leon Henkin.
"Journal Symb. Logic", 1955, vol.20, pp. 115-118

**Loeb's Theorem.** If T is a fundamental theory, and PR_{T}(x)
is a PA formula satisfying Hilbert-Bernays conditions (see Section 5.4), then for any closed
formula B: if T proves PR_{T}(**B**)->B, then T
proves B.

Hence, T proves the above formula H_{T}.

**"Proof".** If T proves PR_{T}(**B**)->B,
then T proves ~B->~PR_{T}(**B**). Hence, T+~B
proves ~PR_{T}(**B**). I.e. T+~B proves that B is
unprovable in T. Hence, T+~B proves that T+~B is a consistent
theory. By Goedel's second theorem, if T+~B proves its own
consistency, then T+~B is inconsistent, i.e. T proves B. Q.E.D.

The above "proof" contains essential gaps.

**Exercise 6.6 **(the final test of the entire course).
Determine and fill in these gaps.

Formula PR_{T}(**B**)->B asserts: "If B is
provable in T, then B is true", i.e. it asserts that T is
"sound" for B. Loeb's theorem says that if T proves its
own "soundness" for B, then T proves B. I.e. if T
cannot prove B, then T cannot prove that it is "sound"
for B.

Read more about implications of Loeb's theorem in Barwise [1977] (the section about incompleteness theorems).

**Open Problem?** Formula B->PR_{T}(**B**)
asserts: "If B is true, then B is provable in T", i.e.
it asserts that T is "complete" for B. If T proves its
own "completeness" for B, then - what?

Goedel, incompleteness theorem, Gödel, theorem, incompleteness, significance, size of proofs, Loeb, Kronecker, Löb, lieber Gott

Back to title page.