Godel's incompleteness theorem
The Gödel's incompleteness theorem is one of the most important sets of modern logic . He deals with the derivability of statements in formal systems . The sentence shows the limits of the formal systems - above a certain performance level. He shows that in sufficiently strong systems, such as arithmetic , there must be statements that can neither be formally proven nor refuted. The theorem thus proves the impossibility of the Hilbert program , which was founded by David Hilbert, among other things, to prove the consistency of mathematics. The theorem was published in 1931 by the Austrian mathematician Kurt Gödel .
More precisely, a distinction is made between two sentences of incompleteness. The first theorem of incompleteness says that there are always unprovable statements in sufficiently strong, consistent systems. The second theorem of incompleteness says that sufficiently strong consistent systems cannot prove their own consistency.
Through these sets is mathematics set a fundamental limit: Not every mathematical set may consist of the axioms of a mathematical sub-region (for example, arithmetic, geometry and algebra ) are formally derived or refuted.
In the philosophy of science and in other areas of philosophy, the sentence is one of the most popular in mathematics. The book Gödel, Escher, Bach and the works of John Randolph Lucas are often highlighted as examples.
Statements are sequences of characters that, like a program in a programming language, must comply with a certain syntax . For such statements one defines the concept of validity or truth in structures in an obvious way (see model theory ). The truth of a statement can depend on the structure under consideration: A statement with the intended meaning "There is an element that is really greater than 0 and really less than 1" applies to the structure of real numbers, but not to the structure of natural numbers.
A formal system is a system in which mathematical statements can be proven. Each formal system consists of a language, which specifies the amount of well-formed formulas and statements, a set of axioms and a set of rules of inference , with which new statements can be derived from already proven statements. A formal system determines a theory , the set of all statements that can be derived in the system. It is important that the correctness of a proof in the formal system can be verified in a mechanical way. For example, calculi with infinitely large proofs are not formal systems in this sense. In terms of computability theory , this corresponds to the formal requirement that the theory must be recursively enumerable .
The term sufficiently powerful means something different in the 1st and 2nd incompleteness clause. In the second sentence of incompleteness it is meant that the system T fulfills the Löbschen conditions (L1-L3). In addition, Bernays' derivability condition must be fulfilled.
A system T is called free of contradictions or consistent if there is no statement A, so that both A and the negation of A follow from T. As one can easily show with the principle Ex falso quodlibet, this condition is equivalent to the fact that not every statement follows from T.
A system T is complete , if the statement A or its negation of T follows for all propositions A.
First sentence of incompleteness
"Any sufficiently powerful, recursively enumerable formal system is either contradictory or incomplete."
A sufficient condition for a system to be "sufficiently powerful" is that it describes natural numbers with addition and multiplication and that some elementary properties of natural numbers can be expressed and proven in them, including, for example, that there is no natural number below zero and that statements like , or etc. can be formulated.
Gödel originally showed the theorem under a somewhat stronger assumption than consistency, namely ω-consistency , which is also assumed in this sketch for the sake of simplicity. In 1936 John Barkley Rosser showed how this requirement can be dropped.
His reasoning uses a count of all sentences within the formal system under consideration. Each sentence is assigned a unique number (its Gödel number ). Gödel then constructs a formula for the form
"The sentence with the number cannot be derived."
and shows with the help of a diagonalization that there is an substitution for such that the sentence with the number is equivalent to the statement
"The sentence with the number cannot be derived."
is. This gives him a sentence with the intuitive meaning “I cannot be deduced”, the so-called Godel's sentence. Godel himself motivated this construction with the liar's paradox .
Now consider the sentence "The sentence with the number can be derived". A proof of contradiction shows that this proposition, like its negation, cannot be derived, and thus the system is incomplete: Assuming that the proposition could be derived. Then it follows from the ω-consistency and the strength of the system that the sentence with the number can be derived. However, this is exactly equivalent to the negation of the sentence “The sentence with the number can be derived”. This results in a contradiction in the system. However, since this was assumed to be consistent, the sentence cannot be derived.
Let us now assume that the negation of the sentence, ie the sentence “The sentence with the number cannot be derived”, and thus the sentence with the number equivalent to it, can be derived . Because the system is assumed to be sufficiently powerful to "understand" this proof within the system, it now follows that the sentence "The sentence with the number can be derived" can be derived. For this, however, the system would again have to be contradicting itself. So the sentence “The sentence with the number cannot be derived” cannot be derived either. The metalinguistic sentence that the sentence with the number cannot be derived in the system is thus proven.
Second sentence of incompleteness
The second theorem of incompleteness says that any sufficiently powerful consistent system cannot prove its own consistency:
"Any sufficiently powerful consistent formal system cannot prove its own consistency."
The statement follows from the first sentence. Be a consistent formal system that is strong enough to formalize and prove the first incompleteness clause in it. Then the statement proves : "If is consistent, then the sentence 'I am not provable' is not provable." In order to generate a contradiction, one suppose that proves the statement " is consistent". Combining the two statements, modus ponens in a proof yields the statement “The sentence I am not provable is not provable.” However, this statement is synonymous with the statement “I am not provable”, so there is also a proof for this statement. This is a contradiction to the first sentence of incompleteness. So it is either inconsistent, or it cannot prove its own consistency.
First sentence of incompleteness
Godel's first incompleteness theorem shows that every consistent formal system that contains enough statements about natural numbers is incomplete: there are true statements that can be expressed in his language, but that cannot be proven. This means that no formal system (which fulfills the prerequisites of the theorem) can uniquely characterize the natural numbers, since unprovable number theoretic statements always remain.
The existence of an incomplete formal system is initially not surprising. A system can be incomplete simply because not all of the necessary axioms have been formulated. For example, Euclidean geometry is incomplete without the axiom of parallels ; this can neither be proved nor refuted with the other axioms.
Godel's theorem shows that in theories that contain a small amount of number theory, a complete and consistent finite list of axioms cannot in principle exist, and that a corresponding infinite list cannot be enumerated by a computer program. According to the Church-Turing thesis , such a list cannot be created by any other intuitively calculable algorithm . Every time a new theorem is added as an axiom, there are other true statements that still cannot be proven with the new axiom. If an axiom is added that makes the system complete, the system becomes contradictory at the same time.
Nevertheless, there are complete and consistent sets of axioms for arithmetic, but they cannot be enumerated by an algorithm. For example, the set of true statements about natural numbers,, is a complete and consistent axiomatization of arithmetic. The difficulty with this is that there is no mechanical method to prove that a statement is in this set. A similar problem arises with infinite calculi such as arithmetic with the ω-rule , an infinite inference rule with which exactly the true arithmetic statements can be proven. Since derivatives with the ω-rule are infinitely large, there is no mechanical method to verify such proofs.
The incompleteness theorem only says something for formal systems that meet the necessary requirements. Not all mathematically interesting axiom systems meet these requirements, even if they have models that contain the natural numbers. For example, there are complete axiomatizations of Euclidean geometry , the theory of the algebraically closed fields of characteristics , the dense linear orders without the largest and smallest element, and the natural numbers without multiplication ( Presburger arithmetic ). Crucially, these theories are not expressive enough to represent certain essential properties in terms of natural numbers.
Second sentence of incompleteness
Godel's second theorem of incompleteness also implies that a sufficiently strong, consistent theory cannot prove the consistency of a theory if it proves the consistency of . Because such a theory can prove that if is consistent and this proves the consistency of , must also be consistent. Because the consistency of can be formalized as "no number is Gödel number of a contradiction in ". If would be inconsistent, then would a , prove that the Gödel number of a proof by contradiction in is. But if also proves the consistency of , it also proves that no such exists, so would be inconsistent.
This corollary of the second theorem of incompleteness shows that it is not possible, for example, to formalize the consistency of Peano arithmetic with finite means, which can be formalized in a weaker theory, the consistency of which Peano arithmetic can prove. For example, the consistency of Primitive Recursive Arithmetic (PRA), which is often viewed as the formalization of the finite kernel of mathematics, can be proven in Peano arithmetic. This means that PRA cannot prove the consistency of Peano arithmetic. The fact is often seen as proof that Hilbert's program , which mathematics wanted to justify by finite consistency proofs, is at least not executable in the narrower sense of "finite".
The second theorem of incompleteness does not make consistency proofs completely impossible, but only consistency proofs that can be formalized in the theory concerned. In particular, consistency proofs are often possible in stronger systems. Peano arithmetic proves the consistency of weaker forms of arithmetic, Zermelo-Fraenkel set theory the consistency of Peano arithmetic, and extensions of Zermelo-Fraenkel set theory with large cardinal numbers prove the consistency of set theory. Such a theory does not always have to be stronger. Gentzen's proof of consistency for Peano arithmetic can be formalized in a theory that consists of the weak primitive recursive arithmetic and an axiom for the well-foundedness of the ordinal number ε 0 . Neither of the two theories proves all the statements of the other, so the strengths of the two theories are not directly comparable.
The second theorem of incompleteness is only proven for formal systems that are strong enough to formalize the proof of the first theorem of incompleteness. There are consistent theories that can express and prove consistency, especially subsystems of arithmetic in which multiplication is not provable as a total function. These systems can formalize the concept of provability, but not the diagonalization necessary for the first incompleteness theorem.
Significance for the Hilbert program
Gödel dealt a severe blow to the so-called Hilbert program with his incompleteness sentence . This was proposed by David Hilbert in 1921 and had a decisive influence on research in logic in the 1920s. It aimed to formalize all mathematics through a system of axioms in first-order predicate logic and to demonstrate the consistency of the axioms. This was intended to dispel concerns about non-constructive conclusions in mathematics, which have been expressed primarily by intuitionists . Hilbert proposed to prove the consistency of more complex systems by that of simpler systems. The motivation for this is that a proof of the consistency of a system that is given in this system itself cannot be trusted. Because everything can be proven from a contradiction ( ex falso quodlibet ), so the consistency of the system could also be proven from a contradiction in the system. Therefore the consistency should be proven in a simpler system, so that ultimately the consistency of all mathematics can be reduced to simple, apparently consistent axioms.
According to the second theorem of incompleteness, however, it is impossible to prove the consistency of a system in itself, and thus even more so to prove it in a simpler system.
Although Godel repeatedly identified himself as a Platonist in the course of his life, his sentence of incompleteness was repeatedly interpreted in a subjectivist sense. Gödel's participation in the Vienna Circle also seemed to suggest a proximity between the principle of incompleteness and logical positivism , which is opposed to Platonism in many ways. Gödel's reserved, conflict-averse manner helped keep these interpretations alive.
Gödel himself understood his sentence, however, in particular as a blow to the formalism in mathematics propagated by Hilbert, which should ultimately make all mathematics a purely formal structure without reference to the “real world”. For Gödel as a Platonist, however, the mathematical objects were quite "real". While they could not be confirmed by sensory perception (as the positivists demanded), they were accessible to knowledge. For Gödel, the incompleteness theorem showed that this reality could not be approached with purely formal means.
Although Gödel did not differ very much from Ludwig Wittgenstein in his basic attitude towards the then significant logical positivism , who recognized a reality beyond the possible meaning of sentences (and even considered it more important than what could be said), Wittgenstein and Gödel did not think much of their lives from each other. In Wittgenstein's work, the incompleteness sentence is treated rather disparagingly. For Wittgenstein, the sentence was only good for "logical feats". Gödel, on the other hand, dismissed any influence Wittgenstein had on his own thinking in later interviews.
Gödel's incompleteness theorems are also quoted outside of mathematical logic, not only in mathematics. It can easily be overlooked that the technical terms used in the sentences do not always have the same meaning as identical or similar terms in other contexts. In some attempts to make the results available to a wider audience, this problem is not clearly highlighted. In this respect, wrong ideas about the meaning of the sentences can arise.
Therefore, here are some warnings about possible false conclusions:
- Confusion can arise from the fact that Gödel proved not only the incompleteness theorems, but also Gödel's completeness theorem . It should be noted here that the term completeness is used in two different meanings:
- The completeness theorem proves the semantic completeness of the first-level predicate logic, i.e. it deals with a relationship between models and proofs.
- The incompleteness theorem, however, proves that certain sets of expressions are not complete in the sense of a theory: there are cases where neither a sentence nor its negation belong to the theory.
- Another fallacy is that most theories used in mathematics are incomplete. But there are some important complete, recursively enumerable, consistent theories, such as B. the theory of algebraically closed bodies of characteristics , the theory of dense linear orders without largest and smallest element or Tarski's axiomatization of Euclidean geometry . Crucially, these theories are not expressive enough to represent essential properties in terms of natural numbers and to talk about themselves. There are even certain complete, recursively enumerable fragments of arithmetic in a restricted language. A simple example of such a weak system is arithmetic with only 0 and successors, another is Presburger arithmetic .
- It is possible to describe the arithmetic completely: The theory is (in the sense required here) a complete, consistent extension of the well-known Peano axioms, called true arithmetic . The whole set of these propositions could be called the "axiomatization" of arithmetic. The first theorem of incompleteness shows that this axiomatization is not recursively enumerable.
Examples for the unprovability of concrete sentences
While the unprovable statement that is constructed when proving the first incompleteness theorem is rather artificial, natural mathematical statements are also known that are unprovable in natural mathematical axiom systems.
- In 1943 Gerhard Gentzen showed that the transfinite induction up to ε 0 cannot be derived in Peano arithmetic .
- In 1977 Jeff Paris and Leo Harrington showed that a certain variant of Ramsey's theorem is true in the natural numbers given by the Zermelo-Fraenkel set theory , but unprovable in Peano arithmetic ( Paris-Harrington theorem ).
- In 1982, Jeff Paris and Laurie Kirby showed that Goodstein's theorem in Peano arithmetic is unprovable.
- Since Paul Cohen's proof in 1963, it has been known that both the axiom of choice and the continuum hypothesis are formally undecidable on the basis of the Zermelo-Fraenkel set theory. (In this set theory one can of course formulate a sufficient number of statements about natural numbers.) Since then numerous other examples have been found that in the Zermelo-Fraenkel set theory, and limitations or extensions thereof, statements are neither provable nor refutable.
In order to show the unprovability of some statements of set theory, the second incompleteness theorem can be used directly: If a statement in a set theory implies that there is a model of this set theory and it is therefore consistent, then this statement - consistency of the respective Set theory assumed - not to be derivable. Examples are the unprovability of the replacement axiom in Zermelo set theory , because with it the model can be constructed, or the unprovability of the universe axiom , which directly requires the existence of certain models from ZFC.
Gödel called his essay On Formally Undecidable Theorems of Principia Mathematica and Related Systems I because he planned to write a second essay in which he wanted to explain the proof in more detail. The first essay, however, was so widely recognized that a second was no longer required, which is why it was never written.
Specifically, Gödel's essay referred to the Principia Mathematica , a large formal system that Bertrand Russell and Alfred North Whitehead published between 1910 and 1913. However, Gödel showed that any system with the same power as the Principia Mathematica is just as vulnerable.
Furthermore, Gerhard Gentzen was able to show that constructive mathematics and logic are entirely free of contradictions. This shows a fundamental dispute in mathematics . The philosopher Paul Lorenzen developed a consistent logic and mathematics ( methodical constructivism ), and wrote his book Metamathematik (1962) specifically to show that Godel's incompleteness theorem does not represent an objection to a consistent structure of mathematics.
- Kurt Gödel: About formally undecidable sentences of the Principia Mathematica and related systems I. In: Monthly books for mathematics and physics . 38, 1931, pp. 173-198, doi: 10.1007 / BF01700692 . Zentralblatt MATH. ; available online at  , accessed July 20, 2020
- Kurt Gödel: Discussion on the foundation of mathematics: Knowledge 2. In: Monthly books for math. And physics. 1931-32, pp. 147-148.
- J. Barkley Rosser: Extensions of some theorems of Godel and Church . In: Journal of Symbolic Logic . tape 1 , 1936, pp. 87-91 .
- Douglas R. Hofstadter : Gödel, Escher, Bach , an endless braided ribbon. Munich 1991 ISBN 3-423-30017-5 . (An interesting and relatively easy to understand explanation of Godel's theorem and its implications).
- Wolfgang Franz : About mathematical statements that, including their negation, are demonstrably unprovable. Gödel's incompleteness theorem. Franz Steiner Verlag, Wiesbaden, 1977, 27 pages, ISBN 3-515-02612-6 . (Understandable lecture with references to the history of science).
- Raymond Smullyan : Lady or Tiger - Logical thinking games and a mathematical novel about Gödel's great discovery. Fischer-Verlag, Frankfurt am Main 1983. The American original was published by Alfred A. Knopf, New York in 1982.
- Raymond Smullyan: To Mock a Mockingbird. 1985.
- Raymond Smullyan: Forever undecided: A puzzle guide to Gödel. 1987.
- Dirk W. Hoffmann : Gödel's incompleteness sentences: A guided journey through Kurt Gödel's historical evidence. Springer 2013, ISBN 978-3-8274-2999-5 .
- Bernd Buldt: Incompleteness , in: Jürgen Mittelstraß (Ed.): Encyclopedia Philosophy and Philosophy of Science. 2nd Edition. Volume 8: Th - Z. Stuttgart, Metzler 2018, ISBN 978-3-476-02107-6 , pp. 216-219 (one page bibliography).
- David Hilbert, Paul Bernays: Fundamentals of Mathematics. II (= The Basic Teachings of the Mathematical Sciences . Volume 50 ). Springer, Berlin 1939 ( ags.uni-sb.de - contains a detailed arithmetized proof sketch of the second incompleteness sentence ).
- Peter G. Hinman: Fundamentals of Mathematical Logic . AK Peters, Wellesley 2005, ISBN 1-56881-262-0 (contains a detailed proof of the second incompleteness theorem in set theory).
- Ernest Nagel, James R. Newman: The Gödelsche Proof. 8th edition. 2007, ISBN 978-3-486-45218-1 .
- Wolfgang Rautenberg : Introduction to Mathematical Logic . Vieweg + Teubner, Wiesbaden 2008, ISBN 978-3-8348-0578-2 .
- Peter Smith: An Introduction to Gödel's Theorems. Cambridge Introductions to Philosophy. 2nd edition, Cambridge 2013, ISBN 978-1-107-60675-3 .
- Craig Smorynski: The incompleteness theorems . In: Jon Barwise (Ed.): Handbook of Mathematical Logic . North Holland, 1977, ISBN 0-444-86388-5 .
- Raymond Smullyan: Gödel's Incompleteness Theorems. Oxford Logic Guides. Oxford University Press, 1992.
- Max Urchs: Classic Logic: An Introduction. Berlin 1993, ISBN 3-05-002228-0 (there in the chapter on theories of the first order. Pp. 137-149).
About the meaning of the sentences
- Norbert Domeisen: Logic of the Antinomies. Bern 1990. ISBN 3-261-04214-1 , Zentralblatt MATH.
- Ludwig Fischer: The basics of philosophy and mathematics. Leipzig 1933.
- Torkel Franzen: Gödel's Theorem. An incomplete guide to its use and abuse. Wellesley MA 2005, ISBN 1-56881-238-8 (An easily understandable explanation of Gödel's incompleteness theorems, their implications and their misinterpretations).
- Sybille Krämer: Symbolic machines: the idea of formalization in a historical outline. Darmstadt 1988, ISBN 3-534-03207-1 .
- Paul Lorenzen : Metamathematics. Mannheim 1962, ISBN 3-86025-870-2 .
- Paul Lorenzen : Textbook of the constructive philosophy of science. Stuttgart 2000, ISBN 3-476-01784-2 .
- SG Shanker (Ed.): Gödel's Theorem in focus. London / New York 1988, ISBN 0-415-04575-4 .
- Wolfgang Stegmüller : Incompleteness and undecidability. The metamathematic results of Gödel, Church, Kleene, Rosser and their epistemological significance. 3. Edition. Springer-Verlag, Vienna / New York 1973, ISBN 3-211-81208-3 .
- Max Woitschach: Gödel, Götzen and Computer: a critique of impure reason. Stuttgart 1986. ISBN 3-87959-294-2 .
- Palle Yourgrau: Gödel, Einstein and the consequences. Legacy of an unusual friendship. Beck, Munich 2005. ISBN 3-406-52914-3 . (Original: A World Without Time: The Forgotten Legacy of Gödel and Einstein. Basic Books, Cambridge MA 2005).
- Panu Raatikainen: Gödel's Incompleteness Theorem . In: Edward N. Zalta (Ed.): The Stanford Encyclopedia of Philosophy 2013.
- The limits of predictability
- Christopher v. Bülow: Gödel's first incompleteness theorem. A representation for future logicians. (PDF; 355 kB). March 1992.
- An English translation of Gödel's essay On Formally Undecidable Statements. (PDF; 328 kB).
- Thomas Jech : A short proof of Gödel's Second Incompleteness Theorem . (PDF; 85 kB).
- Gödel's incompleteness sentence in the lexicon of mathematics on Spektrum.de
- Kurt Gödel: About formally undecidable sentences of the Principia Mathematica and related systems I. In: Monthly books for mathematics and physics . 38, 1931, pp. 173-198, doi: 10.1007 / BF01700692 , Zentralblatt MATH.
- Egon Börger: Computability, Complexity, Logic: An introduction to algorithms, languages and calculus with special consideration of their complexity . 2nd Edition. Springer Fachmedien , 2013, ISBN 978-3-663-14213-3 , pp. 378 ( Google Books ).
- Matthias Varga von Kibed : Structure types of logic . Springer-Verlag, Berlin 1984, ISBN 978-3-642-61722-5 , pp. 343 ( Google Books ).
- Dan E. Willard: Self Verifying Axiom Systems, the Incompleteness Theorem and the Tangibility Reflection Principle . In: Journal of Symbolic Logic . tape 66 , 2001, p. 536-596 .
- Gerhard Gentzen: Proof and unprovability of initial cases of transfinite induction in pure number theory . In: Mathematical Annals . tape 119 , 1943, pp. 140-161 , doi : 10.1007 / BF01564760 ( gdz.sub.uni-goettingen.de ).