Godel, incompleteness theorem, significance, consequences, Gödel, theorem, Goedel, incompleteness, consistency, size of proofs, unsolvability, inconsistent, size, proofs, theorems, creative, Loeb, inconsistency, Kronecker, Löb, creativity, consistent, mathematics, Diophantine, Lob

Back to title page.

6. Around Goedel's Theorem

6.1. Methodological Consequences

From incompleteness theorems, some people derive the thesis about the superiority of the "alive, informal, creative, human thinking" over axiomatic theories. Or, about the impossibility to cover "all the treasures 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 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 are painting the following picture.

Let us consider any formal theory T that contains a full-fledged concept of natural numbers (i.e. – in my terms – T is 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 – a true statement 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 the properties of natural numbers, which cannot be proved in T. Hence, none of formal theories can express 100% of the "informal, human" notion of natural numbers. If you fix some particular formal theory, my "creative mind" will unmistakably find a true assertion G_T overcoming all what can be proved in T.

The analysis of Goedel's proof presented in Section 5.4 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 the consistency of T. Indeed, if G_T were proved to be true, then also the consistency of T were proved (G_T asserts its own unprovability, and the unprovability of at least one formula means the 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 will not be taken seriously. Still, the following fact has to be taken absolutely seriously: there is no algorithm that could detect, by 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 any 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 by Stanley Burris)

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

In 1902, when the second (final!) volume of Frege's book was ready to print, he received a letter from Bertrand Russell, who established that from Frege's principles a contradiction can be derived (about Russell's paradox see Section 2.2). Frege added Appendix II:

"Hardly anything more unfortunate can befall a scientific writer than to have one of the foundations of his edifice shaken after the work is finished. This was the position I was placed in by a letter of Mr. Bertrand Russell..." (quoted after Heijenoort [1967]).

Soon after this, Frege's wife died in 1904. Frege died in 1925, yet after 1903 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 could consider the situation as his personal failure. Was it really? Even today, reading Frege's book without prejudice, you have the impression of absolute reliability of his basic principles. 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 mathematical 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 – to 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 and how distinguished people share this "feeling", cannot serve as an absolute warranty against contradictions.

Martin Davis: "I'm fond of noting that the list of logicians who have seriously proposed formal systems that turned out to be inconsistent reads like an honor roll: Frege, Church, Curry, Quine, Rosser." (see FOM Archives, May 30, 2003, http://cs.nyu.edu/pipermail/fom/2003-May/006665.html).

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 obtaining 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 must be called 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. When drawing consequences from a hypothesis we may come to contradictions, and then we will be forced to reject it.

And once you postulate the consistency of your favorite theory T, then, to prove the truth of the formula G_T we need no more than the (formal!) axioms of PA! Indeed, as we know, PA proves Con(T)->G_T, hence, after assuming of Con(T), the truth of G_T follows immediately and formally!

“The method of "postulating" what we want has many advantages; they are the same as the advantages of theft over honest toil.” (Bertrand Russell, Introduction to Mathematical Philosophy, 1919, quoted from http://en.wikiquote.org/wiki/Bertrand_Russell)

Our final conclusion may be formulated as follows: incompleteness theorems do not yield a general method allowing to overcome unmistakably (i.e. on the first trial) any given formal theory. It seems that such general methods do 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 the problems from its domain of competence. 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.

Imperfect theory must be and can be improved. Contradictions can be removed by improving axioms. The problems that were proved (or are suspected) to be undecidable – we can try to solve them 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 the 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 and 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. unstable or non-self-contained) systems of reasoning – this would be no mathematics! Im mathematics, one is allowed to change the axioms only deliberately.

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 the 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 are simply some kind of imperfect systems that should be improved.

6.2. Double Incompleteness Theorem

Paul Levy discussed the possibility of the double incompleteness phenomenon in 1926:

P.Lévy. Sur le principe du tiers exclu et sur les théoremes non susceptibles de démonstration. "Revue de Métaphysique et de Morale", 1926, vol. 33, N2, pp. 253-258.

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 judgment 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 in 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 Tr_T and Tr_M the translations 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 a metatheory for T. Then there is a closed 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 computably enumerable, let an appropriate Turing machine enumerate all arithmetical theorems of T and M:

(T, A₀), (M, A₁), (T, A₂), (M, A₃), ... -----------(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 computably 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 closed 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 possibility 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 for solving of 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. the consistency of T+~H), nor ~RF_T (H) (i.e. the 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.

From this point of view, for example, the axiom of determinacy (AD) is only a "semi-dangerous" postulate: if ZF is consistent, then

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

cannot be proved in ZF. However, one can prove in PA that

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

Open problem? All the well-known powerful set-theoretic hypotheses H are "semi-dangerous" only (in the above sense), all having the following properties:
a) PA proves: Con(ZFC) -> Con(ZFC+ ~H);
b) Con(ZFC) -> Con(ZFC+H) cannot be proved (sometimes, even in ZFC+H).
Or, the same property with ZF instead of ZFC. Is there some interesting set-theoretical hypothesis H such that neither
Con(ZF) -> Con(ZF+H) (or Con(ZFC+H)),
nor
Con(ZF) -> Con(ZF+ ~H) (or Con(ZFC+ ~H))
can be proved (in PA, in ZF etc.)?

6.3. Is Mathematics "Creative"?

In mathematics all theorems are being 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, when 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: continuum hypothesis, axiom of constructibility and axiom of determinacy!

Q.E.D., if you agree that the distinctive character of a mathematical theory is a stable 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 computably enumerable. I.e. you can write a computer program that will work printing out the (infinite) sequence of all theorems of ZFC:

F₀, F₁, F₂, F₃, F₄, ...

Note. According to the official terminology, computably enumerable sets are called "recursively enumerable sets", in some texts – also effectively enumerable sets, or listable sets.

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 ZFC "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 the above computer program for this purpose? Having bought enough beer you could stay sitting very long by the paper tape of your computer waiting for the formula H printed out (this would mean that ZFC proves H) or the formula ~H printed out (this would 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 – let us wait another 100 years or let us drop waiting immediately.

Hence, the obvious enumerating program for ZFC almost 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" (producing "nothing new"), 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, if and only if there is an algorithm determining the 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. 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, i.e. under the assumption that classes a) and b) do not intersect. Then, by the First (Goedel-Rosser) Incompleteness Theorem, the class c) is non-empty.

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 computably separable (another term – "recursively separable") from the class of all T-refutable formulas, if and only if 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 an algorithm does not exist, if T is a consistent fundamental theory. I.e., we will prove that the class of all T-provable PA formulas (i.e. first order arithmetical formulas) is not computably separable from the class of all T-refutable PA formulas.

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

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₀(x, t), C₁(x, t) express in PA the following (computably solvable) 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₁(E, t) -> (Ez<t)C₀(E, z)).

Exercise 6.4. Following 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, no algorithm can separate T-provable PA formulas from T-refutable PA formulas. Q.E.D.

As you know, the class of all T-provable formulas, and the class of all T-refutable formulas both are computably enumerable (or, recursively enumerable). It follows from our theorem that neither of these classes can be computably solvable (i.e. recursive), and that the class of all T-undecidable formulas is not even computably enumerable (and, in particular, non-empty).

Exercise 6.4A. Verify.

Thus, the First Incompleteness Theorem is an easy consequence of the Unsolvability Theorem.

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, this 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.1, 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. Any decision procedure of this theory necessarily takes 2^2^Cn steps to decide about formulas consisting of n characters (^ stands for exponentiation). Thus, from a practical point of view, we may think as well that Presburger arithmetic “has no decision procedure”.

Working mathematicians can view formal theories as mathematical models of the traditional (purely intuitive, semi-axiomatic etc.) mathematical theories. Formal theories, themselves, can be investigated 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 solving of 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 – a never ending challenge, a never ending source of new ideas.

6.4. On the Size of Proofs

As number theorists have noticed long ago, the famous Riemann's hypothesis (published 1859) allows not only proving of new (stronger) theorems about prime numbers. By 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 "purist" 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 1935 (published 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 |K|_T 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

|K|_T+H < f(|K|_T).

For example, let us take f(x) = x/100. There is a theorem K₁ 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 may try also f(x) = x/1000, or √x, or log₂(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:

|K|_T+H ≥ f(|K|_T). ------------(1)

The main idea – 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(|~H->K|_T) ≤ |~H->K|_T+H. -----------(1a)

The second idea – let us note that the formula ~H->K always is provable in T+H, moreover, it 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. By (1a), this fact yields an upper bound b for the size of the shortest proof of ~H->K in T. By scanning all proofs of size ≤b we can determine, is ~H->K provable in T (i.e. is K provable in T+~H), or not.

More precisely, let us imagine the mentioned "very short proof" of ~H->K in full:

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:

|~H->K|_T+H ≤ g(H, K),

and

f(|~H->K|_T+H) ≤ 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

|~H->K|_T ≤ 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 the 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!

Further reading:

Samuel R. Buss. On Godel's theorems on lengths of proofs I: Number of lines and speedups for arithmetic. Journal of Symbolic Logic 39 (1994) 737-756.

Samuel R. Buss. On Godel's Theorems on Lengths of Proofs II: Lower Bounds for Recognizing k Symbol Provability. In Feasible Mathematics II, P. Clote and J. Remmel (eds), Birkhauser, 1995, pp. 57-90.

Short Theorems with Long Proofs

Inspired by reading
D.Zeilberger. THEOREMS FOR A PRICE: Tomorrow's Semi-Rigorous Mathematical Culture. Notices of the AMS, Vol. 40, N8 (October 1993), pp.978-981 (online copy available).

Joel H. Spencer. Short Theorems with Long Proofs. Amer. Math. Monthly, 1983, vol. 90, pp. 365-366.

John W. Dawson. The Godel incompleteness theorem from the length of proof perspective. Amer. Math. Monthly, 1979, vol. 86, pp. 740-747.

Theorem. Assume, T is a fundamental formal theory, and f(x) is a computable function that grows to infinity. If T is consistent, then there is a theorem K of T such that |K|_T > f(|K|), i.e. the shortest T-proof of K is "f-longer" than the length |K| of the theorem K itself.

For example, let us take f(x) = 1000000*x. There is a theorem K of the theory T such that its proof is more than million times longer than the formula K itself. You may try also f(x) = (1000*x)², or 2^1000*x etc.

Exercise 6.6. Prove the above theorem. (Hint: assume the contrary, and derive a contradiction with the Unsolvability Theorem.)

6.5. Diophantine Incompleteness Theorem: Natural Numbers Evolving?

How would we prove Goedel's incompleteness theorem knowing that for every computably 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 computably enumerable:

pr_T(x) = "T proves the T-translation of the PA-formula number x".

Let us denote by

Ez₁...Ez_k P_T(x, z₁,... , z_k)=0

a 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]). Every PA-formula F is provable in T, if and only if the Diophantine equation P_T(F, z₁,... , z_k)=0 has solutions in natural numbers (F is Goedel number of F). By applying the Self-Referential Lemma we obtain a closed PA-formula D_T such that

