Gödel's 1931 incompleteness paper proved that his type-theoretic system P, and related systems under mild hypotheses, contain undecidable sentences and cannot prove their own consistency, while explicitly assuming rather than establishing the consistency of the systems it analyzed; a promised second part — containing the detailed proof of the second theorem, the analysis of the "true reason for incompleteness", and the study of how adjoining ever higher types makes the undecidable sentences decidable — was never written. The present statement reconstructs what later literature made of each unresolved point. The detailed second-theorem proofs were supplied by Hilbert and Bernays (1939), with compact and general treatments by Löb (1955) and Feferman (1960); the consistency of Peano arithmetic was established by Gentzen (1936) from transfinite induction up to the ordinal ε0\varepsilon_0, calibrated by Gentzen (1943), and given a second proof from computable functionals of finite type by Gödel (1958); the higher-type tradeoff was analyzed by Turing (1939) and Feferman (1962), showing that iterating the remedy never removes incompleteness. The surviving open core is the consistency of the formal systems of classical mathematics beyond arithmetic — full second-order arithmetic (classical analysis) and Zermelo–Fraenkel set theory: no constructive consistency proof of an accepted kind exists for either, their proof-theoretic ordinals are unknown, and the second theorem shows any such proof must use means not formalizable in the systems themselves. The problem asks for such a proof of the consistency of Z2\mathsf{Z}_2 and ZFC.

Background

Hilbert's program and its problem. Near the turn of the twentieth century, David Hilbert proposed to secure classical mathematics — which reasons freely about infinite totalities — by finitary means: concrete, surveyable, purely syntactic reasoning about finite strings of symbols. The centerpiece would be a finitary proof that the formal axiom systems of arithmetic, of analysis (the theory of the real numbers), and of set theory are consistent, where consistent means syntactically consistent: no formal derivation of a contradiction such as 0=10=1 exists. A consistency proof for the arithmetical axioms was Hilbert's second problem, posed in 1900; as Zach's survey recounts, the program demanded, more generally, a reduction of all of classical mathematics to finitary mathematics.

Gödel's 1931 paper. The paper proves two theorems about such systems. Its system P is the type-theoretic system of Principia Mathematica (a formalization of higher-order logic with a hierarchy of types) with the Peano axioms of arithmetic added — in effect, higher-order arithmetic. A theory is ω-consistent if it never proves both ∃n φ(n)\exists n\,\varphi(n) and the negation of φ(nˉ)\varphi(\bar{n}) for each concrete numeral nˉ\bar{n} (the notation for the individual number nn); this strengthens ordinary consistency. Satz VI (the first incompleteness theorem) states that if P is ω-consistent, then P contains undecidable sentences — sentences neither provable nor refutable in P — obtained by Gödel numbering, an effective coding of formulas and proofs as natural numbers under which the proof predicate becomes expressible in arithmetic, so that a Gödel sentence can assert its own unprovability. Satz XI (the second incompleteness theorem) states that the sentence formally expressing the consistency of P is not provable in P (assuming P is consistent). The paper is explicit about the limits of its achievement: everything is derived under the presupposition that P is consistent (a footnote states that the existence of consistent-but-not-ω-consistent systems is proved "naturally only under the presupposition that there exist consistent systems at all, i.e., that P is consistent"), and the title itself ends with "I", announcing a continuation. A footnote to the closing section announces the "true reason for incompleteness" for the planned Part II: the formation of ever higher types can be continued into the transfinite, whereas any one formal system contains at most countably many types; adjoining suitable higher types (for example type ω\omega, the type that codes truth about the lower language) makes the undecidable sentences decidable; and the analogous facts hold, Gödel adds, for the axiom system of set theory.

The arithmetic part of the agenda was completed by others. The detailed proof of the second theorem — omitted in 1931 — was supplied by Hilbert and Bernays in 1939, whose Grundlagen der Mathematik (volume II) devotes some seventy pages to establishing the derivability conditions (standard conditions on a formal provability predicate, roughly: provability of a sentence implies provability of the code of that fact; the provability predicate distributes over implication; and the provability predicate is correct about its own outputs) under which the second theorem applies to arbitrary theories; compact and completely general treatments followed. For consistency itself, Gentzen in 1936 proved the consistency of first-order Peano arithmetic (PA: the standard first-order axioms for the natural numbers, with induction for all formulas) from transfinite induction up to the ordinal ε0\varepsilon_0 — the smallest ordinal closed under α↦ωα\alpha \mapsto \omega^\alpha, the limit of 1,ω,ωω,ωωω,…1, \omega, \omega^\omega, \omega^{\omega^\omega}, \ldots — where transfinite induction means induction extended from the natural numbers to a primitive-recursively given system of notations for ordinals. Gentzen in 1943 calibrated the result: PA proves transfinite induction along every proper initial segment of the ε0\varepsilon_0-notations but not along the whole system, which identifies ε0\varepsilon_0 as the proof-theoretic ordinal of PA, the least ordinal that exactly measures how much transfinite induction the theory's consistency requires. Gödel in 1958 supplied a second consistency proof by the Dialectica interpretation: a translation of PA into a quantifier-free theory of computable functionals of finite type (higher-type primitive recursive functions), explicitly presented as an extension of the finitary standpoint of the kind the 1931 footnote had pointed toward. The strictly finitary demand is unattainable — that is what the second theorem says — so the post-Gödel standard is "constructive but stronger than the target system".

