Gödel Proves Incompleteness-Inconsistency for Formal Systems Summary

  • Last updated on November 10, 2022

Kurt Gödel derived incompleteness-inconsistency theorems for any formal system strong enough to include the laws of arithmetic.

Summary of Event

Partly in response to the appearance of logical and set theoretic contradictions following David Hilbert’s Hilbert, David Grundlagen der Geometrie (1899; The Foundations of Geometry, 1902), Foundations of Geometry, The (Hilbert) a number of redoubled efforts focused on extending or reducing mathematics and logic to remove or resolve these difficulties. First published in 1899, Georg Cantor’s Cantor, Georg paradox states that if S is the set of all sets and T is the set of all subsets of S, then because T corresponds one-by-one to itself as a subset of S, it cannot have a greater cardinal than S, yet, by Cantor’s theorem, it must. In addition to Cantor’s paradox, and Bertrand Russell’s Russell, Bertrand proof that Gottlob Frege’s system was contradictory, several other paradoxes with impacts on both mathematics and logic arose during this period. These include Burali-Forti’s paradox of the greatest ordinal number, Berry’s paradox of the least integer not nameable in less than nineteen syllables, Richard’s paradox of the class of all decimal numbers definable in a finite number of words, and symbolic forms of the Cretan-Liar conundrum. [kw]Gödel Proves Incompleteness-Inconsistency for Formal Systems (July, 1929-July, 1931) [kw]Incompleteness-Inconsistency for Formal Systems, Gödel Proves (July, 1929-July, 1931) [kw]Inconsistency for Formal Systems, Gödel Proves Incompleteness- (July, 1929-July, 1931) [kw]Formal Systems, Gödel Proves Incompleteness-Inconsistency for (July, 1929-July, 1931) Mathematics;incompleteness-inconsistency theorems[incompleteness inconsistency theorems] Incompleteness-inconsistency theorems[Incompleteness inconsistency theorems] [g]Austria;July, 1929-July, 1931: Gödel Proves Incompleteness-Inconsistency for Formal Systems[07290] [c]Mathematics;July, 1929-July, 1931: Gödel Proves Incompleteness-Inconsistency for Formal Systems[07290] Gödel, Kurt

The varying approaches of Russell and Hilbert called for the axiomatization, and then formalization, of a suitable portion of existing logic and/or mathematics, including “ideal” statements that did not have identifiable elementary intuitive meanings, to include the new system of (paradox-free) mathematics. In a formal system, all combinatory methods of constructing formulas to express mathematical propositions, and all mathematical assumptions and principles of logic used in proving theorems, are to be governed by a finite set of stated rules. An essential requirement of Hilbert’s original (finitistic) program was that all demonstrations of the formal consistency of a mathematical system involve only procedures that make no reference to an infinite number of properties or operations with mathematical formulas. Second, these proofs were to be undertaken only by “safe” methods such that the resulting formal system of axioms be entirely consistent, interpreted by Hilbert to mean that no two configurations should exist that constitute proofs in the system of a formula A and its negation –A.

In his 1904 lecture on the foundations of logic and arithmetic at the University of Heidelberg, Hilbert for the first time observed that, although it is possible to prove the consistency of geometry by an arithmetic interpretation, for the consistency of arithmetic itself, the appeal to some other more fundamental discipline seems illegitimate. Hilbert, for example, required use of the principle of mathematical induction to justify his definitions of whole numbers, yet had no proof of the consistency of this principle or its resulting definitions. Hilbert, nevertheless, initially suggested building up logic and arithmetic simultaneously, as well as translating these proofs completely into the language of symbolic logic to turn the proof of consistency into a problem of elementary manipulations in arithmetic. Hilbert did not return to foundational studies until his 1917 Zurich lecture on axiomatic thinking, in which he praised the axiomatization of logic by Russell and Alfred North Whitehead Whitehead, Alfred North as the crowning of all work in efforts at completely translating all of mathematics into a self-contained symbolic language.