PA proves: D_T <-> ~Ez₁...Ez_k P_T(D_T, z₁,... , 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₁,... , z_k)=0 ----------- (2)

 as solutions in natural numbers. Denote one of these solutions by (b₁,... , b_k), then

PA proves: P_T(D_T, b₁,... , b_k)=0

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

PA proves: Ez₁...Ez_k P_T(D_T, z₁,... , 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₁...Ez_k P_T(D_T, z₁,... , 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₁, ... , 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 in 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 "the" 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 human notion of natural numbers is evolving. When Georg Cantor invented the set theory in 1873, 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. For a much more striking example (the so-called Extended Finite Ramsey's Theorem) see Appendix 2.

Note. The following remarks by Walter Felscher 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.

6.6. Löb's Theorem

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 Martin Hugo Löb (M.H.Loeb) proved in 1955:

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

Löb's Theorem. If T is a fundamental theory, and PR_T(x) is a PA-formula satisfying Hilbert-Bernays-Löb derivability 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.

As put nicely by Marc Geddes on the extropy-chat mailing list (February 8, 2006): "...Löb's theorem says that if a löbian machine (PM, PA, or ZF for example) proves Bp -> p, for some proposition p, then soon or later the machine will prove p (if it has not been done already)."

"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.7 (the final test of the entire course). Determine and fill in these gaps. (Hint: a) Show that there is a closed formula L such that PA proves L<->~PR_T(~B->L). Verify that, if T+~B proves L, then T+~B is an inconsistent theory. c) Define Con(T+~B) as ~PR_T(~B->0=1), and verify that if T+~B proves Con(T+~B), then T+~B is inconsistent. d) Next gap?)

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. Löb'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 Löb's theorem in the chapter about incompleteness theorems written by Craig Smorynski in Barwise [1977].

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?

Back to title page.

Godel, incompleteness theorem, significance, consequences, Gödel, theorem, Goedel, incompleteness, consistency, size of proofs, unsolvability, inconsistent, size, proofs, theorems, creative, Loeb, inconsistency, Kronecker, Löb, creativity, consistent, mathematics, Diophantine, Lob