The higher-type thread became the theory of iterated extensions. Turing's 1939 ordinal logics study what happens when one repeatedly adjoins to a system the sentences that express its own soundness (Gödel sentences), indexing the iterations by recursive ordinals; the stated aim was to "avoid as far as possible the effects of Gödel's theorem", and the outcome was that no logic so obtained is complete. Feferman's 1962 transfinite recursive progressions of axiomatic theories gave the definitive general theory of such hierarchies. In modern terms the 1931 observation that adjoining type ω\omega decides the undecidable sentences is routine — a satisfaction class, i.e., a new predicate obeying the compositional truth clauses for the old language, proves the old system's Gödel sentence — but the enriched system has its own new undecidable sentence, so the regress is constitutive: no level of the hierarchy is complete.

What remains open is the part of classical mathematics beyond arithmetic. Full second-order arithmetic, Z2\mathsf{Z}_2 (also called classical analysis: the first-order theory of the natural numbers together with variables for sets of numbers and the full comprehension axiom scheme, which allows a set of numbers to be defined by any formula whatsoever, even one quantifying over the totality of all sets of numbers — impredicative comprehension), and Zermelo–Fraenkel set theory (ZFC, the standard first-order foundation of mathematics) have no consistency proof by any means that is not itself as strong as, or as questionable as, they are. The second theorem rules out internal proofs, so any proof must use means not formalizable in the target system. The relativized form of Hilbert's program therefore seeks reductions of classical theories to accepted but non-finitary constructive principles, and its most developed instrument is ordinal analysis: the assignment to a theory T of a canonical ordinal ∣T∣|T|, presented through a primitive-recursive notation system, such that (i) elementary finitary reasoning converts transfinite induction along the notations for ∣T∣|T| into a proof of the consistency of T, and (ii) T itself proves transfinite induction along the proper initial segments but not the whole, so that ∣T∣|T| calibrates the strength of T exactly. Ordinal analysis has been completed for PA (ε0\varepsilon_0), extended through the predicative fragments of analysis by the 1960s, and — after decades of work on impredicative collapsing techniques — up to subsystems of Z2\mathsf{Z}_2 around Π21\Pi^1_2-comprehension (comprehension for formulas of the form "for every set X there is a set Y such that θ", with θ containing no further set quantifiers) in the 1990s (Rathjen 1995). It has never been completed for full Z2\mathsf{Z}_2 or for ZFC: their proof-theoretic ordinals are unknown, and for ZFC it is not known whether its strength is measured by any ordinal with a recursive notation system at all. Von Plato's survey of proof theory records the state of the problem: after the consistency of arithmetic, "The next obvious task in proof theory ... was to prove the consistency of analysis", and "More than half a century has passed with no constructive proof of the consistency of full second-order arithmetic in sight."

Conventions. "Consistency" is syntactic consistency as above. "Constructive" is understood in the post-Gödel extended sense — finitary reasoning plus principles such as transfinite induction along a primitive-recursively presented well-ordering, or computation with functionals of finite type — since the second theorem proves that means formalizable in the target system cannot suffice. The target is the standard full-strength formalization of each system: a named calculus together with a standard full-strength axiom set for Z2\mathsf{Z}_2, respectively ZFC — in particular, the full impredicative comprehension scheme for Z2\mathsf{Z}_2 and the standard Zermelo–Fraenkel axioms with Choice, exactly as these systems are defined in the Background above. A restricted or weakened axiomatization whose consistency is already attainable is not the target.

Problem Statement

Gödel's 1931 paper explicitly left open, first, whether the formal systems it analyzed are in fact consistent — it proved only that their consistency cannot be established within the systems themselves — and, second, how the higher-type remedy for incompleteness trades off against the transfinite continuation of the type hierarchy, deferring both the detailed proof of Satz XI and this analysis to a continuation ("II. Teil") that was never written. The later literature closed the second thread and closed the first thread for arithmetic: the detailed second-theorem proofs were supplied by Hilbert and Bernays (1939), with compact and general treatments by Löb (1955) and Feferman (1960); the consistency of Peano arithmetic follows from transfinite induction up to ε0\varepsilon_0 (Gentzen 1936), which Gentzen (1943) showed is exactly calibrated, and Gödel (1958) reproved via computable functionals of finite type; and iterated higher-type extensions were analyzed by Turing (1939) and Feferman (1962), showing the incompleteness regress is never removed.