It was only after 1920 that Hilbert, in collaboration with Paul Bernays Bernays, Paul and in opposition to Hermann Weyl Weyl, Hermann and L. E. J. Brouwer, Brouwer, L. E. J. began to focus explicitly on proof theory. In this approach, description of a formal axiomatic system must enable clear decision as to whether any given formula is an axiom and is a permissible inference from other axioms. This is considered a decision procedure for whether a given finite list of formulas constitutes a proof in any given system, yet a decision procedure is not provided as to whether a given formula is itself provable. The problem of finding a decision procedure has been called the decision problem for formal systems, first recognized as a problem for logic by Ernst Schröder Schröder, Ernst in 1895, and in mathematics by Leopold Löwenheim Löwenheim, Leopold in 1917 and Thoralf Albert Skolem Skolem, Thoralf Albert in 1922. A decision procedure for a formal system embracing a segment of mathematics such as arithmetic would, in principle, make automatic the solution to any problem in that segment. Because of historically intractable problems such as whether Pierre de Fermat’s last theorem is true, pointed out by Brouwer and others, a decision procedure in this case would mean that the infinitely many arithmetical problems require only a finite number of solutions.

By 1928, it was widely believed that the consistency of number theory and arithmetic had finally been nearly achieved by the finitist method of Hilbert and Bernays. As reported in Hilbert’s September, 1928, lecture “On the Problems of the Foundations of Mathematics” in Bologna, Italy, Hilbert announced that his students Wilhelm Ackermann Ackermann, Wilhelm and John von Neumann Von Neumann, John had completed consistency proofs for almost the entire field of arithmetic. Hilbert then listed four of twenty-eight as-yet unresolved problems: a finite consistency proof of mathematical analysis, an extension of this proof to higher-order analysis and functional calculus, the completeness of the axiom systems for number theory and analysis, and the completeness of the system of logical rules (first-order logic).

From the Austrian philosopher and logician Rudolf Carnap’s Carnap, Rudolf diaries and letters to associates, it can be determined that Kurt Gödel was first stimulated to foundational problems by his reading of the text of Hilbert’s lecture and by his attendance at Brouwer’s Vienna lecture in March, 1928, on mathematics, science, and language. From Gödel’s collected papers, it is clear that he was strongly impressed by the intuitionist claim that all of mathematics would never be completely formalizable or preplanned a priori. In 1928, Gödel read the first edition of Hilbert and Ackermann’s Grundzüge der theoretischen Logik (foundations of theoretical logic), in which the completeness of the restricted form of Hilbert’s operational first-level predicate calculus was formulated and posed as an open problem for further study.

A major obstacle to the general solution of Hilbert’s formal decision problem was the lack of a clear and accepted concept of decidability and computability. By decision procedure or decidability for a given formalized theory is meant a method permitting one to decide in any given case whether a specific proposition formulated in the theory’s symbolism can be proven exclusively by means of the axioms and techniques available to the theory itself. Gödel decided to focus explicitly on this problem and wrote the results as his doctoral dissertation in September, 1929, proving the completeness of first-order logic. In the summer of 1930, however, Gödel began to study the problem of proving the consistency of formal analysis itself (including higher arithmetic, logical analysis, and set theory), doubting the feasibility of Hilbert’s wish to prove consistency directly by finitist methods Gödel instead believed that the difficulties encountered by Ackermann and von Neumann could be lessened by dividing the total problem into different stages or levels. In this case, he sought to prove the consistency of number theory by finitist number theory and then to prove the consistency of analysis by number theory, assuming the latter’s truth as well as consistency.

