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 GT asserting "I am not provable in T". Goedel proved that, indeed, GT cannot be proved in T, i.e Goedel proved that GT 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 GT 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 GT 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 GT is a true formula (i.e. that GT cannot be proved in T) only by postulating consistency of T. Indeed, if GT is proved to be true, then also consistency of T is proved (GT 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 GT. 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 GT 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 GT.
b) To prove the formula GT, 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 RT 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 RT 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 RT 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 (NT, TrT) and (NM, TrM) 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 PRT(x) and RFT(x) such that for all PA-formulas F:
a) If T proves TrT(F), then M proves TrM(PRT(F)).
b) If T proves TrT(~F), then M proves TrM(RFT(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 PRT(F), M proves RFT(F)
instead of
T proves TrT(F), M proves TrM(PRT(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 ~PRT(H), nor ~RFT(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, A0), (M, A1), (T, A2), (M, A3), ... -----------(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 ~PRT(H), M proves ~RFT(H). ----------(2)
Therefore, let us call a formula Q positive, if in the enumeration (1) one of the pairs (T, Q) or (M. ~RFT(Q)) appears first, and let us call Q negative, if first appears (T, ~Q) or (M, ~PRT(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 ~PRT(H) (i.e. consistency of T+~H), nor ~RFT (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:
F0, F1, F2, F3, F4, ...
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 C0(x, t), C1(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(C1(E, t) -> (Ez<t)C0(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_proofT(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_proofT+H(K) < f(min_proofT(K)).
For example, let use take f(x) = x/100. There is a theorem K1 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 log10(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 st 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_proofT+H(K) >= f(min_proofT(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_proofT(~H->K)) <= min_proofT+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_proofT+H(~H->K) <= g(H, K),
and
f(min_proofT(~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_proofT (~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:
prT(x) = "T proves the T-translation of the PA-formula number x".
Let us denote by
Ez1...Ezk PT(x, z1,... , zk)=0
the Diophantine representation of prT(x). Here: PT 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 PT(F, z1,... , zk)=0 has solutions in natural numbers (F is Goedel number of F). By applying Self-Referential lemma we obtain a closed PA-formula DT such that
PA proves: DT <-> ~Ez1...Ezk PT(DT, z1,... , zk)=0. --------(1)
Thus DT is a Diophantine version of the Goedel's formula GT.
Let us assume that T proves DT. Then prT (DT) is true, and hence, the equation
PT(DT, z1,... , zk)=0 -----------(2)
has solutions in natural numbers. Denote one of these solutions by (b1,... , bk), then
PA proves: PT(DT, b1,... , bk)=0
as a numerical equality that does not contain variables (see Exercise 3.4). Hence,
PA proves: Ez1...Ezk PT(DT, z1,... , zk)=0,
and by (1) we have established that PA (and T) proves ~DT. I.e., if T proves DT, then T is inconsistent.
On the other hand, if T is consistent, then T cannot prove DT. Hence, prT(DT) is false, and the equation (2) has no solutions in natural numbers. Nevertheless, the corresponding formula
~Ez1...Ezk PT(DT, z1,... , zk)=0
that asserts this unsolvability cannot be proved in T (because it is equivalent to DT).
Thus we have established the following
Diophantine Incompleteness Theorem. Let T be a fundamental theory. Then there is a Diophantine equation QT(x1, ... , xn)=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 QPA=0. If we will find some its solution in natural numbers, then we will find a contradiction in PA. Still, if QPA=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 QPA=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 QPA=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 GT such that
PA proves: GT <-> ~PRT(GT).
If T is a consistent theory, then, indeed, GT is unprovable in T.
Now let us imagine a formula asserting just the opposite - "I am provable in T", i.e. a formula HT such that
PA proves: HT <-> PRT(HT).
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 PRT(x) is a PA formula satisfying Hilbert-Bernays conditions (see Section 5.4), then for any closed formula B: if T proves PRT(B)->B, then T proves B.
Hence, T proves the above formula HT.
"Proof". If T proves PRT(B)->B, then T proves ~B->~PRT(B). Hence, T+~B proves ~PRT(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 PRT(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->PRT(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.