The surviving open problem is the analysis-and-set-theory part of the first thread. Establish the consistency of the formal systems of classical mathematics beyond arithmetic — full second-order arithmetic Z2\mathsf{Z}_2 (classical analysis) and Zermelo–Fraenkel set theory (ZFC) — by constructive means that are not formalizable in those systems (by the second incompleteness theorem, which the 1931 paper explicitly extended to the set-theoretic axioms, any proof must be external). The open question is the consistency status of Z2\mathsf{Z}_2 and ZFC: a formal inconsistency in a standard pinned formalization of either system would show that system to be inconsistent. The two consistency components are not independent: since ZFC proves the consistency of Z2\mathsf{Z}_2, and a consistent theory is Π10\Pi^0_1-sound, a constructive consistency proof of ZFC already yields one for Z2\mathsf{Z}_2 by finitary means.

References

  1. Kurt Gödel, "Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I", Monatshefte für Mathematik und Physik 38 (1931), pp. 173–198. DOI: 10.1007/BF01700692, https://doi.org/10.1007/BF01700692.
  2. Gerhard Gentzen, "Die Widerspruchsfreiheit der reinen Zahlentheorie", Mathematische Annalen 112 (1936), pp. 493–565. DOI: 10.1007/BF01565428, https://doi.org/10.1007/BF01565428.
  3. Gerhard Gentzen, "Beweisbarkeit und Unbeweisbarkeit von Anfangsfällen der transfiniten Induktion in der reinen Zahlentheorie", Mathematische Annalen 119 (1943), pp. 140–161. DOI: 10.1007/BF01564760, https://doi.org/10.1007/BF01564760.
  4. David Hilbert and Paul Bernays, Grundlagen der Mathematik II, 2nd edition, Springer, Berlin, Heidelberg, 1970 (volume II first published 1939). ISBN 978-3-642-86897-9, DOI: 10.1007/978-3-642-86896-2, https://doi.org/10.1007/978-3-642-86896-2.
  5. Kurt Gödel, "Über eine bisher noch nicht benützte Erweiterung des finiten Standpunktes", Dialectica 12 (1958), pp. 280–287. DOI: 10.1111/j.1746-8361.1958.tb01464.x, https://doi.org/10.1111/j.1746-8361.1958.tb01464.x.
  6. A. M. Turing, "Systems of Logic Based on Ordinals", Proceedings of the London Mathematical Society, series 2, 45 (1939), pp. 161–228. DOI: 10.1112/plms/s2-45.1.161, https://doi.org/10.1112/plms/s2-45.1.161.
  7. Solomon Feferman, "Arithmetization of Metamathematics in a General Setting", Fundamenta Mathematicae 49 (1960), pp. 35–92. DOI: 10.4064/fm-49-1-35-92, https://doi.org/10.4064/fm-49-1-35-92.
  8. M. H. Löb, "Solution of a Problem of Leon Henkin", The Journal of Symbolic Logic 20 (1955), pp. 115–118. DOI: 10.2307/2266895, https://doi.org/10.2307/2266895.
  9. Solomon Feferman, "Transfinite Recursive Progressions of Axiomatic Theories", The Journal of Symbolic Logic 27 (1962), pp. 259–316. DOI: 10.2307/2964649, https://doi.org/10.2307/2964649.
  10. Michael Rathjen, "Recent Advances in Ordinal Analysis: Π¹₂-CA and Related Systems", The Bulletin of Symbolic Logic 1 (1995), pp. 468–485. DOI: 10.2307/421132, https://doi.org/10.2307/421132.
  11. Toshiyasu Arai, Ordinal Analysis with an Introduction to Proof Theory, Logic in Asia: Studia Logica Library, Springer Singapore, 2020. ISBN 978-981-15-6458-1, DOI: 10.1007/978-981-15-6459-8, https://doi.org/10.1007/978-981-15-6459-8.
  12. Panu Raatikainen, "Gödel's Incompleteness Theorems", Stanford Encyclopedia of Philosophy (ISSN 1095-5054; substantive revision of 8 October 2025), https://plato.stanford.edu/entries/goedel-incompleteness/.
  13. Juliette Kennedy, "Kurt Gödel", Stanford Encyclopedia of Philosophy (ISSN 1095-5054; substantive revision of 10 September 2025), https://plato.stanford.edu/entries/goedel/.
  14. Jan von Plato, "The Development of Proof Theory", Stanford Encyclopedia of Philosophy (ISSN 1095-5054; substantive revision of 13 October 2014), https://plato.stanford.edu/entries/proof-theory-development/.
  15. Richard Zach, "Hilbert's Program", Stanford Encyclopedia of Philosophy (ISSN 1095-5054; substantive revision of 29 September 2023), https://plato.stanford.edu/entries/hilbert-program/.
  16. B. Jack Copeland, "Alan Turing", Stanford Encyclopedia of Philosophy (ISSN 1095-5054; substantive revision of 30 September 2013), https://plato.stanford.edu/entries/turing/.