The technical details of Gödel’s proofs are practically impossible to recapitulate in nontechnical nonmathematical language. In terms of mathematical technique, Gödel’s proof employed what has since been known as the arithmetizing of a formalism, in terms of a one-to-one mapping between every proposition in a given theory and the natural numbers of arithmetic. Gödel then extended to general mathematical expressions, such as variables, formulas, propositions, and logical axioms and operations, a similar higher-order arithmetical representation using various recursive functions. (A set of relations is recursive if there is a mechanical method or algorithm permitting one to decide automatically in a particular set whether a given relation does or does not belong to that set.) Gödel ran into several of the paradoxes connected with truth and definability. He realized that “truth” in number theory cannot be defined within number theory itself and that, therefore, his original plan of proving the relative consistency of analysis could not work. Although Gödel realized that these paradoxes did not, strictly speaking, apply to the precisely specified formal analysis of axiomatic systems, he realized that analogous nonlogical analogues could be carried out by substituting the notion of provability for truth.

Pursuing this approach, Gödel concluded that any formal system in which a certain amount of theoretical arithmetic can be developed (according to Giuseppe Peano’s symbolic system) and that satisfies certain minimal consistency conditions is necessarily incomplete in Hilbert’s sense. Gödel, therefore, proceeded to draw the conclusion that in suitably strong systems such as that of Whitehead and Russell’s Principia Mathematica (1910-1913) and Ernst Zennelo’s set theory, there are formally undecidable propositions. This means that for number and set theory, there can be no absolute consistency proof of any of these systems formalizable within these systems. Using Hilbert’s own methods and formalism, Gödel showed that in any formal system with arithmetic, there exist elementary arithmetic propositions that are “intuitively” obvious, yet undeducible, within the system, and that any proof expressing the consistency of the formal system is not deducible within the system. Hence Gödel had not only settled Hilbert’s first three problems in the negative but also refuted Hilbert’s underlying general belief in there always being a finitist consistency proof. In Gödel’s interpretation, this meant that the formal axiomatization of systems of formal mathematics cannot simplify only these systems through logical combinatorics, but introduces inescapable and insoluble problems. Gödel hinted further that the limits of mathematical formalization operate such that every concept in a mathematical theory is meaningful and legitimate, except for certain “singular” points or regions, beyond which the set- and logical-theory paradoxes appear, as something analogous to division by zero. In Weyl’s view, Gödel established that what is provable by intuition and what is provable by deduction, respectively, overlap but are not mutually reducible or expressible.


Whereas Brouwer’s verbally expressed intuitionist convictions on the inexhaustibility and unprovability of mathematics were impressive predominantly to those of affine philosophic outlook, Gödel’s precise formal arguments were more convincing (if less accessible) to mathematicians and logicians of all outlooks. Gödel’s famous first paper was written as part one of a double publication; he planned to give full background and details of his second theorem’s proof in his concluding paper. Unfortunately, this second exposition was never published because, as Gödel admitted, his introductory proof sketch was generally accepted even by those antagonized by his results. As noted by several authors, although many reexaminations have been attempted, no simpler proofs other than Gödel’s originals have, as yet, been developed.

Gödel continued to pursue what he saw as the underlying problems of mathematical evidence and intuition. In 1941, Gödel found an interpretation of Brouwer’s intuitionist number theory using primitive recursive functions of his own origination. This result was jointly regarded as an extension of both Hilbert’s formalism and Brouwer’s intuitionism. The further development of recursive function theory by, for example, Alonzo Church and Alan Mathison Turing, in the context of other problems that could not be decided formally with axiomatic systems, made possible a large number of results about general decision procedures.

There are as many philosophical reactions to and interpretations of Gödel’s recondite conclusions as there are philosophers, including those of Ludwig Wittgenstein, Wittgenstein, Ludwig Russell, and Jean Cavaillès. Cavaillès, Jean Both Russell and Wittgenstein, using differing arguments like Brouwer, basically acknowledged the correctness of Gödel’s result as part of formal axiomatic arithmetic, but denied any wider application of Gödel’s theorems to cases of “uncertainty” and “incompleteness” in mathematics, science, and language at large. Diametrically opposed responses were published by Cavaillès in Sur la logique et la théorie de la science (1947; on the theory of science). In his own essay on Russell’s mathematical logic, Gödel wrote that he did not consider the incompletability of formal systems (such as Whitehead and Russell’s Principia Mathematica) as encompassing a final argument against a neoplatonistic conceptually realistic interpretation of mathematics, but rather as indicating an essential limitation on the expressive power of abstract formal symbolisms considered apart from their field of application. For Gödel, the unexceptional everyday agreement in accepting a mathematical proof reveals a kind of universality and objectivity in mathematics that goes beyond the intersubjective agreement envisioned by Brouwer. Conceptual realism, according to Gödel, requires not only objective concepts but also that to which mathematical concepts are applied, that is, mathematical objects. In his largely unpublished manuscripts, Gödel speaks in a unique idiom about the “perception” and “intuition” of mathematical objects as the common denominator in learning and applying mathematics within mathematics, as well as in the physical and engineering sciences. These are still areas of much continuing debate. Mathematics;incompleteness-inconsistency theorems[incompleteness inconsistency theorems] Incompleteness-inconsistency theorems[Incompleteness inconsistency theorems]

Further Reading
  • citation-type="booksimple"

    xlink:type="simple">Bulloff, J. J., T. C. Holyoke, and S. W. Hahn. Foundations of Mathematics: Symposium Papers Commemorating the Sixtieth Birthday of Kurt Gödel. New York: Springer-Verlag, 1969. Collection includes several valuable essays by both mathematicians and philosophers that underscore and examine the philosophical assumptions that Gödel held but never fully published.
  • citation-type="booksimple"

    xlink:type="simple">Feferman, S., J. W. Dawson, and S. C. Kleene, eds. Kurt Gödel: Collected Works. 2 vols. New York: Oxford University Press, 1986-1990. Presents English translations of unpublished notes as well as technical journal and conference publications by Gödel. Includes a complete bibliography on Gödel.
  • citation-type="booksimple"

    xlink:type="simple">Goldstein, Rebecca. Incompleteness: The Proof and Paradox of Kurt Gödel. New York: W. W. Norton, 2005. Examines the philosophy of Gödel’s mathematics and discusses his theorem of incompleteness as well as various misinterpretations of the theorem. Includes list of suggested reading and index.
  • citation-type="booksimple"

    xlink:type="simple">Nagel, Ernest, and James R. Newman. Gödel’s Proof. Rev. ed. New York: New York University Press, 2002. Reasonably accessible and complete semitechnical account of the recursive functional symbolism and its motivations in a simplified reconstruction of Gödel’s incompleteness proof.
  • citation-type="booksimple"

    xlink:type="simple">Shanker, S. G., ed. Gödel’s Theorem in Focus. New York: Croom Helm, 1988. Valuable collection of interpretations, principally by philosophers of mathematics, about the conceptual origins and implications of Gödel’s theorems. Written in readable style.
  • citation-type="booksimple"

    xlink:type="simple">Van Heijenoort, Jean, comp. From Frege to Gödel: A Source Book on Mathematical Logic, 1879-1931. 1967. Reprint. Cambridge, Mass.: Harvard University Press, 2002. Underscores the historical progression of the “problem of mathematical foundations.” Includes bibliography.
  • citation-type="booksimple"

    xlink:type="simple">Wang, Hao. Reflections on Kurt Gödel. Cambridge, Mass.: MIT Press, 1987. Offers very extensive and detailed biographical information and a painstakingly constructed detailed chronology of Gödel’s readings, course work, lectures, and associations, from his diaries, collected and unpublished letters and manuscripts, and original and untranslated publications.

Levi Recognizes the Axiom of Choice in Set Theory

Russell Discovers the “Great Paradox”

Brouwer Develops Intuitionist Foundations of Mathematics

Zermelo Undertakes Comprehensive Axiomatization of Set Theory

Fréchet Introduces the Concept of Abstract Space

Bourbaki Group Publishes ÉLÉments de mathématique

Categories: History