Insight Editions · No. 231
Collected Works II
Publications 1938–1974
Kurt Gödel
Gödel’s later publications: the constructible universe and the consistency of the continuum hypothesis, Russell’s logic, Cantor’s continuum problem, rotating universes, and the Dialectica interpretation.
A study guide to Collected Works II by Kurt Gödel. Shared free for personal reading; not for sale and not endorsed by the authors or publishers. Please read and buy the original.
Consistency is not truth. The constructible universe makes AC and GCH consistent, but the real universe of sets, like time in a rotating cosmos, is richer than any formalism; only new axioms and new abstract concepts can reach further.
All Gödel's publications 1938 to 1974: L and the continuum, Russell, ordinal definability, rotating universes, relativity and time, the Dialectica interpretation, the undecidability remarks and infinitesimals, with 9 introductory notes.
16 items in 36 years. L is built in 8 operations. Gödel's universe: CTCs beyond r = ln(1+√2), rotation period 2 × 10¹¹ years. T proves PA consistent up to ε₀.
Readers who want the set theory, philosophy and physics of the later Gödel in one place, and anyone weighing what formal systems, AI provers and new axioms can and cannot settle.
The Book on One Page
Volume II of Gödel's Collected Works (Oxford, 1990; editor-in-chief Solomon Feferman, with John Dawson, Stephen Kleene, Gregory Moore, Robert Solovay, Jean van Heijenoort) prints every Gödel publication from 1938 to 1974, with introductory notes by Solovay, Parsons, Moore, Hawking, Stein, Troelstra, Feferman, Webb and Fenstad. Where Volume I settled what formal systems can and cannot prove, this volume asks what lies beyond them and how we could know it. Read as a whole, it is the work of a realist who builds the smallest universe of sets to show what the axioms permit, then argues that the true universe is larger, that time in physics may not flow, and that only new axioms and new abstract concepts can carry mathematics past its formal limits.
The argument of the volume, in seven moves.
- Build the minimal universe (1938 to 1940). At each stage of the cumulative hierarchy keep only the definable subsets. The resulting L satisfies ZF, the axiom of choice and the generalized continuum hypothesis, so neither can be refuted. The proof's core, condensation, became the engine of fine structure and inner model theory.
- Defend the objects (1944). Against Russell's no-class theory, classes and concepts are real objects, as legitimate as physical bodies; the vicious-circle principle is false for them, and Russell's constructivism leaves "only fragments" of logic.
- Seek absolute notions (1946). Computability is the first absolute epistemological notion; definability might be made absolute through ordinal definability, and the inner model HOD gives AC but probably not CH.
- Restate the continuum problem (1947, 1964). CH is probably independent, yet independence would not settle it: in a determinate universe CH is true or false. New axioms, justified intrinsically or by fruitfulness, must decide it; mathematical intuition is a kind of perception. Cohen confirmed the independence in 1963.
- Rotate the universe (1949, 1952). Einstein's equations allow rotating worlds with no cosmic time and closed timelike curves, and also realistic expanding rotating models; hence general relativity does not enforce Mach's principle or a global causal order, and, Gödel argues (1949a), change is not objective.
- Extend finitism (1958, 1972). Replace Hilbert's concrete intuition by computable functionals of finite type: the Dialectica translation interprets arithmetic in the quantifier-free system T, proving it consistent and seeding bar recursion, normalization and proof mining.
- Mark the limits of formalism (1972a, 1974). The second theorem in its "best and most general" form; problems of growing complexity need axioms of growing complexity; Turing's analysis limits machines but, Gödel argues, perhaps not a developing mind; and infinitesimals are "the analysis of the future".
Chapter map
| Ch | Title | One-line payload |
|---|---|---|
| 1 | The Constructible Universe: Solovay's Guide | L from definable subsets; condensation; 0#, covering, inner models, Ultimate L |
| 2 | The Announcements: 1938, 1939, 1939a | V = L as axiom; the 1939a proof via Löwenheim–Skolem + collapse |
| 3 | The 1940 Monograph | Eight operations; model Δ; AC and GCH in L |
| 4 | Parsons's Guide to 1944 | Realism about sets and concepts; the predicativity programme to Γ₀ |
| 5 | Russell's Mathematical Logic | Descriptions; vicious circle refuted; no-class theory leaves fragments |
| 6 | The Princeton Bicentennial Remarks | Absolute provability; OD and HOD; McAloon's V = HOD + ¬CH |
| 7 | Moore's Guide to the Continuum Problem | History; Gödel's changing verdicts; square axioms and ℵ₂ |
| 8 | What Is Cantor's Continuum Problem? | Iterative concept; intrinsic and extrinsic justification; thin sets |
| 9 | A Rotating Universe | The Gödel metric; nine properties; closed timelike curves |
| 10 | Relativity and Idealistic Philosophy | No objective lapse of time; Jeans answered; Stein on Kant |
| 11 | Rotating Universes in GR | ∞⁸ expanding rotating models; |
| 12 | Troelstra's Guide to Dialectica | System T; the D-translation; three models; later research |
| 13 | The 1958 Paper and the Spector Postscript | Constructive vs finitistic elements; bar recursion credit |
| 14 | The Continuum Problem, 1964 | Asymmetry with geometry; intuition as perception; Cohen |
| 15 | The 1972 Revision | Anschauung critique; accessibility; reductive proof |
| 16 | Remarks on the Undecidability Results | Outer consistency; complexity of axioms; Turing's "error" |
| 17 | Remark on Non-Standard Analysis | Infinitesimals as "the next quite natural step" |
How to read this edition. Most chapters pair an introductory note (by a specialist, written in the late 1980s) with Gödel's text. This edition gives Gödel's arguments in full, attributes each interpretation to the note's author, flags with CRITICAL LENS where Gödel or a commentator erred or was overtaken, and updates the 1990 state of knowledge to 2026 in SINCE THEN boxes. Formulas lost from the scanned source were reconstructed from the standard literature (e.g. The Gödel metric, the Dialectica clauses).
The Constructible Universe: Solovay's Guide
Robert M. Solovay's introductory note is the map for Gödel's most technically demanding achievement: the proof that the axiom of choice (AC) and the generalized continuum hypothesis (GCH) are consistent with the other axioms of set theory. He sets the history (Zermelo, Skolem, Fraenkel, von Neumann), reconstructs the proof in the conceptual form Gödel sketched in 1939a, and then follows L through fifty years of later set theory: forcing, Suslin's problem, fine structure, absoluteness, 0#, covering, and inner models for large cardinals. The core idea is a parsimonious cumulative hierarchy: at each stage add only the subsets that are first-order definable, and the resulting universe L satisfies ZF, AC and GCH because it is too thin to contain a counterexample.
What the four items are
Solovay's note covers four publications that tell one story at four levels of detail:
| Item | Form | What it gives |
|---|---|---|
| 1938 | Note in PNAS | The theorem, four consequences, the ramified-types picture, V = L as a "natural completion" |
| 1939 | Abstract | The hierarchy Mα, two models, the key lemma "by a generalization of Skolem's method" |
| 1939a | Note in PNAS | A near-complete sketch with Skolem functions and a collapse isomorphism |
| 1940 | Princeton monograph | Essentially complete proofs, "along somewhat different lines", inside a class theory |
Solovay's advice: learn the ideas from 1938 and 1939a, then read a modern text (Kunen 1980, Jech 1978, Devlin 1973) before attempting 1940.
Historical antecedents
The axiom of choice
- Cantor conjectured the well-ordering theorem: every set can be well-ordered (linearly ordered so that every non-empty subset has a least element).
- Zermelo (1904) proved it from the principle that every set X has a choice function f on its non-empty subsets with f(A) ∈ A; in 1908 he axiomatized set theory so that the proof could be carried out, with this principle as the "Axiom der Auswahl".
- Controversy. There is no obvious way to define a well-ordering of the reals, and Zermelo's proof gave none. Unlike the other set-existence axioms (each asserts that a collection explicitly definable from given parameters is a set), AC asserts existence without a definition. Zermelo knew this; many contemporaries distrusted existence proofs that exhibit no example (the history is told in Moore 1982).
- Gödel's result makes AC "safe": if ZF (with foundation, without AC) is consistent, so is ZF + AC.
- Footnote f, later knowledge: by Cohen (1963, 1964) and Feferman (1965) it is consistent with ZFC that there is no definable well-ordering of the reals at all. The worry about AC was well-founded: choice really does assert things no definition can supply.
Thought experiment: choosing socks and shoes. Russell's illustration: from infinitely many pairs of shoes you can choose one of each pair by a rule ("take the left one"); from infinitely many pairs of socks, identical within each pair, no rule distinguishes the two, so only an axiom can guarantee a choice. A well-ordering of the reals is the socks case at full scale: every attempt to describe a rule fails, and Cohen–Feferman showed that failure is not a lack of ingenuity. Gödel's L is the universe where every set wears a label (its place in the construction), so the socks become shoes and choice becomes a theorem.
The continuum hypothesis
Cantor proved (using AC implicitly) that the infinite cardinals are well-ordered, indeed order-isomorphic to the ordinals. With c the cardinal of the reals, he showed c > ℵ₀ but could not place c in the series; he conjectured c = ℵ₁ (1883): the continuum hypothesis (CH), equivalently 2ℵ₀ = ℵ₁. Hausdorff (1908) considered the generalized form, GCH: 2ℵα = ℵα₊₁ for every ordinal α. Gödel showed the axioms do not disprove CH (or GCH), so if they settle it at all, it must be a theorem; Cohen (1963) showed it is not a theorem. The same method that gives CH gives GCH at no extra cost.
Axiomatizations of set theory
Modern systems descend from Zermelo 1908, modified by Skolem and Fraenkel in four ways (Moore 1982, §4.9, traces the process).
From Zermelo 1908 to ZFC
- Pure sets. Zermelo allowed urelements (members that are not sets); modern ZF has only sets, so extensionality reads: sets with the same members are equal.
- Separation made precise. Zermelo's "definite property" ("the fundamental relations of the domain, by means of the axioms and the universally valid laws of logic, determine without arbitrariness whether it holds or not") was fine for practice but too vague for metamathematics. Skolem (1923) allowed only properties expressible in the first-order language of set theory, at a time when "first-order language" was itself a new idea.
- Foundation. Zermelo's axioms permit anomalies such as a set x = {x}; the axiom of foundation says every non-empty x has a member disjoint from x.
- Replacement. Zermelo could not prove that {Z₀, Z₁, …} exists where Z₀ = ω and Zᵢ₊₁ = P(Zᵢ), a construction natural in Cantor's naive set theory. Replacement says: if a definable property P determines a function F on all sets, then for every set a the values F(y), y ∈ a, form a set.
ZFC = Zermelo + these four changes; ZF without AC; ZC and Z without replacement.
- The cumulative hierarchy. R(0) = ∅, R(α+1) = P(R(α)), R(λ) = ⋃α<λ R(α) at limits. In ZF without foundation, foundation is equivalent to "every set lies in some R(α)"; the proof needs replacement and fails in Z or ZC. Zermelo stated the rank hierarchy clearly in 1930 (for second-order models); Mirimanoff (1917) introduced it but was not influential; von Neumann (1929) used it "in a very confusing way".
- Bernays–Gödel (BG). Gödel's 1940 uses a two-sorted theory, which he called Σ and which is now called BG or NBG, grown from von Neumann's work. Set variables range over sets; class variables over collections of sets; every set is a class, every member of a class is a set, classes with the same members are equal; proper classes such as the universal class V are "too large" to be sets. BG is finitely axiomatizable while ZF is not: each of ZF's two schemas (separation, replacement) becomes a single axiom about classes (e.g. "for every class A and set x, x ∩ A is a set"), and finitely many class-existence axioms, matching the finitely many predicates and connectives of the language, prove comprehension for every property expressible in ZF (Gödel's metatheorem M1).
- Conservativity. Mostowski: BG is a conservative extension of ZF (a sentence of ZF's language is a BG theorem iff it is a ZF theorem). BGC, with global choice (a single class function selecting from every non-empty set), is conservative over ZFC, proved about the same time by Kripke, Cohen and Solovay, later rediscovered by Felgner (1971).
- Natural models. For limit α > ω (e.g. ω + ω), R(α) ⊨ ZC. A cardinal κ is regular if not a sum of fewer than κ smaller cardinals, a strong limit if 2λ < κ for all λ < κ, strongly inaccessible if regular, uncountable and strong limit. For inaccessible Ω, R(Ω) ⊨ ZFC, and (sets R(Ω), classes all subsets of R(Ω)) ⊨ BGC. With H(λ) the sets whose transitive closure has size < λ: for regular λ > ℵ₀, H(λ) models ZFC minus power set; for strong limit λ, ZC; for inaccessible λ, H(λ) = R(λ) ⊨ ZFC. Since all this is provable in ZFC, the second incompleteness theorem implies that ZFC cannot prove an inaccessible exists (if ZFC is consistent).
Thought experiment: the first few floors. Build V by hand. R(0) = ∅; R(1) = {∅}; R(2) = {∅, {∅}}; R(3) has 4 elements, R(4) has 16, R(5) has 65,536, R(6) has 265,536. Every finite floor is finite, and R(ω), their union, is the countable set of hereditarily finite sets. Now build L by the same rule but keeping only definable subsets. On finite floors every subset is definable (list its members as parameters), so Lₙ = R(n) and Lω = R(ω). The first difference appears one floor up: R(ω+1) is all subsets of a countable set, uncountably many; Lω+1 is only the subsets definable over R(ω), and there are only countably many formulas with finitely many parameters, so Lω+1 is countable. From here on L climbs a thin staircase inside V's vast floors.
The inner-model method
Gödel defines a class of constructible sets, proves in ZF without AC that each ZF axiom holds in L, and that AC and GCH hold in L. If ZF + AC + GCH proved 0 = 1, that proof could be recast as a proof that 0 = 1 holds in L, which is a contradiction in ZF itself. Because the transformation is explicit, the result is a constructive relative consistency proof.
- Earlier model-theoretic work. Zermelo (1908): "I have not yet even been able to prove rigorously that my axioms are consistent, though this is certainly very essential"; he suspected the axioms independent but did not try to prove it. Fraenkel (1922) attempted independence proofs (of choice and separation), not in first-order terms and not to modern standards (made rigorous by Lindenbaum–Mostowski 1938). Skolem (1923), thinking first-order, studied countable models, noted that even with standard natural numbers such a model must omit some set of naturals, asked whether one could add it and still have a model (the question forcing later answered), and argued that CH is probably neither provable nor refutable.
- First relative consistency proof: von Neumann (1929) for foundation. Ackermann (1937): the consistency of number theory implies that of ZFC minus infinity (hereditarily finite sets coded as numbers).
- Dates: constructible sets and AC by 1935; CH and GCH apparently 1937 (an item in the Nachlass); compare the letter to Menger of December 1937 in Chapter 7.
Two parents of L. Solovay: Gödel combined Zermelo's rank hierarchy with Skolem's first-order perspective. Gödel himself called L the transfinite prolongation of Russell's ramified type theory (1944), and wrote to Hao Wang (7 March 1968) that constructivists could never have found the proof, because "the ramified hierarchy, which had been invented expressly for constructive purposes, has to be used in an entirely nonconstructive way": the levels run through arbitrary ordinals, which no constructivist would accept as given.
The proof, as outlined in 1939a
The constructible hierarchy
- L₀ = ∅.
- Lα₊₁ = the subsets of Lα definable by a first-order formula of set theory with parameters from Lα, quantifiers ranging over Lα (write Def(Lα)).
- Lλ = ⋃α<λ Lα for limit λ.
x is constructible iff x ∈ some Lα. The class L is not in the range of ZF's variables, but "x is constructible" is definable in ZF as ∃α (x ∈ Lα), and expressions like On ⊆ L are shorthand for statements about sets (Kunen 1980, ch. 1 §9). Compared with R(α+1) = P(R(α)), L is "far more parsimonious": stage α+1 adds only subsets that must appear in any model of set theory containing Lα. (Unlike V, new subsets of Lα can first appear later than α+1; this happens at every infinite stage.)
- "Model" with a grain of salt. For each ZF axiom, the statement that it holds in L is expressible in ZF and is a theorem of ZF. But "all of ZF holds in L" is not a single sentence of ZF, so there is no clash with the second incompleteness theorem. This understanding suffices to prove Con(ZF) → Con(ZFC + GCH).
- Absoluteness. A formula φ(x₁, …, xₙ) is absolute from a transitive class M to a transitive N ⊆ M if, for all parameters in N, φ holds in N (∈ as usual, quantifiers over N) iff it holds in M. A class X is transitive if every member of X is a subset of X; L and V are transitive.
- Checking the axioms in L is routine except for separation. The key is the reflection principle: for any formula there are many stages Lα at which it is absolute from L to Lα. So if x ∈ Lα, a subset of x defined by a formula over all of L is defined equally well over Lα, and therefore lies in Lα₊₁.
Why reflection holds (Solovay's footnote w). Given finitely many formulas Φ, closed under subformulas, with ∃ as the basic quantifier: introduce for each formula of Φ beginning with ∃ a Skolem function picking a witness. (1) If a level R(α) (or Lα) is closed under all these Skolem functions, every formula of Φ is absolute between it and V (or L). (2) By replacement, there are unboundedly many α with this closure: start anywhere, close up ω times, take the supremum. 1939a does not discuss the axioms in L, but uses the same Skolem-function idea in its Theorem 2.
Step 1: V = L holds in L
One might think this trivial: from L's point of view, the universe is L. But a set x in L may have a property (being a cardinal, being constructible) in V and lack it in L, or conversely; "is not a cardinal" can change, because L may lack the bijection that collapses x in V. The fix is to show that the Lα computed inside L are exactly the Lα computed in V, by a detailed study of which notions are absolute: forming Def(X), the set of definable subsets, is absolute; forming the full power set is not. By-product: L is the minimal transitive class model of ZF containing all ordinals, an intrinsic characterization showing how fundamental the notion is.
| Notion | Absolute between transitive models of ZF? | Why |
|---|---|---|
| x ∈ y, x ⊆ y, pairs, functions, ω | Yes | Bounded (Δ₀) definitions look only inside the sets involved |
| "α is an ordinal", α + 1, limits | Yes | Transitive and well-ordered by ∈ is Δ₀ given foundation |
| Def(X), Lα, "x is constructible" | Yes | Defined by recursion from absolute operations |
| "x is countable" | Upward only | A bijection with ω in N stays one in M; M may have one N lacks |
| "κ is a cardinal" | Downward only | A cardinal of M stays a cardinal in N ⊆ M, but may stop being one in the bigger model |
| P(x), V | No | N may contain fewer subsets than M |
Step 2: V = L implies AC
Well-order each Lα by induction. At limits, take the union of the earlier orders (with care so the union is a well-ordering). At successors: a definition of a set in Lα₊₁ is a finite sequence of symbols, each an integer (coding logic) or a member of Lα; well-order these sequences using the order of Lα; then order Lα₊₁ by putting old elements first in their old order, and new elements by their least definitions. If V = L, this is a well-ordering of the universe. (Footnote x: for AC alone, a simpler route uses Gödel's ordinal-definable sets of 1946: HOD satisfies AC.)
Step 3: V = L implies GCH
Key lemma (Theorem 2 of 1939a). If V = L, λ is an infinite cardinal and x ⊆ λ, then x ∈ Lλ⁺. Since |Lλ⁺| = λ⁺ (easy), this gives 2λ = λ⁺.
- x lies in some Lγ; enlarge γ > λ so that Lγ satisfies V = L and a fixed finite fragment T of ZF strong enough to prove the basic properties of the Lα. Between transitive set models of T, the computation of the Lα is absolute.
- Downward Löwenheim–Skolem: take an elementary submodel M ≺ Lγ of cardinality λ containing x, λ and all ordinals < λ.
- Collapse: M need not be transitive, but it is ∈-isomorphic to a transitive N (the Mostowski collapse).
- N satisfies V = L and T; by absoluteness, for ordinals δ of N, (Lδ)N = Lδ, so N = Lθ for θ the least ordinal not in N.
- The collapse is the identity on ordinals < λ (they form an initial segment of M), so it carries x to itself: x ∈ Lθ. And |θ| ≤ |N| = |M| = λ, so θ < λ⁺.
Thought experiment: the census of subsets. Ask how many subsets of ω exist in L. Each one is born at some stage; the lemma says each is born before ω₁ of L, because any subset of ω can be captured, with everything needed to define it, inside a countable elementary piece of a big level, and that piece shrinks (collapses) to some countable level. Since there are only ℵ₁ countable levels and each is countable, L holds at most ℵ₁ subsets of ω: CH. The same census one cardinal up gives 2ℵ₁ = ℵ₂, and so on. The engine is condensation: a small elementary copy of L's levels is itself a level of L.
Natural models. Gödel also notes Lℵω ⊨ ZC + GCH and, for inaccessible λ, Lλ ⊨ ZFC + GCH. These parallel the H(λ) models above; indeed, by the same arguments, if V = L then Lλ = H(λ) for every infinite cardinal λ.
Why 1940 looks so different
1939a (conceptual). ZF; Lα defined by first-order definability; GCH via Löwenheim–Skolem and collapse; the model-theoretic details passed over in silence.
1940 (monograph). BG class theory; eight fundamental operations on classes, each matching a syntactic operation (e.g. Intersection ↔ conjunction); a function F: On → V enumerating sets, whose range is closed under the operations and with F(λ) = {F(α) : α < λ} at many limits; L = range of F. Full detail, "very little motivation", and a GCH proof that obscures the link with Löwenheim–Skolem.
Solovay's guess: Gödel wanted to avoid developing the rudiments of model theory inside axiomatic set theory; 1939a passes over those portions in silence, and 1940 develops an alternative that needs no such formalization.
Descriptive set theory in L
Terminology. Work in Rⁿ (or any complete separable metric space without isolated points). The Borel sets are generated from open sets by complements and countable unions; Σ¹₁ (analytic) sets are projections of Borel subsets of Rⁿ⁺¹; Π¹₁ sets their complements; Σ¹ₖ₊₁ projections of Π¹ₖ sets; Δ¹ₖ sets both Σ¹ₖ and Π¹ₖ; projective sets those in some Σ¹ₖ.
| Class | Meaning | Regularity in ZFC |
|---|---|---|
| Borel | Generated from open sets by complements and countable unions | Measurable; perfect set property |
| Σ¹₁ (analytic) | Projection of a Borel set | Measurable; uncountable ones contain a perfect subset |
| Π¹₁ | Complement of Σ¹₁ | Measurable; perfect set property not provable |
| Σ¹ₖ₊₁ / Π¹ₖ₊₁ | Projection of Π¹ₖ / complement of Σ¹ₖ₊₁ | Undecided by ZFC from level 2 on |
| Δ¹ₖ | Both Σ¹ₖ and Π¹ₖ | |
| Projective | Σ¹ₖ for some k | Fully regular under projective determinacy |
Gödel (1938) noted two pathologies that hold in L, against the ZFC theorems (Moschovakis 1980) that every Σ¹₁ or Π¹₁ set is Lebesgue measurable and every uncountable Σ¹₁ set has a perfect subset:
- A Δ¹₂ set of reals that is not Lebesgue measurable.
- A Π¹₁ set of cardinality c with no perfect subset.
Both follow because, under V = L, the canonical well-ordering of L restricted to the reals is a good Δ¹₂ well-ordering ("good" being a technical strengthening Solovay does not stop to explain: the initial segments are uniformly Δ¹₂). Gödel gave no proof in 1939a and a few lines "comprehensible only to cognoscenti" in 1940 (a fuller one is in his handwritten lecture notes); full proofs: Novikov 1951 for the two propositions, Addison 1959 for the good well-ordering (readable accounts: Jech 1978, pp. 527–530; Moschovakis 1980, pp. 274–281).
Thought experiment: a well-ordering you can write down. In L, "real r comes before real s" can be stated as: "there is a countable level Lα, coded by a real, that is well-founded, satisfies enough of V = L, contains both r and s, and orders r first". Quantifying over codes (reals) and checking well-foundedness (a Π¹₁ condition) puts the relation at the Δ¹₂ level. From such a definable well-ordering, the classical constructions by transfinite recursion (a non-measurable set picking one point from each coset; a thin uncountable set) become projective, as Kuratowski showed. The pathologies of AC become concrete when every real has a definable rank.
After Gödel: fifty years of L
1940s: Mostowski reconstructs the Δ¹₂ well-ordering (manuscript destroyed in the war); Kuratowski shows classical AC + CH pathologies become projective in L (his work also destroyed, reconstructed as Kuratowski 1948).
1951 to 1953: Shepherdson: inner models cannot show V ≠ L is consistent, since the universe might be minimal.
Late 1950s: Hajnal, Lévy, Shoenfield: relative constructibility L[x]; AC holds in L[x], GCH in L[x] when x ⊆ ω (or x ⊆ ω₁). Lévy–Shoenfield: if GCH implied V = L, then ZF would prove V = L.
1961: Scott: a measurable cardinal implies V ≠ L. Shoenfield absoluteness: Σ¹₂ formulas are absolute between L and V.
1963 to 1966: Cohen's forcing: models with AC + GCH + V ≠ L; AC + ¬CH; ¬AC (reals not well-orderable).
1964 to 1971: Gaifman, Rowbottom: large cardinals make L small. Suslin's hypothesis independent (Jech, Tennenbaum, Solovay–Tennenbaum). Silver indiscernibles (1971); 0# (Solovay 1967).
1972: Jensen: SH fails in L via ◇; fine structure of L.
1974: Shelah: Whitehead's problem undecidable (◇ vs MA + ¬CH).
1975: Devlin–Jensen covering theorem.
1970s to 1980s: Kunen, Silver: L[D] for a measurable; Mitchell, Dodd, Jensen, Baldwin: core models.
1984: Woodin: a superstrong cardinal rules out any projective well-ordering of the reals.
Why inner models cannot refute V = L
Shepherdson's minimality argument (1951–53)
- A minimal model of ZFC (one with no proper inner model) must satisfy V = L, since L is always an inner model.
- If there are no transitive set models of V = L, then L itself can be shown minimal.
- If there are transitive set models of ZFC, building L inside one gives transitive models of the form Lδ; the least such δ gives a minimal model.
- So ZFC cannot rule out that the universe is minimal, and any method that only passes to inner models can never produce a model of V ≠ L.
A fortiori, inner models cannot answer: (a) is CH a theorem of ZFC? (b) can the reals be proved well-orderable without AC? (Mostowski, building on Fraenkel, had shown AC unprovable with urelements, which left open the case of pure sets like the reals.) The expected answers, "no", needed a new method.
The clue from L[x]. The relative-constructibility work showed: if V = L is not a theorem, there is a model L[x] with x a non-constructible set of ordinals, probably even a set of integers. Since L[x] is transparent (its sets are parametrized by ordinals), the problem became: given a countable transitive model Lδ ⊨ ZFC, find x ⊆ ω with Lδ[x] ⊨ ZFC. Choosing x to code δ itself breaks replacement, and there was no obvious way to keep replacement. Cohen's forcing solved exactly this, producing models in which (a) AC and GCH hold but some set of integers is non-constructible; (b) AC holds and CH fails; (c) AC fails and the reals cannot be well-ordered.
What forcing can and cannot do
Unlike Gödel's method, which yields one model, forcing is a flexible tool for building models of a huge variety of statements. But it enlarges a countable transitive model M to N while keeping constructibility absolute (LN = LM), so it gives no information about ZFC + V = L. Questions left open in L had to be settled by analysing L itself.
Suslin's hypothesis and ◇
SH (Suslin 1920): the real line is characterized as a linear order by (1) density (between any two points another), (2) completeness (bounded sets have least upper bounds), (3) no endpoints, (4) countable chain condition (every family of pairwise disjoint open intervals is countable). With (4′) a countable dense subset instead of (4), Cantor (1895) proved categoricity; since (4′) implies (4), SH says the weaker (4) already suffices. SH is natural in the theory of partial orders and Boolean algebras, and is equivalent to: there is no Suslin tree on ℵ₁ (an uncountable tree with no uncountable branch or antichain). It was shown independent of ZFC soon after forcing (Jech 1967, Tennenbaum 1968, Solovay–Tennenbaum 1971), which left open its status in L.
Jensen's diamond ◇ (a strong form of CH that holds in L). A set C ⊆ ω₁ is club if unbounded and containing the supremum of each of its countable subsets; S is stationary if it meets every club. ◇ asserts Aα ⊆ α (α < ω₁) such that for every S ⊆ ω₁, the set {α : Aα = S ∩ α} is stationary: a "guessing procedure" that predicts S ∩ α correctly a significant portion of the time. Analogy (Solovay): club ≈ measure 1, stationary ≈ positive measure.
Why it matters: in a construction of length ℵ₁, ◇ lets one meet ℵ₂ requirements by guessing them at stationarily many stages. With it, building a Suslin tree becomes comparatively easy: grow the tree level by level, and at stage α use Aα to guess a maximal antichain of the tree so far and seal it, so that every potential uncountable antichain is killed somewhere.
Other uses: Shelah (exposition: Eklof 1976): under ◇ every Whitehead group (abelian G with Ext(G, ℤ) = 0) of size ℵ₁ is free, while MA + 2ℵ₀ > ℵ₁ gives a non-free one, so Whitehead's problem is undecidable, an algebraic question settled by set theory.
Higher Suslin trees and fine structure. Generalize: for which regular uncountable κ is there a κ-Suslin tree? If κ is weakly compact, none exists. Jensen: under V = L, there is one for every regular uncountable κ that is not weakly compact. Unlike the ◇ argument (classical in spirit, the same ideas as the GCH proof), this required a level-by-level fine structure analysis of L: Jensen worked with a variant hierarchy with better closure, studied the exact level at which an ordinal becomes singular, and exploited "the residue of regularity that still remains just before that level". Fine structure also gives model-theoretic two-cardinal theorems in L and the covering theorem. Silver machines later gave simpler proofs of most applications (unpublished; presented in Devlin 1984, which also covers Velleman's simplified morasses).
Absoluteness
A sentence φ is absolute (in ZFC) if ZFC proves that φ holds in V iff it holds in L. Before Cohen, it could not be ruled out that every sentence is absolute.
- Arithmetical sentences are absolute: L and V have the same integers. Π¹₁ sentences are absolute too, by their link with well-ordering and because L and V have the same ordinals.
- Shoenfield (1961): Σ¹₂ formulas are absolute, the best possible; hence a Π¹₃ sentence true in V holds in L (not conversely: "every real is constructible" is Π¹₃, true in L, false in Cohen's models). This lets descriptive set theorists prove statements that do not look absolute by proving them in L.
- Kreisel's observation: any arithmetical theorem proved with AC and GCH is provable without them. Ax–Kochen (1965) on p-adic fields used ultraproducts, whose theory is much smoother under GCH; their decidability of p-adic fields is nonetheless a plain ZFC theorem.
Thought experiment: the borrowed ladder. You want to prove a statement about whole numbers. You climb a ladder made of extra assumptions (choice, GCH, even V = L), reach the result, and climb down. Absoluteness says the view from the top was the same view: whole numbers are identical in L and V, so whatever you proved about them with L's extra structure was already true without it. This is why number theorists can use set-theoretic shortcuts freely, and why Gödel's consistency results cost nothing for arithmetic.
Large cardinals and the thinness of L
Gödel's heuristic for measurables, and Solovay's doubt. In 1947 Gödel hoped large cardinals would settle CH; that has not happened, as all known ones are consistent with both CH and ¬CH. In conversation Gödel told Solovay he believed measurable cardinals exist, arguing that every strongly compact cardinal is measurable, that strongly compact cardinals exist iff some cardinal > ℵ₀ shares a certain property of ℵ₀, and that "reasonable" properties of ℵ₀ should be shared by some larger cardinal. Solovay: "I am unable to present [it] in a coherent way"; the restriction to "reasonable" is his addition "to keep the argument from being blatantly fallacious" (being the least infinite ordinal holds of ℵ₀ alone), and "I do not find this particular argument … convincing". He nonetheless believes measurables exist.
- Measurable cardinal κ: a non-trivial {0, 1}-valued κ-additive measure on all subsets of κ. Tarski 1962: κ is strongly inaccessible, indeed the κ-th inaccessible. Its existence cannot be proved in ZFC, nor its consistency derived from ZFC's (provided no false arithmetical statement is provable).
- If a measurable exists: (a) for uncountable λ, Lλ ≺ L; (b) hence every ordinal definable in L (such as ℵ₁ of L, or the third inaccessible of L) is countable in V, and there are only countably many constructible reals; every uncountable cardinal of V is a limit cardinal in L; for infinite γ there are exactly |γ| constructible subsets of γ; and the satisfaction relation of L is definable in V (contrast Tarski's undefinability of truth within L itself). Gaifman and Rowbottom did important intermediate work.
- Silver indiscernibles (1971): using Ehrenfeucht–Mostowski (1956) models (generated by indiscernibles: few types realized, many self-embeddings), Silver found a canonical class C: (1) closed unbounded in the ordinals; (2) it generates L (every constructible set is definable in L from finitely many members of C); (3) its members are indiscernible in L (increasing n-tuples have the same properties). Every uncountable V-cardinal is in C, and each member is inaccessible, Mahlo, weakly compact and more in L: every large-cardinal property compatible with V = L holds of them in L.
- 0# ("zero sharp"): the set of Gödel numbers of formulas true in L of increasing tuples from C. It codes the whole structure of L in countably many bits. It was the first natural definable non-constructible real; it is Δ¹₃ (best possible, by Shoenfield) and every constructible real is recursive in 0# (Solovay 1967). "0# exists" can be stated as ∃x φ(x) for a Π¹₂ formula φ, and already implies all the consequences of measurability for L listed above. Kunen: 0# exists iff there is a non-trivial elementary embedding L → L (compare: a measurable exists iff some j: V → M is non-trivial).
- Gödel's 1938 remark: the consistency proof for V = L survives stronger axioms of infinity (inaccessibles), so the consistency of V = L "seems to be absolute in some sense". Today: weak large-cardinal properties (inaccessible, Mahlo, weakly compact) hold in L if they hold in V, and of all Silver indiscernibles if 0# exists; stronger ones imply 0# and contradict V = L; there are no large-cardinal properties whose compatibility with V = L is unknown (dividing line through partition cardinals: Baumgartner–Galvin 1978).
Jensen's covering theorem: L is either very close to V or very far. If 0# does not exist, every set of ordinals X is covered by a constructible Y ⊇ X with |Y| ≤ max(|X|, ℵ₁). So either 0# exists and L is a very sparse subclass of V, or every set of ordinals is tightly approximated from above by a constructible one. Consequences (if 0# does not exist): GCH holds at every singular strong limit κ, and (κ⁺)L = κ⁺ for singular κ. "0# does not exist" holds in every forcing extension of L, so covering limits what forcing alone can do: getting GCH to fail first at a singular cardinal needs large cardinals (Magidor 1977 started from a huge cardinal, far beyond the first measurable, to make GCH first fail at ℵω).
Inner models for large cardinals
- L[A] for a class A: the least transitive ZF model containing all ordinals and closed under x ↦ A ∩ x (for A a set of ordinals, the earlier L[x]; even for a set, A need not belong to L[A]).
- Measures and normality. A two-valued measure is a homomorphism from P(κ) to {0, 1}; it is non-trivial if μ(κ) = 1 and singletons get 0; κ-additive if unions of fewer than κ null sets are null. Normal: every function regressive on a measure-one set is constant on a measure-one set; equivalently, in the ultrapower j: V → M, κ is the critical point and the identity function represents κ. Every measurable carries a normal measure, and normal measures give measure one to the inaccessibles below κ.
- L[D] for a measurable (D the measure-one sets of a normal measure): κ is measurable in L[D], and by Kunen (1970) L[D] depends only on κ, κ is the unique measurable there, and D ∩ L[D] is its unique normal measure. L[D] closely resembles L: GCH holds (Silver 1971a) and the reals have a good Δ¹₃ well-ordering (Silver 1971b), one level above L's Δ¹₂. Solovay's unpublished fine structure of L[D] underlies Dodd–Jensen's core model K (1981).
- Why it matters: inner models give lower bounds on consistency strength. Mitchell: if GCH can first fail at ℵω, then a measurable of high Mitchell order is consistent; the proof builds inner models for such measurables.
Large cardinals defined by embeddings j: V → M with critical point κ (M transitive; the critical point is the least ordinal moved)
- Measurable: some non-trivial j exists (the critical point of any such j is measurable).
- λ-strong: j(κ) > λ and R(λ) ⊆ M; strong: λ-strong for all λ > κ.
- Superstrong: R(j(κ)) ⊆ M.
- λ-supercompact: M closed under λ-sequences.
Kunen (1971): no non-trivial j: V → V. Consistency strength: a 2κ-supercompact gives a model with a proper class of superstrongs; a superstrong gives a model with a proper class of strongs. Mitchell (1974, 1979), Dodd, Baldwin built L-like models up to a proper class of strong cardinals, all with a Δ¹₃ well-ordering of the reals. (References: Kanamori–Reinhardt–Solovay 1978; Kanamori–Magidor 1978.)
Woodin's anti-inner-model theorem (1984). If a superstrong cardinal exists, there is no projective well-ordering of the reals (building on Foreman–Magidor–Shelah). Since every inner model then known has a Δ¹₃ well-ordering, inner models for cardinals that large must be very unlike L. Solovay's open questions in 1990: (1) where exactly the line falls between cardinals compatible with a Δ¹₃ well-ordering and those that are not; (2) if κ is κ⁺-supercompact, is there an inner model with GCH where it remains so? (Woodin had made the first measurable κ⁺-supercompact, but under GCH the first κ⁺-supercompact has κ measurables below it, so a positive answer needs an inner model theory for supercompacts of a kind Woodin's theorem does not exclude.) His summary: "almost all of the natural questions raised by Gödel's work on L have by now been settled. However, the topic of L-like models for large cardinals is still rife with mystery."
Inner model theory since 1990. Martin–Steel (1989, 1994) and iteration trees produced fine-structural inner models (mice) with Woodin cardinals; projective determinacy follows from infinitely many Woodins, and the minimal model Mₙ with n Woodin cardinals has a good Δ¹ₙ₊₂ well-ordering of the reals, a precise answer in the spirit of Solovay's question (1). Mitchell–Steel (1994), Steel's core model below a Woodin (1996), Neeman, Schimmerling and others extended the theory; Steel and Woodin showed that, under determinacy, HOD of L(ℝ) is itself a fine-structural model below Θ. Woodin's HOD dichotomy and Ultimate L programme (2010s) conjecture an L-like model compatible with supercompact cardinals, which would answer question (2); "V = Ultimate L" would imply CH. Goldberg's Ultrapower Axiom (2022) gives a rival structural approach, proving much of what an Ultimate L would provide. Asperó and Schindler (2021, Annals of Mathematics) proved Martin's Maximum⁺⁺ implies Woodin's (*), uniting two competing axioms that both make 2ℵ₀ = ℵ₂. Gödel's L remains the template every one of these models generalizes.
The inner-model pattern in system design. Gödel proved AC "safe" by finding a sub-universe built only from what is explicitly definable, then showing every rule still holds there. Architects use the same move to de-risk contested assumptions: build a minimal, fully specified sub-environment (a reference implementation, a golden dataset, a sandbox with only declared dependencies), show the requirements hold there, and any contradiction in the full system must already exist in the minimal one. Shepherdson's lesson is the converse warning: a minimal environment can show that an assumption is safe, but never that its negation is.
The Announcements: 1938, 1939, 1939a
Gödel announced his set-theoretic results three times before the full monograph. The 1938 note in the Proceedings of the National Academy of Sciences states the theorem and two descriptive-set-theory pathologies; the 1939 abstract defines the hierarchy Mα and the key lemma; 1939a, also in PNAS, gives a nearly complete sketch built on Skolem functions and an explicit collapse isomorphism. The 1938 note also contains Gödel's most quoted, and later most doubted, sentence: the axiom "every set is constructible" seems to give "a natural completion of the axioms of set theory".
1938: the theorem and the model
Theorem (1938). Let T be von Neumann's set theory S* (1929) without choice (Axiom III3* replaced by III3). If T is consistent, it stays consistent when these are added simultaneously:
- The axiom of choice (von Neumann's III3*).
- GCH: 2ℵα = ℵα₊₁ for every ordinal α.
- Non-measurable sets: linear sets that are not Lebesgue measurable, such that both they and their complements are one-to-one projections of plane complements of analytic sets (hence B₂-sets in Luzin's terminology; Δ¹₂ in modern notation).
- Thin co-analytic sets: linear complements of analytic sets with the power of the continuum and no perfect subset.
The same holds if T is the system of Principia mathematica (as formulated by Tarski 1933) or Fraenkel's system, without choice but with the axiom of infinity.
- A constructive relative proof. "If a contradiction were obtained in the enlarged system, a contradiction in T could actually be exhibited." Footnote 5: the model is built by "essentially transfinite methods", so the proof is only relative, requiring Con(T) as hypothesis.
- "Constructible" in a semi-intuitionistic sense. The model "consists of all 'mathematically constructible' sets", constructible in a sense that "excludes impredicative procedures": the sets obtainable by Russell's ramified hierarchy of types, extended to transfinite orders.
- Why the impredicative axioms come out true. The transfinite extension makes "an axiom of reducibility" provable "for sufficiently high orders": every set of integers definable at any order is already present at some countable order, so quantifying over "all sets of integers" no longer outruns the hierarchy.
- Proposition A, "every set is constructible" (today V = L), is true in the model and so consistent with T; propositions 1 to 4 follow from A.
- The source of GCH: "all constructible sets of integers are obtained already for orders < ω₁, all constructible sets of sets of integers for orders < ω₂, and so on." Since there are only ℵ₁ orders below ω₁, each contributing countably many sets, there are at most ℵ₁ sets of integers.
Thought experiment: Russell's hierarchy taken to infinity. Russell built properties in orders: order 1 mentions only individuals; order 2 may quantify over order-1 properties; and so on, to avoid defining a property by reference to a totality containing it. He needed the axiom of reducibility to recover ordinary mathematics, and could not justify it. Gödel keeps climbing: order ω, ω + 1, …, through all ordinals. At order ω₁ the climb catches up with itself for sets of integers: nothing new about integers can be defined later. Reducibility, an axiom for Russell, becomes a theorem at transfinite height. The price is the step a constructivist will not take: the orders run through ordinals that cannot be constructed.
"The proposition A added as a new axiom seems to give a natural completion of the axioms of set theory, in so far as it determines the vague notion of an arbitrary infinite set in a definite way." Gödel, 1938
- The closing caution. "It is important that the consistency proof for A does not break down if stronger axioms of infinity (e.g., the existence of inaccessible numbers) are adjoined to T. Hence the consistency of A seems to be absolute in some sense, although it is not possible in the present state of affairs to give a precise meaning to this phrase."
A view Gödel abandoned. Here V = L looks like a candidate axiom; by 1947 Gödel argued that CH is probably false and that V = L is a minimality principle at odds with the concept of an arbitrary set (Chapter 7). Martin Davis takes the 1938 remark as evidence that Gödel's platonism about sets evolved gradually. The "absoluteness" hope was also overturned: it holds for inaccessibles and Mahlo cardinals (they relativize to L), but measurable cardinals refute V = L (Scott 1961), and every stronger large cardinal does so emphatically (Chapter 1).
1939: the abstract
- The hierarchy: M₀ = ∅; Mα₊₁ = subsets of Mα definable by propositional functions using only ¬, ∨, ∈, elements of Mα and quantifiers over Mα; Mβ = ⋃α<β Mα at limits.
- Two models: Mωω for set theory (Fraenkel, von Neumann, Skolem, Bernays) without the axiom of substitution (replacement), MΩ (Ω the first inaccessible) with it; GCH is true in both. Since the construction can be formalized within set theory, 2ℵα = ℵα₊₁ is consistent if set theory is.
- The lemma: "Any subset of Mωα which is an element of some Mβ is an element of Mωα₊₁", proved by "a generalization of Skolem's method for constructing enumerable models".
- AC is a by-product: not used in building the models, but true in them, so its consistency is "obtained as an incidental result".
A small puzzle about the two models. Why MΩ, which needs an inaccessible, if Gödel wants consistency relative to plain set theory? Because the abstract states the result in terms of set models; when the argument is formalized inside set theory, the whole class of constructible sets can play the role of MΩ (as it does in 1940), so no inaccessible need be assumed. 1939a footnote 13 also notes that without replacement Mωω itself cannot be proved to exist (it contains sets of infinite type), so one uses an isomorphic image with another relation in place of ∈.
1939a: the sketch with Skolem functions
Definitions of 1939a
- Propositional function over M (M any domain with a relation ∈): an expression built from variables ranging over M, constants naming elements of M (it is assumed a symbol can be introduced for each), ∈, ¬, ∨ and quantifiers over M. M′ = the set of subsets of M defined by such functions with one free variable.
- Functions in M: f with s arguments is "in M" if defined and M-valued on all s-tuples from M.
- Skolem functions for φ and a: for φ(x) in prenex form ∀x₁…∀xₙ∃y₁…∃yₖ∀z…, functions f₁, …, g₁, … in M producing witnesses for each existential quantifier from the preceding universal ones; φ(a) holds iff Skolem functions for φ and a exist.
- M₀ = ∅, Mα₊₁ = (Mα)′, Mβ = ⋃ Mα. x is constructible if x ∈ some Mα, of order α if x ∈ Mα₊₁ − Mα. Immediately Mα ⊆ Mβ and Mα ∈ Mβ for α < β.
- Theorem 1: x ∈ y implies order(x) < order(y).
- A well-ordering of the constructible sets, a unique "definition" φα for each set, and, for each true φα(a), designated Skolem functions (after first fixing an equivalent prenex form for each φα).
Theorem 2, step by step
Theorem 2: any constructible m ⊆ Mωμ has order < ωμ+1. (A constructible set all of whose elements have orders < ωμ has order < ωμ+1.)
Define the least triple K (constructible sets), O (ordinals), F (Skolem functions) satisfying:
- I. All of Mωμ is in K, and m ∈ K.
- II. The order of every x ∈ K is in O.
- III. All constants in the definition of x ∈ K are in K.
- IV. For α ∈ O and φα over Mα with constants in K: (1) the subset of Mα defined by φα is in K; (2) for each y ∈ K ∩ Mα, the designated Skolem functions for φα and y (or for ¬φα and y) are in F.
- V. K is closed under the functions in F.
- VI. If x ≠ y are in K, the first element (in the well-ordering) of the difference is in K.
- VII. Minimality: no proper subsets satisfy I to VI.
Theorem 3 (from VI and Theorem 1): distinct x, y ∈ K of order ≤ α are separated by some z ∈ K of smaller order. Theorem 4: |K + O + F| = ℵμ, since |Mωμ| = ℵμ and closing under the countably many operations II to VI adds no cardinality.
Theorem 5: the collapse. With η the order type of O and ᾱ the image of α under the order-isomorphism of O onto η, there is a one-to-one map x ↦ x′ of K onto Mη with x ∈ y ↔ x′ ∈ y′, carrying elements of order α to sets of order ᾱ. Built by transfinite induction on the order: given an isomorphism f of K ∩ Mα onto Mᾱ, extend it to g on K ∩ Mα₊₁:
- Map each definition φα over Mα with constants in K to φ̄α over Mᾱ by replacing constants a by a′ and quantifier ranges Mα by Mᾱ.
- Theorem 6: for x ∈ K ∩ Mα, φα(x) ↔ φ̄α(x′). If φα(x) holds, its designated Skolem functions are in F (IV.2), are functions in K ∩ Mα (V), and f carries them to Skolem functions for φ̄α and x′, because f preserves ∈; so φ̄α(x′). The converse is the same argument with ¬φα.
- Every element of K ∩ Mα₊₁ is defined by such a φα (by III if new; by "x ∈ b" if old). So g is defined, and: A single-valued (same set, same image, by Theorem 6); B x ∈ y ↔ x′ ∈ g(y); C one-to-one (Theorem 3 gives a separating z); D extends f; E maps K ∩ Mα onto Mᾱ and the new elements onto Mᾱ+1 − Mᾱ; F preserves ∈ (by B, D and Theorem 1).
- Since all ordinals below ωμ lie in O, ᾱ = α for them, and x′ = x for x ∈ Mωμ.
Conclusion. m′ ∈ Mη with η < ωμ+1 (by Theorem 4, |η| ≤ ℵμ); and x ∈ m ↔ x ∈ m′ for x ∈ Mωμ, so m = m′ ∩ Mωμ, an intersection of two sets of order < ωμ+1, hence itself of order < ωμ+1. This is the Mostowski collapse, years before Mostowski.
Theorems 7 to 10: from the lemma to consistency
- Theorem 7: Mωω satisfies all of Zermelo's axioms (except perhaps choice), and MΩ also satisfies substitution, with "definite property" read as "propositional function over the class of all sets". Sketch: extensionality and the like are trivial; infinity holds by Z = Mω; the existence axioms III to V say some x satisfies a propositional function over Mωω, so such an x lies in Mωω+1, and Theorems 1 and 2 show its order is in fact below ωω; substitution in MΩ the same way.
- Theorem 8: with A = "there are no non-constructible sets", R = choice, C = GCH: A → R (the constructible sets can be well-ordered) and A → C (by Theorem 2, every subset of Mωα lies in Mωα₊₁, which has power ℵα₊₁).
- Theorem 9: every element of Mωω (respectively MΩ) is constructible relative to the model, so A is true in it. Two facts: (1) the operation M ↦ M′ is absolute: computed inside the model it gives the same result; (2) the set of all Mβ (β < α) is constructible-in-the-model, by induction on α.
- Theorem 10: R and C are true in the models, since Theorem 8 is provable in set theory. Everything can be formalized (with slight modifications) in set theory without choice, so a contradiction from C, R, A would yield one without them.
- Footnote 12: to give A an intuitive meaning, read "sets" as all objects obtained by building the simplified hierarchy of types on an empty set of individuals, through arbitrary transfinite orders.
Thought experiment: shrinking a library. Picture L as an infinite library whose books are sets, each shelved at the stage it was first defined. You hold one book, m, about the first ℵμ shelves. Gather m, every book it cites, every book needed to define those, every "witness" book that backs up an existential claim in a definition, and the first book separating any two you hold. You end with a collection of size ℵμ. Now re-shelve it with no gaps, preserving the citation structure: the result is an exact copy of an initial segment of the library, and m sits on a shelf numbered below ωμ+1. Nothing about m changed; only the empty shelves disappeared. That is condensation.
1938. Statement, four propositions, the ramified-types picture, V = L as a "natural completion".
1939. Mα hierarchy, two models (Mωω, MΩ), the key lemma via Skolem's method.
1939a. Full architecture: Skolem functions, the closure K, O, F, the collapse isomorphism, absoluteness of M ↦ M′, the formalization. Solovay's recommended starting point.
Since then. The 1939a argument is exactly the modern condensation lemma: if X ≺ Lα then the transitive collapse of X is some Lβ. Jensen's fine structure refines it level by level (Σₙ-condensation for the J-hierarchy), and it is the template for condensation in mice, the key property that makes fine-structural inner models (Chapter 1) behave like L. Condensation is now also studied as a principle that can hold beyond L: Friedman and Holy (2011) formulated "local club condensation", consistent with very large cardinals, as part of the search for L-like models of strong axioms.
Announce the invariant, then the mechanism. Gödel's three short notes each state the guarantee first (relative consistency, constructively transformable contradictions) and only then the construction. For architecture and risk documents the same order works: lead with what is guaranteed and under which assumptions, then the mechanism, then the full proof for those who need it.
The 1940 Monograph: Consistency of AC and GCH with the Axioms of Set Theory
Based on Gödel's autumn 1938 IAS lectures (notes by George W. Brown) and published by Princeton in 1940, the monograph proves the consistency results in full detail inside the class theory Σ (Bernays–Gödel). It replaces logical definability with eight fundamental operations on classes, enumerates the constructible sets by a function F on the ordinals, proves every axiom absolute for the model Δ, shows V = L holds in Δ, and derives AC and GCH from V = L. Its technique is purely algebraic (closure under operations, isomorphism of closed sets of ordinals), which avoids formalizing model theory inside set theory at the cost of hiding the idea, as Solovay notes. Later notes record Cohen's 1963 independence proof and the new large cardinals.
Introduction: what is proved
If a contradiction could be derived in Σ from the axiom of choice and GCH, it could be transformed into one from the axioms of Σ alone. Gödel builds within Σ, using only its primitive terms and axioms, a model Δ such that (1) "the axioms of Σ hold in Δ" are theorems of Σ, and (2) "AC and GCH hold in Δ" are theorems of Σ.
- The system Σ includes substitution (replacement, Fraenkel 1927) and Fundierung (foundation, Zermelo 1930), excludes choice, is "essentially due to P. Bernays (1937)", and is equivalent to von Neumann's S* + VI (1929) without choice.
- A stronger proposition. Δ satisfies "a much stronger proposition" with other consequences (V = L itself). 1951 note: it implies a projective well-ordering of the reals whose set of pairs is PCA (Σ¹₂): consider pairs of relations s, e on the integers isomorphic, for some γ < ω₁, to (<, the membership pattern among the F′α) restricted to γ. This class can be defined directly by recursive postulates analogous to those defining F (Dfn 9.3), with quantifiers only over integers and reals, which fixes its projective level by "counting the changes of sign" of the real quantifiers (consequences: Kuratowski 1948).
- Not a formal system but an axiomatic theory. Theorems are written in logical symbols, but their meanings are presupposed; formalization in Hilbert's engerer Funktionenkalkül is routine.
- Metamathematics only as a shortcut. The general existence theorem (M1) and the notions of relativization and absoluteness are metatheorems that show how infinitely many proofs go. Since only finitely many instances are needed for properties (1) and (2), they could be dropped (footnote 2: inductions only up to about 20 are used in 1.16, M1, M2).
- Sources. Chapters II to IV develop set theory without full proofs where they "can be literally transferred" from ordinary set theory; von Neumann (1928a) gave a similar axiomatic treatment.
Chapter I: the axioms of Σ
Primitives: class (Cls), set (𝔐), and ∈ between any combination of classes and sets. Capital variables X, Y, Z range over classes, lower-case x, y, z over sets. Classes are Zermelo's "definite Eigenschaften", but Σ states explicitly, by group B, how they are built; and classes double as relations (A relates x to y if the pair (x, y) ∈ A).
The axiom groups
- Group A (A1 to A4): every set is a class; every member of a class is a set (so a proper class such as V is never a member: "B ∈ X is then always false, but meaningful"); extensionality for classes (a class with the same members as a set is that set); pairing {x, y}.
- Group B (B1 to B8), class existence: B1 ∈-relation (a class of pairs (x, y) with x ∈ y); B2 intersection; B3 complement; B4 domain; B5 direct product (essentially V × A); B6 to B8 inversions (converse of pairs and permutations of triples). The classes in B2 to B4 are unique (A · B, −A, 𝔇(A)); those in B1, B5 to B8 are not, since nothing is said about non-pairs.
- Group C, set existence: C1 infinity (a non-empty a where every x ∈ a is a proper subset of some y ∈ a); C2 union (a set including the sum of members of x); C3 power set (a set including all subsets of x); C4 substitution (the image of a set under a single-valued class is a set; 1951: now called replacement). Zermelo used Aussonderung instead.
- Axiom D, foundation: every non-empty class A has a member with no members in common with A. Proved consistent by von Neumann 1929; "not indispensable, but it simplifies considerably". Consequences 1.6 ¬(x ∈ x) (apply D to {x}) and 1.7 no 2-cycles x ∈ y ∈ x (apply D to {x, y}). Footnote 6: equivalent to no infinite descending ∈-sequences representable by sets of the system.
- Axiom E, choice: a single class A selecting an element from every non-empty set (global choice). Gödel stresses its strength: it gives a well-ordering of the whole universe; its consistency implies that of weaker forms. Theorems needing E are starred.
Σ = A + B + C + D. Differences from Bernays 1937: Bernays does not identify sets with co-extensive classes, and has an axiom for the class of all {x} that lets B7 and B8 merge. The concise form of D is Bernays's.
Basic definitions (1.1 to 1.3). The unordered pair {x, y}; the singleton; the ordered pair (x, y) = {{x}, {x, y}} with Theorem 1.13 (equal pairs have equal components, Bernays 1937); triples (x, y, z) = (x, (y, z)); n-tuples by iteration (1.15, 1.16); inclusion and proper inclusion; emptiness; mutually exclusive classes; 𝔘n(X), X is one-many (single-valued).
Chapter II: existence of classes and sets
M1, the general existence theorem. A primitive propositional function (ppf) is a formula containing only variables, symbols for particular classes, ∈ and logical operators, with all bound variables ranging over sets (defined recursively from atoms Π ∈ Γ by ¬, ∧ and ∃x). For every ppf φ(x₁, …, xₙ) there is a class A with (x₁, …, xₙ) ∈ A ↔ φ(x₁, …, xₙ). This is how finitely many class axioms yield comprehension for every set-quantified formula, the BG counterpart of ZF's infinitely many separation instances.
How M1 is proved (induction on the number of logical operators).
- Preliminaries. B2 and B3 give the universal class V and the null class 0 (2.1, 2.2). From B5 to B8: theorems 2.3 to 2.8 that let one add dummy coordinates (2.4, 2.41), drop or permute coordinates (2.5 to 2.7), and take the domain over the last coordinate (2.8). Contexts Aᵢ ∈ Γ can be eliminated (A2: Aᵢ is a set; A3: equality by co-extension), so a particular class never stands left of ∈.
- Atomic case xᵣ ∈ xₛ. If r = s, take 0 (by 1.6). Otherwise B1 (or B1 then the converse B6) gives a class F of pairs with (xₚ, xq) ∈ F ↔ xₚ ∈ xq; then 2.6, 2.5, 2.41 pad and permute it to an n-ary class A.
- Atomic case xᵣ ∈ Aₖ. By 2.3 (or B5 when r = n) there is F with (xᵣ, xᵣ₊₁) ∈ F ↔ φ; pad as before.
- ¬ψ: take the complement −B (B3). ψ ∧ χ: take the intersection B · C (B2). ∃x θ: take the domain 𝔇(D) (B4, via 2.8).
M1 is a metatheorem: a theorem about Σ that shows once and for all how the formal derivation goes for any given ppf.
- From ppf to normal formulas (M2). Defined symbols come in four kinds: particular classes (0, V, …), notions (relations like ⊆), operations (like A × B) and kinds of variables (ranges given by notions). A notion or operation is normal if it is equivalent to a ppf; a variable is normal if its range is a class; a propositional function is normal if it uses only normal notions, operations and bound variables. M2: every normal propositional function is equivalent to a ppf (eliminate class-variable quantifiers by restricting to the range class, notions by their defining ppfs, and operations by unfolding u ∈ 𝔅(Γ₁, …) into a ppf), so M1 applies. M3 generalizes to class parameters X₁ … Xₖ.
- Extending operations to classes (3.1). To keep the metamathematics simple, every notion and operation is defined for all classes as arguments: e.g. {X, Y} is {X, Y}, {X}, {Y} or 0 according as both, one or neither is a set. 1951 footnotes: how such operations behave on proper classes "is absolutely unimportant"; and a missing set condition in Dfn 4.65, pointed out by W. L. Duda, is repaired.
- Relations and functions (M4 to M6). M4: a unique n-adic relation for each normal φ (intersect with Vⁿ, by the extensionality principle 4.22). M5: a unique function over B given by a normal term. M6: definition by cases over mutually exclusive domains.
- The operations. A × B (4.1), Vⁿ, relations (Rel), E (the ∈-relation, 4.3) and I (identity), converses (4.4 to 4.412) matching B6 to B8, X + Y and X − Y, domain of values 𝔚(X), A ↾ B (A confined to B), image B″X, composition, one-to-one, functions, A′x (the unique value, or 0 if none or many), five auxiliary functions P₁ to P₅ (projections and pairings), sum 𝔖(X), power class 𝔓(X), with monotonicity and distributivity laws (4.85 to 4.96).
- Sets from sets (§5). 5.1: the image of a set under any class is a set (by C4). Then: subclasses of sets are sets (5.12); power and union of sets are sets (5.121, 5.122); x + y and x × y (5.13, 5.18, via x × y ⊆ 𝔓𝔓(x + y)); the domain of a function on a set is a set (5.19, 5.2); V is not a set (5.31: else V ∈ V); a one-to-one image of a proper class is proper (5.44).
- 1951 correction (footnote 14): the claims that well-ordering (We) and equinumerosity (~) are not normal are wrong as stated, since normality depends on extension, not on the chosen definition. All one can say is that this proof method does not show them normal; with choice they can be shown normal (von Neumann 1929), and the class quantifier in Dfn 6.2 can be replaced by a set quantifier.
Chapters III and IV: ordinals and cardinals
- Orderings (§6). Connex, transitive, asymmetric relations; X is well-ordered by Y if connex and every non-empty subclass has a first element (6.2; not normal because of the class quantifier); 6.21: a well-ordering is transitive and asymmetric. R-sections (closed downward), segments generated by an element (6.31), 6.33: in a well-ordering every proper section is a segment. Isomorphisms with respect to relations (6.4, 6.41).
- Ordinals, von Neumann style. "The ordinal α will be the class of all ordinals less than α": 0 = ∅, 1 = {0}, 2 = {0, 1}, ω = the set of integers. Definition 6.6: X is an ordinal if it is complete (transitive: every member of a member is a member) and ∈ is connex on it; by Axiom D these weak conditions suffice (6.7: ∈ then well-orders X and each element equals the segment it generates; Bernays and R. M. Robinson 1937 had shown related simplifications). An ordinal that is a set is an ordinal number; On is their class.
- Comparability and On (§7). 7.1, 7.11: a complete proper subset of an ordinal is a member of it. 7.12: for ordinals X, Y exactly one of X ∈ Y, X = Y, Y ∈ X. 7.14: members of ordinals are ordinals. 7.161: On is well-ordered by ∈, licensing transfinite induction for normal properties. 7.17, 7.2: On is not a set (Burali-Forti), and On is the only ordinal that is not an ordinal number. 7.3: the union of a set of ordinals is its sup (maximum or limit). Successor α + 1 = α ∪ {α}; ordinals of the first kind (successors or 0) and second kind (limits).
- Transfinite recursion (7.5). For any function G there is a unique F over On with F′α = G′(F ↾ α): take the class K of all "attempts" f defined on some ordinal and satisfying the recursion there; any two agree on their common domain; their union F is the desired function, and its domain cannot be a set, or F could be extended by one more step.
- Isomorphism to On (7.62, 7.7). Two ordinals isomorphic under ∈ are equal (a strictly monotone map satisfies H′α ≥ α). 7.7: a well-ordered proper class whose proper sections are all sets is isomorphic to On; a well-ordered set is isomorphic to an ordinal number. With choice (*7.71), every set is a one-to-one image of an ordinal.
- The canonical ordering R of On² (7.8, 7.81): order pairs by max(α, β), then lexicographically. 7.811: every proper R-section is a set (the predecessors of (α, β) lie in (max + 1)²). Hence (7.82, 7.9) a canonical isomorphism P: On² → On, the pairing function used later.
- Cardinals (§8). Equinumerosity; the cardinal of a set as the least ordinal equinumerous to it (*8.2, von Neumann 1928a); *8.28 and Schröder–Bernstein (here via choice); finite and infinite (8.48); ω as the set of ordinals of the first kind all of whose predecessors are of the first kind (8.4), with induction (8.44) and recursion on integers (8.45); ω exists by C1 (8.51) and is a limit (8.52, 8.53); Cantor's theorem (*8.32); the cardinals form a proper class (*8.33); ωα, ℵα via the isomorphism N of On onto the infinite cardinals (*8.56 to *8.59).
- *8.62, *8.621: ωγ² ≅ ωγ, so x² ~ x for every infinite set x, proved through the canonical pairing P by induction on γ.
- 8.7 to 8.73, the closure lemma: the closure of a set X under finitely many single-valued relations and triadic relations exists, is a set, and if X is infinite has the same cardinality as X (build G that adds all images, iterate ω times by 8.45, take the union; each step preserves |X| by x² ~ x). This is the algebraic form of the downward Löwenheim–Skolem step.
Chapter V: the model Δ
"Constructible sets are those which can be obtained by iterated application of the operations given by Axioms A4, B1–8, modified so that they yield sets if applied to sets. In addition, at certain stages of this generating process the set of all previously obtained sets will be added as a new constructible set. This permits the generating process to continue into the transfinite."
The eight fundamental operations (from axioms A4, B1 to B8, made to yield sets on sets)
- 𝔉₁(X, Y) = {X, Y} (pairing, from A4)
- 𝔉₂(X, Y) = E · X (the ∈-pairs inside X, from B1)
- 𝔉₃(X, Y) = X − Y (difference, from B3; intersection is X − (X − Y), so B2 needs no operation)
- 𝔉₄ to 𝔉₈: X intersected with a set obtained from Y by one of the class-forming steps of axioms B4 to B8: an image Qᵢ″Y under fixed relations Qᵢ that implement the domain (inverse of the second projection), the direct product, and the inversions/permutations of pairs and triples.
The factor X in 𝔉₂ to 𝔉₈ keeps results inside a given set (used in Theorem 9.5). Each sends sets to sets (by 5.11).
Operations versus formulas. In 1939a, Lα₊₁ = Def(Lα): all subsets definable by formulas. In 1940, there are no formulas in the construction at all: the eight operations play the role of the logical building blocks (∈, ¬ as difference, ∃ as domain, variable management as product and permutations), and M1 guarantees that closing under them captures every set-quantified definition. The operations survive today as the Gödel operations, which generate exactly the rudimentary functions of Jensen's fine structure, and L = closure of the ordinals under the Gödel operations in a suitable sense.
The enumeration F of the constructible sets.
- Ordering S on 9 × On² (triples (i, α, β), i < 9): by max(α, β), then the canonical R on pairs, then i (9.2). Every proper section is a set, and 9 × On² is not, so by 7.7 (9 × On², S) ≅ (On, ∈): this is J (9.21). Its nine slices J₀, …, J₈ over On² have disjoint ranges covering On (9.23; in fact Jᵢ(α, β) = 9·P(α, β) + i, the residue classes mod 9). Inverse functions K₁, K₂ recover α, β from γ = Jᵢ(α, β), with K₁γ, K₂γ ≤ γ (9.25).
- *9.26, *9.27: Jᵢ(α, β) has no larger cardinality than (max(α, β) + 1)², so indexing adds no new cardinalities, and ωα ∈ range(J₀) with J₀(ωα, 0) = ωα: every initial ordinal is a "collecting" stage. (Choice is not needed for α = 0.)
- Definition 9.3 (transfinite recursion): F′α = F″α (the set of all earlier values) if α ∈ range of J₀; F′α = 𝔉ᵢ(F′K₁α, F′K₂α) if α ∈ range of Jᵢ, i = 1 to 8. Existence via 7.5 and M6, with a function G defined by cases.
- 9.31 to 9.35 restate this: F′J₁(β, γ) = {F′β, F′γ}, F′J₂(β, γ) = E · F′β, …, F′J₀(β, γ) = F″J₀(β, γ).
- 9.4: L = range of F (the constructible sets). 9.41: a class is constructible if its members are constructible and its intersection with every constructible set is a constructible set. 9.421: Od′x, the least α with x = F′α, is the order of x.
- 9.5: F″α is transitive (complete): every element of F′α appears earlier. Hence 9.51: L is transitive; 9.52: x ∈ y implies Od′x < Od′y (as in 1939a Theorem 1).
- 9.6 to 9.66: L is closed under the fundamental operations, intersection, pairs and ordered pairs (9.62: (x, y) ∈ L ↔ x, y ∈ L). 9.63: every set of constructible sets is included in a constructible set (pick α ∈ range J₀ above all their orders; F′α = F″α), so (9.64) a constructible class that is a set is a constructible set.
- 9.8 to 9.92: constructible classes are closed under the class operations: 0, L itself (9.81), E · L (9.82), differences (9.83), intersections, domains, products and permutations (9.84 to 9.873, using least-order originals for images), A″x (9.91) and pairs (9.92). Not every operation preserves constructibility: it cannot be shown that 𝔓(x) ∩ L behaves, nor that V is absolute.
Thought experiment: a nine-lane production line. Picture an infinite conveyor indexed by the ordinals. Each position γ belongs to one of nine lanes (γ mod 9). Lane 0 is a collector: when position γ comes up, it boxes everything produced so far. Lanes 1 to 8 are machines: each takes the products at two earlier positions K₁γ and K₂γ and applies its operation (pair them, keep the ∈-pairs, take a difference, take an image under a fixed relation). Because the pairing J visits every pair of earlier positions infinitely often, every machine eventually gets to work on every pair of products. L is everything that ever comes off the line, and at each infinite cardinal ωα the collector boxes exactly the first ωα products.
Chapter VI: relativization and absoluteness; the axioms hold in Δ
- The model Δ: "class" means constructible class, "set" means constructible set, and ∈ is restricted to them.
- Relativization: replace class variables by constructible-class variables, set variables by constructible-set variables, ∈ by ∈ₗ, and defined concepts by their relativized versions (leaving logical symbols, including =, alone). A relativized concept need not exist a priori, and may depend on the chosen definition, until the axioms are shown to hold in Δ. 10.1: relativized classes and operations yield constructible classes.
- Absoluteness (Dfn 10): a class, operation or notion is absolute if its relativization exists and coincides with the original on constructible arguments; a variable is absolute if its relativized range is the same. 10.11: absolute classes are constructible.
- The first absolute notions (10.12 to 10.24): ∈ (by definition), ⊆ (10.13, which gives the relativized extensionality 10.131), proper inclusion, emptiness, exclusiveness, the pair {X, Y} (10.17), composition of absolute operations is absolute (10.18), ordered pairs and triples (10.19, 10.20), single-valuedness (10.21), being a set and being a proper class (10.22, via 9.64), Vₗ = L (10.23: the relativized universe is L), and 0 (10.24). Not provably absolute: the power class 𝔓 and V itself.
All axioms of Σ hold in Δ (Chapter VI). Since every notion in the axioms is absolute, each relativized axiom is obtained just by restricting variables to constructible ones; then a witness is exhibited:
- A1ₗ by 9.65; A2ₗ from A2; A3ₗ by 10.131; A4ₗ: {x, y} is constructible (9.6).
- B1ₗ: E · L (9.82); B2ₗ: A · B (9.84); B3ₗ: the relativized complement is L − A (9.83, 9.81); B4ₗ: 𝔇(A) (9.871; any witness y is constructible by 9.62); B5ₗ: L · (V × A) (9.873); B6ₗ to B8ₗ: converses (9.872).
- C1ₗ (infinity): F′ω, since ω ∈ range J₀ and F′ω = F″ω; every x in it is properly included in a later F′β of the same kind.
- C2ₗ, C3ₗ (union, power): the relevant set of constructible sets is included in a constructible set by 9.63; note C3ₗ only asks for a set including all constructible subsets, which is why power set need not be absolute.
- C4ₗ (substitution): A″x is constructible (9.91), and any value of a constructible function at a constructible argument is constructible.
- Dₗ (foundation): inherited, since a member of a constructible class is constructible.
So every unstarred theorem holds in Δ, and the relativized notions 𝔏ₗ and Lₗ exist.
Chapter VII: V = L holds in Δ
The goal: Lₗ = L, i.e. constructibility is absolute; then Vₗ = L = Lₗ, so in Δ every set is constructible.
Two tools. (1) An operation 𝔄 is absolute if it produces constructible classes from constructible ones and satisfies its relativized defining postulate (uniqueness in the model then forces 𝔄ₗ = 𝔄). (2) Lemma before 11.5: a class defined by a postulate φ(A) in which every concept is absolute is itself absolute. With these, absoluteness propagates up the chain of definitions.
| Step | Absolute notions | Key reason |
|---|---|---|
| 11.1 to 11.23 | ×, A², A³, Rel, 𝔇, ·, converses, ↾, 𝔚, image, −, +, Eₗ = E · L, all 𝔉ᵢ (11.221), A′X | Constructibility of results (Chapter V) plus the relativized postulates; relativized complement is L − X |
| 11.3 to 11.32 | Completeness, "is an ordinal" | Ordinals of the model are ordinals; nothing yet about non-constructible ordinals |
| 11.4 to 11.42 | Well-ordering, functions, On | On is a proper ordinal in Δ, hence On ⊆ L: every ordinal is constructible |
| 11.43 to 11.46 | <, ≤, +1, the numerals, sup/lim | Definitions from ∈ and pairs |
| 11.5 to 11.54 | R, S, J, Jᵢ, K₁, K₂ | Defined by postulates using only absolute concepts |
| 11.6, 11.7 | F, then L = 𝔚(F) | F's postulate uses ↾ and the 𝔉ᵢ |
Conclusion (end of Chapter VII). "If there exists a model for the axioms of groups A, B, C, D, there exists also a model for the augmented set of axioms obtained by adding as an axiom the proposition V = L, namely, the model consisting of the classes and sets 'constructible' in the given model." Equivalently: a contradiction from V = L and Σ would yield one from Vₗ = Lₗ and the relativized axioms, all provable in Σ, so Σ itself would be contradictory, and the contradiction could be actually constructed.
Chapter VIII: V = L implies AC and GCH
- Choice (11.8): the relation As, which picks in each non-empty set its element of least order (the "designated" element), satisfies Axiom E if V = L. 11.81: C′α = the order of the designated element of F′α, with C′α < α. From here on starred theorems may be used; only 12.2 really needs V = L.
- 12.1: |F″ωα| = ℵα (≤ by *9.26; ≥ because F is one-to-one on the J₀-stages below ωα).
- 12.2 (needs V = L): every subset of F″ωα belongs to F″ωα₊₁. With 12.1 this gives |𝔓(F″ωα)| ≤ ℵα₊₁, hence GCH.
The condensation lemma in Gödel's algebraic form.
12.3: if m ⊆ On is closed under C (the order of the designated element), K₁, K₂ and the Jᵢ (as triadic relations), and G is an ∈-isomorphism of m onto an ordinal o, then G also preserves the membership structure of F: for α, β ∈ m, F′α ∈ F′β ↔ F′G(α) ∈ F′G(β).
12.3 ⇒ 12.2. Given x ⊆ F″ωα, by V = L x = F′η for some η. Close ωα ∪ {η} under C, K₁, K₂ and J₀ to J₈; by 8.73 the closure m has cardinality ℵα. M is a set of ordinals, so it is isomorphic (7.7) to an ordinal o, with o < ωα₊₁. ωα is an initial section of m, so G is the identity on ωα (7.62). By 12.3, for γ < ωα: F′γ ∈ x ↔ F′γ ∈ F′G(η), so x and F′G(η) have the same elements inside F″ωα. Since x ⊆ F″ωα = F′ωα (ωα ∈ range J₀, 9.27), x = F′ωα · F′G(η), and by 9.611 its order is below ωα₊₁: x ∈ F″ωα₊₁.
12.4 to 12.6: why the collapse preserves F.
- 12.4: if m is closed under K₁, K₂, J₀ … J₈ and G maps m isomorphically onto o, then G commutes with every Jᵢ, and o is closed under them. Outline: J restricted to the triples (i, α, β) with α, β ∈ m is an S-to-∈ isomorphism onto m; transport it by G to an isomorphism of 9 × o² onto o; but J itself maps the S-section 9 × o² onto an ordinal; two isomorphisms of a well-ordered set onto ordinals coincide (7.62), so the transported map is J.
- 12.5, 12.51 state this symmetrically for two closed sets m, m′ with an isomorphism between them, and transfer K₁, K₂.
- 12.6: if m, m′ are also closed under C, then G preserves F′α ∈ F′β and F′α = F′β. Proof by induction on η, the larger order involved, assuming both relations for smaller orders. Write r = F″m and rη for its part below η; the inductive hypothesis gives a map H = F ∘ G ∘ F⁻¹ from rη onto r′η′ that is one-to-one and ∈-preserving. Nine auxiliary facts follow: (1) r is closed under the fundamental operations; (2) orders of members of r lie in m (closure under C); (3) every non-empty member of r has a member in r (the designated element); (3.1) components of pairs and triples in r are in r; (4) r is closed under the images by Q₄ to Q₈; (5) to (7) weak completeness of rη; (8) H preserves unordered pairs, ordered pairs, triples and the Qᵢ.
- The cases. It suffices to prove F′α ∈ F′η → F′α′ ∈ F′η′ (equality and the converse follow by symmetry and the separating element). Then one case per slice of η: J₀ (both sides are "all earlier sets", trivially equivalent); J₁ (pairs: F′α is one of the two components); J₂ (E · X: an ∈-pair transfers by (7), (8)); J₃ (difference: the inductive hypothesis twice); J₄, J₆, J₇, J₈ (images under Qᵢ: a witness x in r with (F′α, x) ∈ Qᵢ transfers by (4), (5), (8)); J₅ (the domain-type operation: a witness u produced inside r by (1) and (3) transfers by (8)). Then 12.3 follows, since o is closed under J (12.4) and under C, K₁, K₂ (they decrease ordinals). q.e.d.
The conceptual proof (1939a, Solovay's outline). Take an elementary submodel of Lγ of size λ containing x, collapse it, recognize the collapse as some Lθ.
The 1940 proof. Take a set of ordinals closed under the indexing functions of F, collapse it as a set of ordinals, and prove by induction on order that F's membership pattern is preserved. Same skeleton, no model theory (no satisfaction, no elementary submodels), but the reader must verify nine cases and cannot see that it is Löwenheim–Skolem plus collapse.
Thought experiment: compressing a recipe book. Each constructible set is a dish with a recipe number; the recipe says which two earlier dishes to combine and with which of eight techniques, or "plate everything so far". Pick one dish x made from ingredients on the first ωα pages. Collect x's number, the numbers of its two inputs, theirs, and so on, plus the number of each dish's "designated" ingredient; you get ℵα recipe numbers. Renumber them consecutively without gaps. Because every recipe only refers to smaller numbers, and the renumbering preserves order, the renumbered book cooks exactly the same dishes from the same ingredients: x reappears at a page below ωα₊₁. Gödel's 12.6 is the check that each of the eight techniques survives renumbering.
Notes added later
1951: projective (PCA) well-ordering of the reals in Δ; the "normality" corrections; Duda's correction to Dfn 4.65; and: the proof extends to stronger axioms of infinity (inaccessibles, Mahlo), and to other axioms "suggested by the intuitive meaning of the primitive terms", "for the simple reason that all these axioms of infinity imply their own relativized form". 1966 addition: this holds for the axioms known at that time (1951).
August 1965: Cohen (1963, 1964, 1966) proved CH unprovable from set theory (even with Mahlo or Lévy axioms), by "a powerful method for constructing denumerable models"; the value of 2ℵ₀ "turns out to be almost completely arbitrary" (Solovay 1963, Easton 1964).
August 1965: progress on axioms of infinity: Lévy's reflection principle (1960) gives a hierarchy of formulations, one of which (Bernays 1961) yields all Mahlo axioms; Tarski (1962), Keisler–Tarski (1964) study much stronger axioms whose truth does not follow from "the basic intuitions underlying abstract set theory" but which are supported by analogy (generalizations of Stone's representation theorem to infinitary Boolean algebras). As Gödel had conjectured in 1947, one of them implies non-constructible sets (Scott 1961); whether one implies ¬GCH "has not yet been determined".
August 1965: for a general discussion see 1947 and 1964; "a slightly different version of the consistency proof …, which exhibits more clearly the basic idea of it, is outlined in 1939a".
What the monograph hides. Solovay's criticism stands: the GCH proof is non-conceptual, and the reader cannot see that it is Löwenheim–Skolem plus collapse. The descriptive-set-theory claims (non-measurable Δ¹₂ set, thin Π¹₁ set) get only a few lines in the 1951 note, "comprehensible only to cognoscenti"; complete proofs came from Novikov (1951) and Addison (1959). Gödel's own 1951 notes also correct errors (normality, Dfn 4.65). And the remark that large-cardinal axioms "imply their own relativized form" fails for measurables, discovered ten years later to refute V = L; the 1966 addendum quietly restricts it to axioms known in 1951.
How L is taught now. Every modern text (Kunen, Jech, Devlin) follows the 1939a route: definable power set, reflection, condensation (if X ≺ Lα then X collapses to some Lβ). Gödel's operations approach survives as the Gödel operations characterizing rudimentary functions in Jensen's fine structure, and his class theory is today NBG (von Neumann–Bernays–Gödel), conservative over ZFC. Proof assistants have caught up: the Isabelle/ZF formalization by Paulson (2003) proved the relative consistency of AC via L, the Isabelle/ZF development of forcing by Gunther, Pagano, Sánchez Terraf and Steinberg (2020s) proved the independence of CH, and the Lean Flypitch project (Han and van Doorn, 2020) machine-checked the independence of CH using Boolean-valued models, so both halves of the CH story are machine-verified.
Takeaway. The 1940 monograph is Gödel's insistence on finitely many axioms and explicit constructions: no satisfaction relation, no model theory, only class operations, a well-ordered enumeration, and induction. It is harder to read than 1939a, but it shows the result can be proved inside a finitely axiomatized set theory, line by line.
Reading "Russell's Mathematical Logic": Parsons's Guide
Charles Parsons introduces Gödel's first and most extended philosophical statement, written for Schilpp's Library of Living Philosophers volume on Bertrand Russell. The paper is formally a commentary on Russell, yet Gödel is "not reticent in expressing his own views", and Parsons reads it chiefly for what it reveals about its author. Parsons's central point is that Gödel's realism covers concepts as well as sets, and that it was never idle metaphysics: it had "cash value" as a programme for extending hierarchies into the transfinite, of which the constructible sets are the prime example.
Origins of the paper
18 Nov 1942: Schilpp invites Gödel, proposes the title, and reports that Russell considers him "the scholar par excellence in this field".
17 May 1943: Gödel sends the manuscript; a long correspondence follows over Schilpp's stylistic editing and Gödel's own revisions.
28 Sep 1943: the revised version arrives after Russell has finished his replies; Gödel writes urging him to respond, stressing that the paper is controversial and critical of him.
1944: Russell replies in one paragraph: it is eighteen years since he worked on logic, Principia was finished thirty-three years ago, and "many of his criticisms of me are justified".
Later: Gödel contributes 1949a to the Einstein volume, drafts but never submits a paper for the Carnap volume ("Is mathematics syntax of language?"), and declines the Popper volume.
1964a, 1972b: two reprints, with only editorial changes plus a new opening footnote on "constructivistic".
"His great ability, as shown in his previous work, makes me think it highly probable that many of his criticisms of me are justified." Russell, reply in Schilpp 1944, p. 741
The shape of a "pointillist" paper
Parsons endorses Weyl's description (1946): the paper is "the work of a pointillist: a delicate pattern of partly disconnected, partly interrelated, critical remarks and suggestions". He nonetheless divides it into eight parts and follows that division.
The archive also holds four annotated reprints (A–D) and a loose page (E) with remarks on Bernays's review (1946). Most annotations are stylistic; a few signal changes of view, but none is known to be final, and the later reprints hardly reflect them.
1. Russell's realism as Gödel's starting point
- The zoology quotation. Gödel opens with Russell's "pronouncedly realistic attitude": "Logic is concerned with the real world just as truly as zoology".
- The epistemological analogy. Axioms need not be self-evident; like physical laws they can be justified because their consequences agree with what has been found evident. Gödel: this view "has been largely justified by subsequent development".
- Parsons's reading. The whole essay can be seen as a defence of these Russellian attitudes against the reductionism in Russell's own philosophy and logical practice. It was perhaps "the most robust defense of realism about mathematics" since the paradoxes reached mathematicians after 1900; Bernays's defence (1935) was more cautious.
2. Descriptions and the "collapsing argument"
Gödel sketches (note 5) a formal argument for Frege's thesis that two sentences have the same signification (Gödel's word for Frege's Bedeutung) whenever they share a truth value. The argument collapses intensional distinctions from simple assumptions about signification.
Why it mattered later. Church (1943) gave a similar argument. Such collapsing arguments (now usually called "slingshot" arguments) became prominent in debates on meaning, reference, modality and propositional attitudes. Quine's use against modal logic is the best known, though it first appears in his writings only in 1953, essentially in Church's form. Church (1942) noted that Russell's theory of descriptions blocks apparent failures of substitutivity of identity, the basis of Smullyan's (1948) reply to Quine. Gödel concedes that Russell's theory avoids Frege's conclusion, but suspects it "only evades" the problem.
3. The paradoxes and the vicious-circle principle
A puzzle reconciled. In 1944 Russell's analysis of the paradoxes shows "the amazing fact that our logical intuitions … are self-contradictory". In 1947 the paradoxes are "a very serious problem, but not for Cantor's set theory" (revised in 1964 to: not for mathematics, "but rather for logic and epistemology"). Parsons dissolves the tension:
- 1947/1964 defends the iterative conception of set (sets formed by iterated collection of previously given objects), which "has never led to any antinomy".
- 1944 follows Russell into logic in the wider sense: intuitions "concerning such notions as: truth, concept, being, class". The iterative conception is mentioned (p. 144) but kept in the background, "perhaps more so than was optimal" for defending realism.
The vicious-circle analysis. Gödel's dissection of the ambiguities of the principle is "probably the most influential piece of direct commentary on Russell in the essay". His main criticism, foreshadowed by Ramsey (1926): the strongest form (no totality may contain members definable only in terms of it) holds only if the entities are "constructed by ourselves". For objects that exist independently of our constructions, impredicative description is "nothing in the least absurd". Since classical mathematics, and even Principia with reducibility, violates the strong form, Gödel takes this "rather as a proof that the vicious-circle principle is false than that classical mathematics is false".
4. Gödel's realism about classes and concepts
The realist declaration (p. 137). Classes and concepts may be understood as real objects "existing independently of our definitions and constructions". Their assumption is "quite as legitimate as the assumption of physical bodies", and they are "in the same sense necessary to obtain a satisfactory system of mathematics as physical bodies are necessary for a satisfactory theory of our sense perceptions". Parsons stresses, against earlier commentators, that this realism covers concepts ("the properties and relations of things") as well as sets.
Parsons poses three questions the paper raises but does not settle.
Parsons's three questions
- What does "real" mean? Realism must assert more than objective existence, or it says no more than a non-subjectivist constructivism. Gödel does not clarify it directly; his realism lives in concrete problems, such as the claim (1947/1964) that CH is definitely true or false though independent, and his critique of Russell for blocking transfinite extensions of type hierarchies. The constructible sets show realism's "cash value".
- How close is the analogy with physical bodies? It is tempting to read sets as theoretical posits explaining data (as Dummett and Chihara do). Direct evidence is lacking: Gödel never uses the language of explanation, and in 1964 he is more cautious about justifying axioms by consequences than in 1944. What plays the role of sense perception in his own epistemology is elementary arithmetical evidence.
- What theory of concepts? "Property of set" is a primitive of set theory for Gödel (1947, note 17), so he had mathematical reasons for adding concepts. He wants an impredicative theory, stronger than the simple theory of types, in which a property may involve a totality to which it belongs. No available theory satisfied him, and none has been built since.
Structures "identical" with proper parts. Gödel claims it is not contradictory that a proper part be identical (not merely equal) to the whole, "as is seen in the case of structures in the abstract sense": the integers contain themselves as a proper part. On the set-theoretic notion of structure this is false, since substructures with smaller domains are never identical with the whole. Gödel is thinking of an informal notion in which isomorphic structures are the same structure, and Parsons notes it "is a problem to construct a theory" where that sameness is identity. In category theory, a monomorphism that is not epi need not exclude identity, though this is a superficial point next to the self-applicability of categories.
The type-free hope. The simple theory of types is the best present solution, but Gödel hopes for a theory in which a concept is significant everywhere except at "singular points", so that the paradoxes resemble dividing by zero. He cites the λ-calculus systems of Church (1932, 1933), refuted by Kleene–Rosser (1935). In 1964 he adds only that the self-applicability of categories transcends the iterative concept, while accepting Mac Lane's large/small distinction as capturing current mathematical content. Parsons conjectures that Gödel never formulated a theory of concepts to his satisfaction and hopes the shorthand notebooks will tell.
5. The ramified theory and the predicativity programme
Gödel reads Principia's contextual definitions as reducing classes to concepts, and finds in the second edition a programme in which all non-simple concepts and propositions "appear as something constructed". The programme motivates ramification intrinsically but cannot yield classical analysis (impredicative arguments) or, perhaps, even number theory, since the Frege–Russell definition of "natural number" quantifies over all classes.
Parsons's puzzles about Gödel's reading.
- Satisfaction is presupposed. If higher-order variables range over predicates (linguistic expressions), translating statements of order n needs truth or satisfaction for lower orders, defined inductively: a further obstacle to deriving arithmetic from logic that Gödel never mentions.
- Elimination versus signification. Gödel seems not to distinguish a nominalist theory that eliminates concepts from one where every concept is signified by an antecedently understood expression but not eliminated (today: a substitutional reading of quantifiers).
- Reducibility misread. That every function is coextensive with one of lowest order does not show "the existence in the data" of concepts, only of classes. Russell was closer: reducibility does "what common sense effects by the admission of classes". This "insensitivity" to the intensional character of Russell's logic surprises in the author of 1958, with its subtle treatment of intensional notions.
A transfinite theorem of reducibility. Gödel presents his constructible sets as the hierarchy of orders extended, inside impredicative mathematics, to all transfinite orders; the theorem that every constructible set of integers has order < ω₁ is a "transfinite theorem of reducibility" (a phrase removed in annotated reprint A). Against Russell, Parsons calls this "a striking application of his realistic point of view".
Predicative extensions. Gödel also remarks that even predicatively the orders can be extended "to such transfinite ordinals as can be constructed within the framework of finite orders". Parsons sees here perhaps the first suggestion of a programme pursued from 1950.
| Stage | Contribution | Outcome |
|---|---|---|
| Lorenzen 1951–55; Wang 1954 | Transfinite ramified theories for a better predicative analysis | Which ordinal levels to admit left open |
| Wang 1954 | Autonomous iteration: admit levels β for which a well-ordering of type β is definable at earlier levels | Closes after one step |
| Spector 1957 | Systems indexed by recursive ordinal notations | Definable sets = hyperarithmetic; definable well-orderings are recursive |
| Kreisel 1960 | Thesis: predicatively definable = hyperarithmetic; proposes autonomy for provability | Doubts about "if": recursive ordinals need not be predicatively recognized |
| Feferman 1964; Schütte 1965 | Autonomous progressions: admit level α once its ordering is proved well-founded | Predicative limit = Γ₀, the first strongly critical ordinal |
| Feferman 1964–74 | Extension to unramified analysis and set theory | Γ₀ characterization holds broadly |
6–8. Simple types, analyticity, Leibniz
- Simple types. Of greatest interest: Gödel questions it as a theory of concepts and hints at a type-free alternative, motivated by Russell's idea of limited ranges of significance.
- Analyticity, first sense (reducible by definitions to the law of identity): even arithmetic is demonstrably non-analytic, by undecidability. With infinitely long sentences all axioms become analytic, but proving it presupposes the whole of mathematics, e.g. Choice is analytic "only if it is assumed to be true". This anticipates Quine's critiques of analyticity (1960).
- Analyticity, second sense (true "owing to the meaning of the concepts", perhaps undefinable): the axioms of the first-edition Principia (except infinity) qualify when "predicative function" means class, or (without choice) concept. Gödel's "concept" here resembles Frege's extension; his "singular points" idea recalls Frege's own failed way out (1903).
- Vienna Circle. The seriousness of this section shows more engagement with Carnap's circle than usually credited: with them, mathematical truths hold by meaning; against them, not by convention or linguistic rules we lay down. The unfinished Carnap paper elaborates the same split.
- Coda. Logic has lagged behind Peano's hopes because of an "incomplete understanding of the foundations", and the characteristica universalis of Leibniz, "the greatest influence" among past philosophers, might still be realistic. The Leibnizian flavour recedes in later writings.
Bernays's review versus Gödel. Bernays (1946) argued, via Frege's sense/reference distinction, that reducing a proposition to a = a "by virtue of meaning" can only use reference, which trivializes the thesis. Gödel's sheet E reads "Misunderstanding of my interpretation of type theory for concepts". Parsons finds Bernays's argument unconvincing: reducing P to Q by virtue of P's sense need not make their senses identical.
Since then. The predicative limit Γ₀ remains standard, though Weaver (2005–09) argued that predicativists can reach beyond it, and reverse mathematics (Friedman, Simpson) showed that most ordinary analysis is provable in weak subsystems such as ACA₀, while even ATR₀, whose proof-theoretic ordinal is Γ₀, is predicatively reducible. Type-free theories of properties grew into Feferman's explicit mathematics, Aczel's Frege structures and Kripke-style truth theories. Gödel's hope that categories reveal a self-applicable notion is echoed in homotopy type theory and its univalence axiom (Voevodsky, 2010s), which makes isomorphic structures literally equal: close to the informal notion of structure Parsons found Gödel assuming.
Takeaway. Read as Parsons reads it, 1944 is less a review of Russell than a manifesto: realism about sets and concepts, a demolition of the strong vicious-circle principle, and a research agenda (transfinite hierarchies, a type-free theory of concepts, a meaning-based notion of analyticity) of which only the first was completed.
Russell's Mathematical Logic (1944)
Gödel's essay assesses Russell's analysis of the concepts and axioms of logic: the theory of descriptions, the diagnosis of the paradoxes, the vicious-circle principle, the no-class theory, the ramified and simple theories of types, and the analyticity of Principia's axioms. Throughout, Gödel turns Russell's stated realism against Russell's constructivist practice. His verdict: the attempt to treat classes and concepts as "logical fictions" has left "only fragments of mathematical logic", so one should instead clarify these notions and build a consistent theory of them as objectively existing entities.
Two aspects of mathematical logic
- Mathematical logic is "nothing else but a precise and complete formulation of formal logic", with two aspects: a branch of mathematics (about classes, relations, symbol combinations) and a science prior to all others, containing the principles underlying all sciences.
- Leibniz conceived it in the second sense in his Characteristica universalis; two centuries later Frege and Peano realized a calculus adequate to exact reasoning. Frege, who "has doubtless the priority" (ten years before Peano), analysed thought and derived arithmetic from logic; Peano built an elegant symbolism for stating theorems.
- Principia's achievement: the first use of the method for actually deriving large parts of mathematics from a few logical notions, and a new instrument, the abstract theory of relations (developed earlier by Peirce and Schröder in too close an analogy with numerical algebra).
- Principia's defect: compared with Frege, a "considerable step backwards" in formal precision. Above all it lacks a precise syntax. The incomplete symbols are introduced by translation rules, and without a survey of all expressions one cannot know that elimination is possible, unique, or compatible with the rules of inference. The order of eliminating defined symbols can matter; Gödel gives a counterexample.
Russell's two analogies with natural science.
- Realism: "Logic is concerned with the real world just as truly as zoology." (Gödel's footnote says the passage was dropped from later editions; the editors note that Blackwell (1976) showed this to be mistaken.)
- Epistemology: axioms of logic are like laws of nature, logical evidence like sense perception; axioms need not be self-evident but are justified because they let the "perceptions" be deduced.
Gödel endorses the second "provided 'evidence' is understood in a sufficiently strict sense". Arithmetical problems already require assumptions transcending arithmetic; set theory and even questions about the reals will likely need new axioms based on some hitherto unknown idea; and some long-unsolved problems may persist because "the necessary axioms have not yet been found". Mathematics may lose some "absolute certainty", but modern criticism has already removed much of it. He compares Hilbert's "supplementing the data of mathematical intuition" (e.g. By excluded middle), though the border between data and assumptions falls elsewhere for Hilbert and Russell.
The theory of descriptions
The problem. What does "the author of Waverley" signify, and what do sentences containing it mean? The obvious answer (it signifies Scott) plus the plausible axiom that the signification of a compound depends only on the significations of its parts yields that "Scott is the author of Waverley" signifies the same as "Scott is Scott", and this leads "almost inevitably" to the conclusion that all true sentences have the same signification.
Frege versus Russell on sentences
- Frege accepted the conclusion, in an almost metaphysical sense recalling the Eleatic "One": all true sentences signify "the True", analysed differently in different propositions.
- Russell held that true sentences "indicate" facts, false ones nothing; so Frege's theory holds, in a sense, for false sentences only.
- Since different truths indicate different facts, Russell must drop either the compositionality principle or the claim that descriptions denote. He drops the latter: "the author of Waverley is Scotch" means "there exists exactly one entity who wrote Waverley, and whoever wrote it is Scotch". The sentence contains no constituent denoting Scott.
- Russell's arguments: descriptions are meaningful even when nothing is described ("the present king of France does not exist"); and one can understand them without acquaintance with the object.
- Gödel's verdict: the problem raised by Frege's conclusion "has only been evaded", and "there is something behind it which is not yet completely understood".
The formal argument (note 5) needs only two further assumptions: that φ(a) means the same as "a is the object which has φ and is identical with a", and that every proposition "speaks about something", i.e. Has the form φ(a). Gödel also notes three correlates of a sentence: Frege's Bedeutung (the fact, or the True), Frege's Sinn (the conceptual correlate, for Russell a "curious shadowy" possible fact he could never believe in), and the psychological correlate (belief), which Russell calls "signification" in An Inquiry into Meaning and Truth.
One formal advantage, soon qualified: Russell needs no axioms about "the", since its theorems follow from explicit definitions, whereas Frege must assume an (analytic) axiom. The advantage holds only if definitions are mere typographical abbreviations, not names for the objects defined.
The paradoxes and two neglected directions
Russell "freed them from all mathematical technicalities", revealing that our logical intuitions are self-contradictory. His diagnosis: the error is to assume that every propositional function determines a class, or exists "as a separate entity" (a concept). The existence of the concept alone suffices for the intensional paradox ("not applying to itself").
Zig-zag versus limitation of size (Russell 1906)
- Gödel's renaming: the zig-zag theory is intensional (classes exist when the function is simple enough in content); limitation of size is extensional (classes exist when the extension is not too big).
- Limitation of size, realized by Zermelo's axiomatic set theory, has no universal class. Von Neumann (1929) made "not too big" precise: a class exists iff it is not equivalent to the universe, a criterion that can replace replacement and choice.
- Zig-zag has one realization sharing its essential features: Quine's system (1937, NF). Gödel thinks other interesting possibilities along these lines are not unlikely.
- Russell's own path took neither, and adopted the more radical no-class theory: classes and concepts never exist as real objects and are a mere façon de parler.
The vicious-circle principle dissected
The principle blames the paradoxes on totalities whose existence would entail new members definable only through the whole. Russell: "no totality can contain members definable only in terms of this totality, or members involving or presupposing this totality". For the intensional paradoxes he adds that every propositional function presupposes the totality of its values, hence of its arguments.
Three principles, not one
- "Definable only in terms of": the strong form. Only this one forbids impredicative definitions, and so destroys the Dedekind–Frege derivation of mathematics and much modern mathematics.
- "Involving": much more plausible.
- "Presupposing": also more plausible, if "presuppose" means for existence rather than for knowability.
The argument against the strong form.
- Classical mathematics violates it. The axioms imply real numbers definable only by reference to all reals; Principia with reducibility does too.
- Gödel takes this "rather as a proof that the vicious circle principle is false".
- First reason: reference to a totality need not mean reference to every element; "all" need not be an infinite conjunction. Langford and Carnap read "all" as analyticity, necessity or demonstrability.
- Second reason: even if "all" is a conjunction, the strong form applies only to entities constructed by ourselves, whose construction cannot rest on a totality containing them. For objects that exist independently, describing one by reference to a totality containing it involves "nothing in the least absurd". This contradicts neither the second form (the description involves the totality, the object does not) nor the third.
Constructivism defined. The strong form therefore applies only on the constructivistic or nominalistic standpoint, where a notion is, e.g., a symbol with a rule for translating sentences containing it into sentences without it. (The 1964/1972 footnote: Gödel's "constructivistic" means strictly nominalistic, like Russell's no-class theory, better called "fictionalism", and is far from intuitionism or the Hilbert school, both of which rely on the mathematical intuition Russell aimed to avoid. What Russell's fictionalism can obtain is the finite orders of the ramified hierarchy, without the axiom of infinity.)
Classes and concepts as real objects
"It seems to me that the assumption of such objects is quite as legitimate as the assumption of physical bodies and there is quite as much reason to believe in their existence. They are in the same sense necessary to obtain a satisfactory system of mathematics as physical bodies are necessary for a satisfactory theory of our sense perceptions." Gödel 1944, p. 137
- The two conceptions. Classes may be "pluralities of things" or structures made of them; concepts the properties and relations of things independent of our definitions. In both mathematics and physics, propositions about these entities cannot be reinterpreted as propositions about the "data". Russell himself admits "with hesitation" that universals exist, but only those of sense perception, "which does not help the logician".
- Different identity conditions. Two different definitions always yield two notions in the constructivist sense (different translation rules); for concepts, the same thing may be described in different ways, and even extensionality might hold. "Two is the notion under which fall all pairs": many constructed notions satisfy this, but there might be one common "form" or "nature" of all pairs.
- Constructivism forbids impredicativity. Retranslating an impredicatively defined symbol reproduces the symbol. Carnap's demonstrability reading does not help, since constructivist demonstrability must itself split into orders. Chwistek (1933) showed that simple types plus an axiom of intensionality (different definitions, different notions), admissible for constructed notions, is contradictory.
- Realism permits it. For objectively existing concepts there is no objection to speaking of all of them or describing some by reference to all. A property may then contain itself as a constituent of its content, which only makes its meaning impossible to construct from non-conceptual entities: "no objection for one who takes the realistic standpoint".
- Approximations even in constructive logic: propositions containing their own formal demonstrability (Gödel 1931), and sentences about a totality containing themselves ("Every sentence … contains at least one relation word").
- Different solutions for different readings. For constructed notions, the paradoxes really are due to a vicious circle; for concepts, the fault lies elsewhere, to be found now in simple types and later perhaps in a type-free theory.
Classes as pluralities. They too are described, not created, by definitions, so the strong form does not apply; even the second form fails for some readings of class as structure (cf. Mirimanoff 1917–20). For contemporary mathematics one may assume the second form, which leads to Zermelo's system: sets split into levels, with mixed and transfinite levels allowed, and the Aussonderungsaxiom replacing reducibility. Russell's objections from the null class and unit classes show at most that these are convenient fictions, like points at infinity, not that all classes are.
The no-class theory and its negative result
A rare example carried out in detail of eliminating objects beyond the "data" in favour of constructions from them. The outcome is "essentially negative": constructed classes and concepts lack the properties mathematics needs unless one either
- adds axioms about the data, such as reducibility, which "in essence already mean the existence in the data of the kind of objects to be constructed", or
- pretends to form propositions of infinite, even non-denumerable length (Ramsey 1926). But "what else is such an infinite truth-function but a special kind of an infinite extension (or structure) … which can be understood only by an infinite mind?"
Hence logic and mathematics, like physics, "are built up on axioms with a real content which cannot be 'explained away'".
- What constructivism does yield: the theory of orders, now not an ad hoc device but an unavoidable consequence of denying that classes, concepts and quantified propositions exist. One may speak of all existing things; classes are simply not among them, and each extension of the symbolism permits a more comprehensive one, indefinitely. It presupposes arithmetic, which "only proves that not even this restricted logic can be built up on nothing".
- First edition of Principia: constructivism is mostly abandoned, since reducibility plus infinity require primitive predicates of arbitrarily high types. What remains: classes as façon de parler; the definition of connectives on quantified propositions ("which incidentally proved its fecundity in a consistency proof for arithmetic"); a step-by-step construction of higher orders made superfluous by reducibility; definitions as typographical abbreviations (largely an illusion); and the theory of descriptions.
- Second edition: constructivism resumed. Reducibility is dropped; all primitive predicates belong to the lowest type; higher orders serve only to assert complicated truth-functions of atomic propositions. This works easily only for finitely many individuals.
- The finite case. With n individuals, "x ∈ m" is literally a disjunction x = a₁ ∨ … ∨ x = aₙ, and "there exists a class" means "there exist individuals x₁ … xₙ". Iterating gives something like simple types with mixed types; axiomatic set theory is then the extrapolation to infinitely many individuals or infinite iteration. Ramsey's infinite propositions are "everything but constructivistic, unless one means constructions of an infinite mind".
Does arithmetic survive ramification? Defining the integers as cardinals belonging to every inductive class must restrict "every" to an order; one gets integers of different orders, and induction for order n works only for properties of order n, though the notion of integer itself is of order n + 1. Principia's Appendix B claims integers of order > 5 equal those of order 5. Gödel finds the proof of lemma *89.16 inconclusive: induction is applied to a property of order > 3 when α has order > 3. The question "must be considered as unsolved". (Later: Myhill 1974 proved the negative answer claimed by Wang.) And a positive answer would not help logicism: defining functions of order n as finite combinations presupposes finiteness, hidden only by leaving "propositional function of order n" unanalysed. If quantifiers are infinite conjunctions instead, why not define the integers by the infinite disjunction x = 0 ∨ x = 0+1 ∨ …?
Transfinite orders: reducibility regained
The mathematical value of the theory of orders. Viewed inside ordinary mathematics, where impredicative definitions are allowed, the hierarchy extends to arbitrary transfinite orders; even predicatively it can reach "such transfinite ordinals as can be constructed within the framework of finite orders", and it demands order ω (functions referring to all finite orders). With transfinite orders an axiom of reducibility can be proved, but the reducing ordinal is so large that it presupposes impredicative totalities. Still, all impredicativity is reduced to one kind: the existence of certain large ordinals and recursive reasoning on them. A well-ordering of type ω₁ suffices for the theory of real numbers, and this "transfinite theorem of reducibility" gives the consistency of AC, CH and GCH with set theory and with Principia. This is L, described in Russell's language.
The simple theory of types
- Independence from orders. Simple types (individuals, properties of individuals, relations, properties of relations …; no mixed or transfinite types) are independent of the vicious-circle principle; mixed types do not violate it. Simple types alone suffice for the epistemological paradoxes too (Ramsey 1926, Tarski 1935).
- Russell's (and Frege's) reason. A propositional function is ambiguous or "unsaturated", so it can occur meaningfully only when the ambiguity is removed; hence it cannot replace an individual, and functions with different ambiguities cannot replace each other. This belongs to the no-class order of ideas, treating functions as "fragments" of propositions, and even there it does not strictly follow, since notions could be built with mixed types.
- On the realist view it is implausible. A concept such as "transitivity" or the number two seems to lie behind all its "realizations" on different levels, and so does not exist according to type theory. There is "some truth" in the idea of realizations on many levels, so types may serve as a stepping stone (as in Quine); typical ambiguity is a step in that direction but adds only symbolic conventions.
- A new idea for the paradoxes. Blame not the axiom that every function defines a concept, but the assumption that every concept yields a meaningful proposition for any argument. The objection that any concept can be extended (false where meaningless) fails because "meaningfully applicable" need not itself be always meaningfully applicable.
- The suspect principle. Simple types assume: whenever x can replace y in one meaningful proposition, it can in every one. This splits objects into exclusive ranges of significance, each concept significant for "an infinitely small portion of all objects". Worse, the principle cannot be stated meaningfully under its own assumption, nor can "x is of type t".
Singular points. "It might even turn out that it is possible to assume every concept to be significant everywhere except for certain 'singular points' or 'limiting points', so that the paradoxes would appear as something analogous to dividing by zero." Our logical intuitions would then be essentially correct, only "blurred". Attempts so far have failed (Church 1932–33, proved inconsistent by Kleene–Rosser 1935), but impossibility has not been proved.
Are the axioms of Principia analytic?
| Tautological sense | Analytic sense | |
|---|---|---|
| Definition | Terms definable so that theorems become cases of a = a | True "owing to the meaning of the concepts", perhaps undefinable |
| Arithmetic | Demonstrably non-analytic if eliminations must be finite: else a decision procedure (Turing 1937) | Analytic |
| With infinite sentences | All axioms (choice, infinity, reducibility) analytic, but only by presupposing all of mathematics; choice is analytic "only if it is assumed to be true" | Not needed |
| Principia axioms | n/a | All except infinity, reading "predicative function" as class or (without choice) as concept |
| Limitation | Circular | We do not perceive "concept" and "class" with sufficient distinctness, as the paradoxes show |
Note 47 removes an apparent conflict: analyticity in the second sense is compatible with "axioms with a real content", because the very existence of the concept "class" is such an axiom; define "class" and "∈" as whatever satisfies the axioms and you cannot prove they exist. And it reopens the Leibnizian possibility that every truth reduces to a = a, by virtue of a meaning "which can never be completely expressed in a set of formal rules".
The conservative course and Leibniz's dream
Gödel's conclusion. Russell treated classes and concepts (except the logically uninteresting primitive predicates) as nonexistent, replacing them with constructions. The result: interesting ideas, but "only fragments of mathematical logic remain" unless the condemned things return as infinite propositions or as reducibility, which with infinitely many individuals is demonstrably false unless one assumes classes or infinitely many "qualitates occultae". The better, conservative course is to make "class" and "concept" clearer and build a consistent theory of them as objectively existing. The actual development, simple types and axiomatic set theory, has done this successfully enough to derive modern mathematics without known paradoxes, though "many symptoms show only too clearly … that the primitive concepts need further elucidation".
Why logic disappointed. Logic has stayed "so far behind the high expectations of Peano and others" who hoped it would aid mathematics as the decimal system aids computation. "For how can one expect to solve mathematical problems systematically by mere analysis of the concepts occurring if our analysis so far does not even suffice to set up the axioms?" Yet Leibniz did not think his characteristica utopian: he estimated five years for a few select scientists to produce "a new kind of an instrument increasing the powers of reason far more than any optical instrument", and credited even its rudimentary form with all his mathematical discoveries.
Critical lens.
- The analogy carries the argument. Realism is defended mostly by parity with physical bodies; no account is given of how we access abstract objects, the gap Benacerraf (1973) later made central.
- The theory of concepts is a promissory note. Gödel rejects every available theory of concepts, offers none, and never published one.
- The reading of Russell is partly a reconstruction. As Parsons notes, Gödel assimilates propositional functions to objects and underrates the intensional side of reducibility.
- Its lasting technical points are sound: the strong VCP is incompatible with classical analysis, ramified arithmetic is problematic, and simple types cannot state its own principle.
Since then. Quine's NF, the zig-zag representative Gödel singled out, resisted a consistency proof for eighty years; Randall Holmes announced a proof of Con(NF) relative to ZFC, and Holmes and Sky Wilshaw completed a Lean 4 formal verification in 2024. The singular-points programme lives on in paraconsistent and paracomplete theories of truth and properties (Kripke 1975, Field 2008), and in type-free systems such as Feferman's. Gödel's "conservative course" is today's practice: ZFC plus large cardinals, with the predicative and constructive alternatives studied as calibrated subsystems.
Takeaway. Gödel accepts Russell's paradox analysis and his science-like epistemology of axioms, rejects his constructivism, and recasts the hierarchy of orders as a realist tool that, carried into the transfinite, becomes the constructible universe.
Absolute Provability and Definability: The Princeton Bicentennial Remarks (1946)
At the Princeton bicentennial conference on problems of mathematics (17–19 December 1946), Gödel commented on Tarski's lecture in a short talk that went almost unread until Davis's anthology The Undecidable (1965). Starting from the observation that computability is the first epistemological notion given an absolute definition, he asks whether provability and definability can be made absolute too, and proposes ordinal definability. The talk's lasting contribution is the notion of ordinal-definable sets (OD) and the inner model HOD, rediscovered independently by others and now central to set theory, together with the idea that large-cardinal axioms might yield an absolute notion of proof.
Parsons's note: setting and history
17 Dec 1946: logic session; Tarski is "discussion leader" and gives the main talk; much of the session concerns decision problems.
Early 1947: Gödel sends the text to McKinsey for a planned volume Problems of Mathematics (never published). Asked by Tukey to write on Hilbert's first two problems, he accepts the continuum problem (the origin of 1947) and declines consistency of analysis, which should go to someone "more sympathetic to Hilbert's views".
1965: first published in Davis, at Kleene's suggestion and with Gödel's approval; Davis had not known it existed.
1968: reprint with changes proposed by Gödel, and a footnote reporting McAloon's result.
Why computability is special
The miracle of computability. With general recursiveness (Turing computability) "one has for the first time succeeded in giving an absolute definition of an interesting epistemological notion, i.e., one not depending on the formalism chosen". For demonstrability and definability, every definition is relative to a language, and for each language the notion obtained "is not the one looked for". For computability, "by a kind of miracle it is not necessary to distinguish orders, and the diagonal procedure does not lead outside the defined notion".
1965 footnote: a function is computable in any formal system containing arithmetic iff it is computable in arithmetic.
Parsons's gloss. The point is less the equivalence of Turing, λ-definability and Herbrand–Gödel recursiveness than the absence of stratification. For definability, diagonal arguments push us to ever richer languages. For computability, the enumeration of recursive functions is not recursive, so diagonalizing yields something non-recursive, not "recursive at the next level". Enumerating partial recursive functions works, but diagonalizing then produces functions undefined at some arguments (and the undecidable halting problem). Gödel takes this as encouragement: negative results such as incompleteness and Richard's paradox may exclude only certain ways of defining the absolute notions.
Absolute demonstrability
Gödel's sketch
- Make provability precise by a formalism; contemplating it yields new axioms "exactly as evident and justified" as the old (e.g. Its consistency).
- The extension iterates into the transfinite, so no formalism embraces all steps.
- But the steps might be "described and collected together in some non-constructive way".
- In set theory the extensions are best represented by stronger and stronger axioms of infinity.
- No decidable characterization of "axiom of infinity" exists, but perhaps: a proposition of a certain decidable formal structure that is also true.
- Hoped-for closure: any proof in the next system up (using truth) is replaceable by a proof from such an axiom.
- Hoped-for completeness theorem: every set-theoretic proposition is decidable from the present axioms plus "some true assertion about the largeness of the universe of all sets".
Parsons's reservations. "Exactly as evident" may be questioned even for the weakest extension, the consistency statement. Transfinite iteration of reflection had been studied by Turing (1939), and completeness results of the envisaged type were proved by Feferman (1962), but these are arithmetical in character. The set-theoretic version was evidently very speculative for Gödel, tied to the hope (so far disappointed) that axioms of infinity decide CH.
Ordinal definability
The construction. For definability there is likewise a transfinite hierarchy of languages. They cannot be collected into one if a language must have finitely many primitive terms; drop that, and allow "as many primitive terms … as there are ordinal numbers". "The simplest way of doing it is to take the ordinals themselves as primitive terms": definability by expressions containing names of ordinals and logical constants, including quantification over all sets.
Properties Gödel claims or conjectures
- Closure: adding a truth predicate for the whole transfinite language yields no new definable sets (only new properties). Consequently "x is ordinal-definable" is expressible in ZF, usually proved today with Lévy's reflection principle; Parsons conjectures Gödel knew reflection, whose proof pattern already appears in the GCH proof of 1940.
- Constructibility is a restricted version: it also defines from ordinals, but quantifies only over constructible sets. So one can "define sets, and even sets of integers, for which you cannot prove that they are constructible". Hence constructibility is not a satisfactory notion of definability.
- Conjecture 1: the OD sets satisfy the axioms of set theory, giving "another, and probably simpler, proof" of the consistency of AC.
- Conjecture 2: a bound exists on the ordinals needed for OD sets of integers, but probably it cannot be proved to be ω₁, so the proof will not give CH.
L versus OD and HOD
- L: definable from ordinals using quantifiers over L only. Satisfies AC + GCH. Every constructible real appears below ω₁.
- OD: definable from ordinals with quantifiers over V. Not transitive in general.
- HOD: sets hereditarily OD (the set, its members, their members …). A transitive inner model of ZFC, so it gives Gödel's "simpler" consistency proof of AC (Myhill–Scott 1971).
- Inclusions: L ⊆ HOD ⊆ OD ⊆ V. Since every Vα is OD and HOD is transitive, V = OD, HOD = OD and V = HOD are equivalent.
A puzzle. How could Gödel in 1946 have known that some definable set of integers is not provably constructible? The first published consistency proof of a non-constructible set of integers is Cohen (1963); Solovay (1967) later showed that measurable or Ramsey cardinals imply analytically definable non-constructible sets of integers.
The denumerability objection
- The objection: admitting all ordinals as primitive terms is "too cheap a way out", since uncountably many sets become definable, while it is plausible that "all things conceivable by us are denumerable". Parsons reads this as: only denumerably many things are conceivable.
- Gödel's reply: if mathematical definability is itself to be mathematically definable, every ordinal must be definable, or one could define "the first ordinal not definable", a contradiction (the paradox of the least indefinable ordinal).
- Consequence: a denumerable notion of definability is not impossible, but would involve "some extramathematical element concerning the psychology of the being who deals with mathematics".
- What OD does capture: in an absolute sense, the property of "being formed according to a law" as opposed to "by a random choice of the elements". The ordinals contain no randomness, especially on von Neumann's definition, which rests on no possibly random well-ordering of sets.
- Limits of absoluteness: both notions are absolute only "with respect to a certain system of things, namely the sets"; whether any epistemological notion can be treated "in a completely absolute way" is "of an entirely different nature".
Parsons on the modal "can". Definability contains a modal element ("can be defined"). Counting every ordinal as definable is an extreme abstraction of mathematical possibility, like ignoring hardware and time limits for computability. An ordinal definition uses only finitely many ordinals (reducible to one), so denying that OD sets are "really" definable means positing ordinals that are never definable, however our means are extended: hard to defend without bringing in "the psychology of the being". (Hazen argues that a physicalist theory of mind would supply such a cardinality restriction.)
What became of ordinal definability
| Year | Who | Result |
|---|---|---|
| 1952–53 | Post | Rediscovers OD; abstract too cryptic; dies soon after |
| 1961 | Takeuti | Idea implicit |
| early 1960s | Myhill, Scott | OD definable in ZF; HOD ⊨ ZFC; OD = L for second-order definability |
| 1965 | Lévy | Cohen's model of V ≠ L + GCH has L = HOD |
| 1966 | McAloon | V = HOD consistent with ¬CH (confirms Gödel's doubt); also L ⊊ HOD ⊊ V; V = OD consistent with a measurable |
| 1970 | Solovay | From an inaccessible: model of ZF + DC where every set of reals is Lebesgue measurable, via sets hereditarily definable from countable sequences of ordinals |
| 1973 | Menas | V = OD consistent with supercompacts |
Gödel's 1968 footnote reports McAloon's result: consistency with ZF of "all sets are ordinal definable" together with 2ℵ₀ much greater than ℵ₁. Gödel may have seen this as a virtue: V = HOD could coexist with the kind of axiom he speculated in 1947 would refute CH. Parsons notes Wang's report that in 1941 Gödel had yet another general method for the consistency of AC, so HOD may not have been his main interest. The whole talk is, for Parsons, another application of Gödel's realism to concrete problems.
Since then. HOD has moved to the centre of the search for the "right" axioms. Woodin's HOD dichotomy (2010): if δ is extendible, either HOD is close to V (computes successors of singular cardinals correctly, covers like L) or far from it (every regular cardinal above δ is measurable in HOD). The HOD Conjecture asserts the first case; it is open, and Aguilera, Bagaria and Lücke (2024) introduced exacting and ultraexacting cardinals, natural reflection principles that imply V ≠ HOD and, combined with extendibles, would refute the HOD Conjecture, so the question has become sharper than ever. The Ultimate-L axiom would imply V = HOD. On provability, Woodin's Ω-logic is the closest realization of Gödel's dream of a completeness theorem relative to large cardinals: under the Ω-conjecture, Ω-validity is generically invariant, but it also shows that large cardinals alone cannot settle CH.
Takeaway. Four pages of conference remarks gave set theory OD and HOD, foresaw that HOD proves AC but not CH, and framed the still-live programme of absolute provability through axioms of infinity.
The Continuum Problem in Gödel's Hands: Moore's Guide
Gregory H. Moore introduces 1947 and its revision 1964, Gödel's only expository article. The continuum problem was a focus of his research from 1935 until his death: he proved CH consistent, tried and failed to prove it independent, argued that independence would not solve it, and spent his last attempts on new axioms that first pointed to 2ℵ₀ = ℵ₂ and then, briefly, to CH. Moore's note shows a constant core under the changing verdicts: Gödel held that CH has a definite truth value in a well-determined reality of sets, and that only new axioms, justified intrinsically or by their fruits, could find it.
The problem before Gödel
1873–74: Cantor proves R is not countable; asks Dedekind whether a segment and a square have the same power.
1878: yes, for every dimension n; Cantor states the weak CH: every uncountable set of reals has the power of R ("two-class theorem").
1883: with well-ordering, the stronger form: R has the power of the countable ordinals; later 2ℵ₀ = ℵ₁. Also 2ℵ₁ = ℵ₂ for real functions.
1884: uncountable closed sets have the power of R; Cantor twice believes he has proved CH and briefly that he has refuted it.
1904: J. König "disproves" CH at the Heidelberg congress; Zermelo finds the gap next day. Corrected: 2ℵ₀ ≠ ℵα+ω; with Hausdorff: 2ℵ₀ never has cofinality ω.
1908: Hausdorff formulates GCH; Tarski (1925) names it.
1903–1916: weak CH extended to Gδ (Young), Gδσ (Hausdorff 1914) and all Borel sets (Hausdorff, Aleksandrov 1916).
1917: Luzin–Suslin: analytic (Σ¹₁) sets have the perfect set property. Then progress stops: for Π¹₁, only "ℵ₁ or 2ℵ₀" (Kuratowski 1933).
1914–34: Luzin, Sierpiński study consequences and equivalents of CH (Hypothèse du continu, 1934).
1923–26: Hilbert claims proof theory will settle CH and sketches a "continuum theorem"; widely doubted.
1923: Skolem conjectures CH is undecidable in Zermelo's system.
c. 1930: Zermelo notes that CH is decided in second-order ZF, since all second-order models are Vκ for inaccessible κ.
1935: Luzin's "second continuum hypothesis" 2ℵ₀ = 2ℵ₁, contradicting CH.
Gödel's own work before 1947
- 1935: restricting each level of the cumulative hierarchy to first-order definable sets gives a class model of ZF; first only AC holds there; by 1937 also GCH.
- 1938: inclined to accept V = L as "a natural completion of the axioms", hence GCH as true.
- Dec 1937 letter to Menger: consistency of GCH proved; told only von Neumann; "Right now I am also trying to prove the independence of the continuum hypothesis". He never succeeded.
- 1942: proofs of the independence of V = L and of AC in type theory. Church's Fields Medal address for Cohen (1966) reported this; Gödel's 1967 letter to Rautenberg confirmed only partial results, by a method close to Scott's Boolean-valued models, and "never … a proof for the independence of the continuum hypothesis".
- By 1947: convinced, against his 1938 view, that CH and V = L are false.
How the paper was written. Lester Ford, editor of the American Mathematical Monthly, asked on 30 Nov 1945 for a "What Is?" article, suggesting "What is the problem of the continuum?", short and "simple, elementary and popular". Ford wanted it by July 1946; Gödel, "an extreme perfectionist", finished it, reread it, added insertions, and sent it on 29 May 1947 to the new editor Newsom. The many footnotes were renumbered in proof without fixing internal references (corrected here). Newsom: "by far the best article in volume 54".
What 1947 says
Four sections
- Cardinal number. Cantor's notion is unique given the minimal requirement that equal cardinals mean a one-to-one correspondence; the alephs give a "natural" representation, and with AC every cardinal is an aleph, so "Which ℵα is 2ℵ₀?" is meaningful. AC is consistent (1940), as self-evident as the other axioms, and provable for sets as "extensions of definable properties".
- What is known. Only König's cofinality result and the weak CH for Σ¹₁ sets. Unknown: any upper bound for 2ℵ₀; whether it is accessible or weakly inaccessible, singular or regular; any further cofinality restriction; even whether 2ℵ₀ < 2ℵ₁. Ignorance about the continuum is part of ignorance about infinite cardinal products.
- Philosophy. The concept of set needs "a more profound analysis … than mathematics is accustomed to give". Intuitionism is rejected as destructive; the iterative "set of" conception (with urelements allowed) has never led to antinomy. The axioms are not closed: the concept suggests new axioms asserting further iterations of "set of".
- Proposal. CH is probably undecidable; proving this is the most promising attack, but would not solve the problem; new axioms might, judged intrinsically or by fruitfulness.
"Only someone who (like the intuitionist) denies that the concepts and axioms of classical set theory have any meaning … could be satisfied with such a solution, not someone who believes them to describe some well-determined reality. For in this reality Cantor's conjecture must be either true or false." Gödel 1947, p. 520
Two reasons to expect independence:
- Two models. The constructible sets and "sets in the sense of arbitrary multitudes" both satisfy the axioms. From an axiom "directly opposite" to V = L, ¬CH might follow. (Moore: mere ¬(V = L) is too weak; Gödel meant a maximality axiom, as 1964 makes explicit.)
- "Paradoxical" consequences of CH: very thin subsets of R of full power 2ℵ₀, e.g. Sets of first category on every perfect set, sets mapped to measure zero by every homeomorphism, sets of absolute measure zero.
Moore's critique of the thin-sets argument. Gödel answered the obvious reply (Peano curves are also counterintuitive) by blaming a mismatch between geometric intuition and set-theoretic concepts. But analysts and set theorists do not find these sets paradoxical: Cohen was "not troubled"; D. A. Martin (1976): "it is even hard for some of us to see why the examples Gödel cites are implausible at all". And Gödel's claim that "not one plausible proposition is known which would imply the continuum hypothesis" was "uncharacteristically incautious": in 1970 he himself proposed one.
The 1964 revision
- Origin. Benacerraf and Putnam asked to reprint 1944 and 1947. Gödel feared positivistic attacks in their introduction and sought editorial control; promised a look at it, he agreed and revised 1947 extensively, meeting Benacerraf repeatedly, ever alert to unwanted readings.
- Over 100 changes, mostly stylistic ("Germanic" sentences shortened); "natural" representation becomes "systematic".
- Ordinal definability omitted entirely, for unknown reasons. A draft credits Zermelo (1930) with "substantially the same solution of the paradoxes" as the "set of" hierarchy; this was not adopted.
- Footnote 20: Scott (1961): a measurable cardinal contradicts V = L, so the L proof of CH fails under it. (Later: Lévy–Solovay 1967: CH and ¬CH both consistent with measurables; Silver 1971: GCH holds in L[μ].) In 1966 Gödel argued that measurables exist, from generalizations of Stone's representation theorem.
- Footnote 23, maximality: an axiom "similar to Hilbert's completeness axiom in geometry" stating "some maximum property of the system of all sets, whereas axiom A [V = L] states a minimum property". To Ulam he praised von Neumann's axiom (a class is proper iff equipotent with V) as such a principle, which explains why it implies AC.
- Supplement and postscript: Cohen's independence proof confirms 1947; Platonism is strengthened ("someone who considers mathematical objects to exist independently of our constructions").
Errera versus Gödel: is CH like the parallel postulate?
- Errera (1952): if CH is undecided, its truth loses meaning, as the parallel postulate did after non-Euclidean geometry.
- Gödel (1964): set theory differs mathematically and epistemologically. "There is an inaccessible" has consequences for number theory; its negation does not. CH is sterile for number theory, because N is absolute for L; some other assumption about 2ℵ₀ might not be.
- Later precision: Platek (1969) (also Kripke, Silver): anything in second-order number theory (indeed any Π²₁ statement) provable from CH is provable in ZFC; Solovay (1965): the same for ¬CH and Π¹₃ sentences. Both CH and ¬CH are arithmetically sterile.
"Despite their remoteness from sense experience, we do have something like a perception also of the objects of set theory, as is seen from the fact that the axioms force themselves upon us as being true." Gödel 1964, p. 271
1966 addendum: Cohen's work is "the greatest advance in the foundations of set theory since its axiomatization"; all known large-cardinal axioms are insufficient to decide CH (Lévy–Solovay).
What later research did to the programme
| Question in 1947 | Answer since |
|---|---|
| Upper bound on 2ℵ₀? | None: Cohen 1963; Solovay 1965: 2ℵ₀ = ℵα consistent for every ℵα of uncountable cofinality |
| Accessible? Regular? | Any of these is consistent |
| 2ℵ₀ < 2ℵ₁? | Not provable: Feferman showed 2ℵ₀ = 2ℵ₁ consistent (Luzin's second CH) |
| Continuum function on regulars | Easton 1964/70: any non-decreasing F with cf F(κ) > κ |
| Singular cardinals | Silver 1974: GCH below singular κ of uncountable cofinality ⇒ at κ; Galvin–Hajnal 1975; Magidor 1977: 2ℵω = ℵω₊₂ with GCH below; Shelah 1982 bounds 2ℵω |
| Exponentiation via gimel | Stated by Gödel 1947; proved Bukovský 1965 |
| Weak CH for Σ¹₂, projective | Solovay 1969 (measurable): Σ¹₂; Martin–Steel: from Woodin cardinals, projective determinacy, all projective sets |
| Maximality principles | PFA⁺, Martin's Maximum (Foreman–Magidor–Shelah) and then PFA alone (Todorcevic) imply 2ℵ₀ = ℵ₂ |
Jensen's covering theorem adds an irony: although no large cardinal decides CH, the negation of one (no 0#) settles the continuum function at singular cardinals (SCH). Foreman's axiom of resemblance (1986) implies GCH, probably disqualifying it for Gödel.
The unpublished 1970 papers
The square axioms and the ℵ₂ paper
- Jan 1964, to Cohen: the key question is whether there is a set of ℵ₁ sequences of integers dominating every sequence eventually; Gödel suspected it "correct and perhaps even demonstrable".
- Square axioms (1970): for each n, a scale of type ωn+1 of functions from ωₙ to ωₙ (eventual domination); perhaps inspired by Borel 1898.
- "Some considerations leading to the probable conclusion that the true power of the continuum is ℵ₂", for PNAS: axioms 1 (squares), 2 (exactly ℵₙ initial segments), 3 (a maximal scale with all monotone sequences of cofinality ω), 4 (Hausdorff continuity; implies 2ℵ₀ = 2ℵ₁).
- The error. Tarski passed it to Solovay; Martin noticed a clash: Solovay had shown in 1965 (at Gödel's own request) that the square axioms do not bound 2ℵ₀. Gödel had refused to accept this despite Prikry's assurance, until Ellentuck rediscovered it around 1973.
- Second version, marked "nur für mich geschrieben": "A proof of Cantor's continuum hypothesis from a highly plausible axiom about orders of growth". The square axiom for ℵ₁ is "much more plausible than CH" and implies it (Takeuti: a scale from ω₁ to ω₀ implies CH).
- Draft letter to Tarski (unsent): the first version was written hurriedly after an illness and medication; his conviction that 2ℵ₀ = ℵ₂ is "somewhat shaken. But it still seems plausible", partly because "I don't believe in any kind of irrationality such as, e.g., random sequences in any absolute sense".
Since then. Gödel's late guess 2ℵ₀ = ℵ₂ is exactly what the strongest forcing axioms give: PFA (Todorcevic, Veličković) and Martin's Maximum imply it, and Asperó–Schindler (2021) proved that MM⁺⁺ implies Woodin's axiom (*), uniting the two leading ¬CH programmes, both yielding ℵ₂. On the other side, Woodin's Ultimate-L conjecture would make CH true, and Woodin moved from favouring ¬CH (2000s, via Ω-logic) to favouring Ultimate L. The multiverse view (Hamkins 2012) rejects Gödel's premise that CH has a single answer. Gödel's thin-set intuitions remain largely unshared; his maximality idea lives on in forcing axioms and in Friedman's inner model hypothesis.
Takeaway. Gödel was right that CH is independent and that independence would not end debate; his specific arguments (thin sets, the 1970 proofs) failed, but his programme of deciding CH by justified new axioms, especially maximality principles, defines the field today.
What Is Cantor's Continuum Problem? (1947)
Written for the American Mathematical Monthly, this is Gödel's only expository paper: four sections that move from the meaning of "how many" to the state of cardinal arithmetic, to a philosophical restatement of the problem, and finally to a forecast. Its argument in one line: the axioms of set theory are incomplete but extendable without arbitrariness, CH is probably independent of them, and its role will be to lead "to the discovery of new axioms which will make it possible to disprove Cantor's conjecture".
1. Why "how many" has a unique answer
The problem. "How many points are there on a straight line in Euclidean space?" or equivalently, "How many different sets of integers do there exist?" One might doubt that "number" extends to infinite sets in a unique way. Gödel argues it does, "in a very striking manner".
The mass-point argument
- Whatever infinite "number" means, the number of objects in a class must not change if one alters only their properties or relations (colour, position).
- If A and B are in one-to-one correspondence, one can (in principle) change each element of A to match its partner in B, making A indistinguishable from B.
- So sets in one-to-one correspondence have the same number: Cantor's definition. Example: a square and a segment filled with mass points can be rearranged into each other.
- The argument applies directly to physical objects, but a notion of number depending on what is counted "could hardly be considered as satisfactory".
- "Less than" follows: |A| < |B| if different and |A| equals the cardinal of a subset of B.
- Then: infinitely many infinite cardinals; 2|A| > |A|; arithmetic extended without arbitrariness to infinite sums and products.
A systematic notation. The problem would still be ill-posed without a representation of cardinals comparable to decimal notation. It exists: every cardinal and every set of cardinals has a unique immediate successor, and every set's cardinal appears in the resulting series: ℵ₀, ℵ₁, …, ℵω, ℵω₊₁, … This needs AC, which (note 2) "is, in the present state of knowledge, exactly as well-founded as the system of the other axioms": consistent relative to them, equally evident for arbitrary multitudes, and provable for sets as extensions of definable properties.
2. A pronounced failure
60+ years of set theory and only 2 results on the size of the continuum:
(1) 2ℵ₀ is not a limit of countably many smaller cardinals (König 1905, who "asserted more than he had actually proved"; Hausdorff).
(2) The weak CH holds for the analytic sets, "a certain infinitesimal fraction" of all subsets; for their complements only "ℵ₀, ℵ₁ or 2ℵ₀" is known (Kuratowski).
0 upper bounds, "however high".
0 knowledge of its quality: regular or singular, accessible or inaccessible, cofinality.
- Cardinal arithmetic. 2ℵ₀ is the simplest non-trivial infinite product (ℵ₀ factors of 2). For no infinite product is even an upper bound known. Only lower bounds (Cantor, König) and reductions (via Tarski 1925) to the values ℵαcf(ℵα) plus ordinal operations.
- With GCH everything is computable; without it, not even whether m < n implies 2m < 2n, nor whether 2ℵ₀ < 2ℵ₁.
3. Restating the problem through foundations
The scarcity of results has "deeper reasons": a complete solution needs "a more profound analysis (than mathematics is accustomed to give) of the meanings of the terms" ("set", "one-to-one correspondence") and of the axioms.
Three foundational standpoints
- Brouwer's intuitionism: "utterly destructive": the theory of alephs beyond ℵ₁ is meaningless; CH splits into several different questions with mixed answers.
- Half-intuitionism (Poincaré, Weyl): hardly preserves more. (Note 11: iterating Weyl's construction transfinitely would yield exactly the reals of L, where CH holds, but that iteration lies outside the standpoint.)
- Axiomatic set theory: a "satisfactory foundation of Cantor's set theory in its whole original extent", with Principia (suitably interpreted) subsumed. The negative attitudes stem only from philosophies admitting objects insofar as they are our constructions or "completely penetrable by our intuition".
The iterative concept defuses the paradoxes. The paradoxes "are a very serious problem, but not for Cantor's set theory". Sets in mathematics are sets of integers, of reals, of functions of reals, and so on. A set is "anything obtainable from the integers (or some other well-defined objects) by iterated application of the operation 'set of'", including transfinite iteration, "and not something obtained by dividing the totality of all existing things into two categories". This concept "has never led to any antinomy whatsoever".
- Note 13: "set of" cannot be defined, only paraphrased ("multitude of x's", "part of the totality of x's"), yet "we have a clear notion of this operation".
- Note 14: a set of all sets cannot exist, since any set gives rise to further applications of "set of".
The minimum meaning. Even the most radical intuitionist must accept the combinatorial question: can CH, or its negation, be derived from the axioms? Assuming consistency, CH is demonstrable, disprovable or undecidable; the third is "the most likely", and seeking a proof of it is "one of the most promising ways" to attack the problem. Undisprovability is already established (1940).
But independence would not settle it (unlike the transcendence of π): in a "well-determined reality" CH is true or false, and undecidability means only that the axioms are not a complete description. Two roads to a decision:
- Intrinsic. The axioms are "by no means a system closed in itself". The concept of set suggests axioms of infinity: inaccessibles (the totality obtained by the other axioms' processes is again a set; Zermelo 1930) and Mahlo's axioms (note 19: Mahlo's presentation does not show they exist). They prove the system incomplete yet extendable "without arbitrariness", and each increases the decidable Diophantine propositions. The concept "property of set" can also be enlarged, but adds nothing for limited domains like CH (note 17). Known axioms cannot decide CH, since the L proof "goes through for all of them without any change"; others may rest on "hitherto unknown principles".
- Extrinsic. Decide "inductively" by "success": fruitfulness in verifiable consequences, provable without the axiom but more simply with it. Analytic number theory already "verifies" the real-number axioms that intuitionists reject. Axioms might be so fruitful that "they would have to be assumed at least in the same sense as any well-established physical theory".
4. In what direction may a solution be expected?
First indication of unsolvability: two classes. Both the sets definable from ordinals (constructible; note 20) and "sets in the sense of arbitrary multitudes" satisfy all axioms written down so far. Before deciding which objects are counted one cannot expect to count them. And a believer in definable sets only must use that characteristic, which the axioms do not state. So CH is plausibly unsolvable now, but solvable by "a new axiom which would state or at least imply something about the definability of sets" (as Hilbert's 1926 attempt also considered all definitions of reals).
- Half verified: axiom A (every set is definable in this sense) implies GCH, and A is consistent: a proof analogous to the consistency of non-Euclidean geometry via a model inside Euclidean geometry.
- Note 22: "from an axiom in some sense directly opposite to this one the negation of Cantor's conjecture could perhaps be derived."
- Ordinals as primitives. "Definability" can be recast as a definition of "set" and "∈" from ordinals, their order, and recursively defined functions of ordinals, axiomatized as an extension of Peano's axioms (cf. Tarski 1924). Richard's paradox does not apply: the ordinals are not denumerable.
- Note 26 (OD): allowing quantification over all sets gives the ordinal-definable sets; that all sets are OD "could be expected with more reason" but is no axiom; the GCH proof fails for OD.
Second indication: implausible consequences. Some properties express "extreme rareness" of point sets; uncountable examples are known, but no route to examples of the power of the continuum. CH supplies such examples, even ones invariant (up to countably many points) under every translation.
| Thin-set property (Gödel's list) | Without CH | With CH | Today's name and status |
|---|---|---|---|
| First category on every perfect set | Uncountable examples exist | Examples of size 2ℵ₀ | Perfectly meagre sets |
| Carried to measure zero by every homeomorphism of the line | Uncountable examples exist | Size 2ℵ₀ | Universally null sets |
| Coverable by intervals of any given lengths | Not even uncountable examples known | Size 2ℵ₀ (Sierpiński) | Strong measure zero; Borel's conjecture (all are countable) is consistent: Laver 1976 |
| Covered by every dense set of intervals (no uncountable nowhere-dense subset) | Size 2ℵ₀ (Luzin 1914) | Luzin sets | |
| No uncountable null subset | Size 2ℵ₀ | Sierpiński sets | |
| Subsets of Hilbert space with no uncountable finite-dimensional subset | Size 2ℵ₀ (Hurewicz) | Equivalent to CH | |
| Braun–Sierpiński decompositions | Exist | Equivalent to CH |
Even with ℵ₁ in place of the continuum these are "very implausible". Counterintuitive results without CH (Peano curves) are explained by a mismatch between geometric intuition and set-theoretic concepts.
"It is very suspicious that, as against the numerous plausible propositions which imply the negation of the continuum hypothesis, not one plausible proposition is known which would imply the continuum hypothesis." Gödel 1947, p. 524
Appendix of definitions. Sixteen terms (cofinality, regular, inaccessible in two senses, dense, zero set, nowhere dense, first category, perfect, Borel, analytic, quantifiers). A curiosity: 0 and 2 are the only finite numbers "inaccessible in the stronger sense", which "suggests that the same will hold also for the correct extension of the concept of inaccessibility to finite numbers"; the two senses coincide under GCH.
Critical lens.
- The uniqueness argument is physical. It rests on rearranging mass points, then generalizes from physical to all objects by fiat ("hardly … satisfactory" otherwise).
- The thin-sets argument persuaded few (Martin, Cohen; see the previous chapter), and the claim that no plausible proposition implies CH was refuted by Gödel's own 1970 square-axiom draft and, later, by axioms such as Ultimate L.
- "Directly opposite" to V = L was left vague; ¬(V = L) is far too weak, and the measurable cardinals that refute V = L still leave CH open.
- The forecasts were sound: independence (Cohen 1963), the failure of known large cardinals for CH, and the need for truly new principles.
Since then. Gödel's "extrinsic" criterion of fruitfulness is now the standard defence of large cardinals (Maddy, Defending the Axioms, 2011): projective determinacy is accepted largely because it gives a complete, regular theory of the projective sets, exactly the "abundance of verifiable consequences" he described. Strong measure zero and the Borel conjecture became a major theme of the combinatorics of the reals; the modern Cichoń diagram classifies Gödel's thin-set cardinals, and Goldstern, Kellner and Shelah (2019) showed that its ten non-trivial cardinals can all be pairwise distinct ("Cichoń's maximum", first from large cardinals, then without them with Mejía, 2022).
Takeaway. 1947 defines the continuum problem's modern shape: independence is likely but not decisive, the iterative concept of set guides new axioms, and such axioms may be justified by intrinsic necessity or by success, like physical theories.
A Rotating Universe with Closed Timelike Lines (1949)
Gödel's first paper in physics, prepared alongside his essay for the Einstein volume, gives an exact solution of Einstein's field equations in which matter rotates relative to the "compass of inertia", there is no absolute time, and there exist closed timelike lines: it is in principle possible "to travel into the past". Stephen Hawking's note explains why this mattered. The Gödel universe was the first solution of general relativity shown to permit time travel, and it proved that general relativity does not incorporate Mach's principle: two results that opened the modern study of causality in spacetime.
Hawking's note: why rotation matters
- The background. The Friedmann–Robertson–Walker models of the 1920s–30s were the simplest solutions consistent with the galactic red-shift: spatially homogeneous, isotropic, expanding and non-rotating. Gödel was the first to consider rotating models.
- Mach's principle, one influence behind Einstein's theory, is obscure but usually read as denying absolute space: matter has inertia only relative to other matter, so gyroscopes should not rotate relative to the distant galaxies.
- Gödel's lesson. Solutions exist in which the galaxies rotate relative to the local inertial frame, so general relativity does not incorporate Mach's principle. Most physicists now reject the principle, since it draws an untenable line between spacetime geometry (the gravitational and inertial field) and other fields and matter.
- Time travel. 1949 is stationary, non-expanding and the same at all points, and the first solution found in which one can travel into the past, raising the "kill your father as a baby" paradox. Physicists agree this cannot happen in our universe, but Gödel showed it is not forbidden by Einstein's equations, provoking much work on relativity and causality.
- 1952 gives expanding rotating models without time travel, possibly realistic, though the isotropy of the microwave background shows any rotation must be very slow.
The nine properties of the solution
All known cosmological solutions with matter contain, in a sense, an absolute time: a one-parameter family of 3-spaces orthogonal to the world lines of matter. The non-existence of such a family is equivalent to rotation of matter relative to the compass of inertia. Gödel's solution S (with cosmological constant λ ≠ 0) has:
Properties of the Gödel universe S
- Homogeneous: any point can be mapped to any other; physically, stationary and spatially homogeneous.
- A one-parameter group maps each world line of matter into itself: all world lines are equidistant.
- Rotational symmetry about every point.
- Time-orientable: a consistent positive direction of time exists everywhere.
- No global time coordinate t that always increases along future-directed timelike lines, whether open or closed (cyclic).
- Matter world lines are open and infinite, but closed timelike lines exist: for P before Q on a matter world line there is a timelike line from P to Q on which Q precedes P. "It is theoretically possible in these worlds to travel into the past, or otherwise influence the past."
- No spacelike 3-space meets every world line of matter exactly once.
- No absolute time, even one not required to agree with every observer's time: any system of disjoint 3-spaces crossing all matter world lines is moved by some symmetry, so it is not definable without reference to individual objects such as a particular galaxy.
- Matter rotates relative to the compass of inertia with angular velocity 2(πκρ)½ (ρ the mean density, κ Newton's constant).
The metric and the field equations
The line element (in units with time in seconds, distance in light-seconds), with a > 0:
ds² = a² [ (dx₀ + eˣ¹ dx₂)² − dx₁² − ½ e²ˣ¹ dx₂² − dx₃² ]
- Signature everywhere −2; only two of the forty derivatives ∂gᵢₖ/∂xₗ are non-zero, so the Christoffel symbols and Ricci tensor are easy to compute.
- Matter moves along the x₀-lines. The field equations hold with 1/a² = 8πκρ and λ = −R/2 = −1/(2a²).
- The cosmological constant has the opposite sign to Einstein's static universe; it corresponds to a positive pressure. (Note 7 warns of sign conventions: physicists often write −Rᵢₖ.)
Proofs in outline.
- Rotation (and no orthogonal 3-spaces): a vector field admits orthogonal hypersurfaces iff the vorticity vector w built from its curl vanishes; here w has components (0, 0, 0, √2/a²), and w is twice the angular velocity of matter in a local inertial frame, giving property 9.
- Homogeneity and equidistance: four explicit families of transformations.
- Time orientation: ξ is future-pointing iff its inner product with the matter velocity u is positive.
- Rotational symmetry: new cylindrical coordinates (r, φ, t, y) give ds² = 4a²[dt² − dr² − dy² + (sh⁴r − sh²r) dφ² + 2√2 sh²r dφ dt], independent of φ.
- Closed timelike lines: for r > ln(1 + √2), sh⁴r − sh²r > 0, so the circle r = R is timelike. Slightly tilting it gives a timelike curve ending before its start on the t-line; repeating, any earlier point is reachable, and homogeneity carries this everywhere.
- Properties 5, 7, 8 follow from 6, simple connectivity, and a rotation argument showing any candidate family of time slices can be moved to a different family.
Geometry and uniqueness
- Uniqueness (stated without proof): up to global connectivity, S and Einstein's static universe are the only spatially homogeneous solutions with matter and equidistant world lines. Non-equidistant stationary solutions face internal friction in the "gas" of galaxies.
- Geometric meaning: S = line × S₀, where S₀ comes from a space R of constant positive curvature and signature (+ − −) by stretching the metric in ratio √2 : 1 along a system of timelike Clifford parallels (the world lines of matter). The same 3-space appears in Bianchi's group theory.
- Hyperbolic quaternions: with units built from ordinary quaternion units times i, motions of R are u ↦ p·u·q; those preserving the Clifford system form the four-parameter group of S₀. Gödel argues this number system "should be so called", since its norm is multiplicative and its projective group is that of the Lobachevskian plane.
Physical meaning
0 red-shift: signals between matter particles arrive at the intervals they were sent.
2 × 10¹¹ years: rotation period of the universe, for ρ = 10⁻³⁰ g/cm³.
1 : 200: assumed contraction ratio (diameter : distance of galaxies).
5 × 10⁶ years: predicted average rotation period of galaxies, by conservation of angular momentum.
2 × 10⁷ and 7 × 10⁷ years: Hubble's values for two medium galaxies; Andromeda's centre about 1.5 × 10⁷.
Gödel concedes that comparison means little "before an expansion has been combined with the rotation", and that the irregular orientation of galactic axes needs explanation (perhaps blurred if axes in different places are not parallel, unlike in S). The smallest timelike circles have radius of the order of the world radius of Einstein's static universe.
Critical lens.
- Not our universe. No expansion, no red-shift, and a negative cosmological constant in Gödel's convention (with the modern sign, the solution needs λ < 0 together with dust, or equivalently a stiff fluid); observations rule it out.
- The time-travel loops are enormous: the critical radius is cosmological, and the curves needed require huge accelerations (Gödel's own estimate in 1949a: fuel far beyond practical limits).
- But the point is logical: the field equations alone permit causality violation; any ban must come from extra principles.
Since then. Gödel's solution launched the global causal theory of spacetime (Hawking–Ellis 1973, Malament). Hawking's chronology protection conjecture (1992) proposes that quantum effects forbid closed timelike curves, and remains unproved. Other CTC solutions followed: van Stockum/Tipler cylinders, Kerr interiors, Morris–Thorne–Yurtsever wormholes (1988), Gott's cosmic strings (1991). Gödel-type metrics reappear as exact supersymmetric solutions of five-dimensional supergravity (Gauntlett et al., 2003), where string theory appears to "protect" chronology holographically. Observationally, Planck-based analyses (Saadeh et al. 2016) disfavour any global vorticity or anisotropy of the expansion by odds of about 121,000 : 1.
Takeaway. In a few pages Gödel showed that Einstein's equations allow rotating matter, no cosmic time and travel into the past, refuting the idea that general relativity enforces Mach's principle or a global causal order.
Relativity and Idealistic Philosophy (1949a)
Written for Schilpp's volume Albert Einstein: Philosopher-Scientist, this short essay is Gödel's only published philosophy outside mathematics. From his rotating universes he argues that those philosophers are right, "like Parmenides, Kant, and the modern idealists", who deny the objectivity of change and treat it as "an illusion or an appearance due to our special mode of perception". The decisive step: if worlds without any absolute time are compatible with the laws of nature, then in our world too an "objective lapse of time" would depend on the accidental arrangement of matter, which "can hardly be considered as satisfactory".
Stein's note: what "idealism" means here
- A caution on the title. "Idealism" names many views whose common thread is that the ultimately real is mental. Not all deny change (minds can change), and denying change need not make reality mental. Gödel argues from the physical possibility of strange worlds; his conclusion is that our conception of the world as changing is subjective, a contribution of our minds, not that physics rests on the mental.
- Kant's transcendental ideality. For Kant space and time characterize not things in themselves but their relation to our faculties; yet within experience they are empirically real and known a priori as forms of intuition. Gödel cannot follow the a priori part: his examples depart radically from the structure Kant thought necessary, and he stresses their "astonishing" character.
- The unpublished Kant manuscript. "Some observations about the relationship between theory of relativity and Kantian philosophy" says Kant overemphasized dependence on our faculties and made two errors: thinking temporal properties are the same for all humans, and missing that geometry is (in one sense) empirical. The real analogy: in relativity, temporal properties are defined only relative to world lines, and for sentient beings these are the loci of sensory contact with the world.
- A tension. The essay calls change an illusion; the manuscript stresses the objective character of these relations. "To be relative is not to be illusory." Stein wishes for dates and for the epistemology, of which only fragments exist (an a priori "physical intuition" of space in the small, per a letter quoted by Greenberg 1980).
Stein on time-travel "paradoxes" (note a). Gödel defends his worlds against absurdity by the impracticality of the journey. Stein finds the defence unnecessary: "What if I went back and murdered my younger self?" has a simple answer: in such a cosmos that act is not possible. Such a world is fully determinate, which Gödel's own argument implies anyway, and classical physics was deterministic too. "But I can always choose whether to lift my arm" never carried weight against determinism; the time-travel version is "more poignant" but the same type of objection.
The argument
Step by step
- Special relativity: simultaneity is relative, and with it, for many pairs of events, succession. (Note 2: there is still an absolute partial order.)
- Objective lapse of time means reality consists of "an infinity of layers of 'now' which come into existence successively".
- With relative simultaneity, reality cannot be split into such layers objectively: "each observer has his own set of 'nows'", none privileged. So change is not objective.
- Objection (Jeans 1936): the equivalence of observers holds only in empty or abstract spacetimes. Matter distinguishes observers who follow the mean motion of matter, and in all known cosmologies their local times fit into one world time, which can be taken as the "true" time.
- Reply: Gödel's rotating universes admit no such world time; any notion of simultaneity is matched by others indistinguishable intrinsically, differing only by reference to individual objects (a particular galaxy).
- Time travel strengthens this: a round trip "in a sufficiently wide curve" reaches any region of past, present and future. For every possible world time, one can travel into regions past according to it, so some observers' experienced lapse of time has no objective counterpart. "If the experience of the lapse of time can exist without an objective lapse of time, no reason can be given why an objective lapse of time should be assumed at all."
- Transfer to our world: (a) expanding rotating solutions may also lack absolute time, and our world might be one; (b) the mere compatibility with the laws of nature of worlds without absolute time shows that, even where one exists, whether "time in the ordinary sense" exists would depend on how matter happens to move: not a contradiction, but unsatisfactory.
Defences in the footnotes
- Meaningless or self-contradictory? (note 4) Calling objective time lapse meaningless is no escape: it too denies that such lapse is possible, the idealist conclusion. Relativity offers a second proof on different grounds, of interest because the thesis "runs so completely counter to common sense" (cf. McTaggart 1908, Mongré 1898).
- "Relative but objective"? (note 5) A relative lapse of time would be "entirely different" from lapse in the ordinary sense, "a change in the existing", and "the concept of existence cannot be relativized without destroying its meaning". A lapse "which is not a lapse in some definite way" is as absurd as "a coloured object which has no definite colours".
- Kant's own words (note 3): beings with other forms of cognition would have perceptions in which "the idea of time, and therefore also of change, would not occur at all", tempting Gödel to add: "such as, e.g., a perception of the inclination … of the world lines of matter in Minkowski space".
- Distinguished observers (note 6): the laws are the same for all, but the actual arrangement of matter offers a "natural" aspect to some and a distorted one to others; the world itself "has certain distinguished directions".
- Mean motion (notes 7, 9): depends on the size of averaging regions; a precise definition may need arbitrary choices (region size, weight function), so Jeans's absolute time is only approximate.
10²² / t²: fuel-to-ship weight ratio for a trip into one's own past taking t years (traveller's time), assuming total matter-to-energy conversion and observed mean density; valid for t ≪ 10¹¹.
1/√2 c: minimum speed of the ship, whatever t.
≈ 1: fuel-to-ship ratio sufficient merely to reach regions past according to any given world time (note 12).
Additions to the German edition (1955).
- Telegraphing into one's past would be another reason to exclude such worlds a priori, but the practical difficulties are not trifling, and "the boundary between difficulties in practice and difficulties in principle is not at all fixed": the uncertainty principle turned a practical limit into one of principle, and the same might happen for the "too large".
- Absolute time means a world time definable without reference to particular objects and agreeing in direction with all observers' times; strictly a "possible absolute time", since several can exist.
- The second law of thermodynamics is compatible with these worlds: a positive time direction exists for all timelike lines; exact return to a former state is vanishingly improbable, and approximate return just means two copies of a system side by side. Initial conditions cannot be chosen freely.
- Note added 2 September 1949: for every value of the cosmological constant there are solutions with no world time of the required kind.
"Kurt Gödel's essay constitutes, in my opinion, an important contribution to the general theory of relativity, especially to the analysis of the concept of time. The problem here involved disturbed me already at the time of the building up of the general theory of relativity, without my having succeeded in clarifying it." Einstein, reply in Schilpp 1949
Critical lens.
- Modal leap. From "a world without absolute time is possible" to "time does not objectively lapse here" needs a premise that the nature of time cannot depend on contingent matter distributions. Critics (Earman 1995, Savitt, Dorato) reject this premise; Gödel calls the opposite view only "unsatisfactory", not false.
- Which time? Our universe has a natural cosmic time (FRW comoving observers), and its rotation is observationally negligible.
- Defenders (notably Yourgrau, Gödel Meets Einstein 1999, A World Without Time 2005) read the essay as a serious argument for the block universe, unjustly neglected by philosophers of physics.
Since then. The Kant manuscript Stein mentions was published in Collected Works III (1995) as drafts *1946/9-B2 and C1, which also contain Gödel's estimates of the Milky Way's rotation and his sympathy for Kant's ideality of time. The debate between eternalism (block universe) and presentism remains live; relativity-based arguments against presentism (Putnam 1967, Rietdijk) parallel Gödel's first step, and his second step, from possible spacetimes to the actual nature of time, remains the most discussed and most contested part.
Takeaway. Gödel uses his rotating universes as a philosophical counterexample: if the laws of nature allow worlds where no time can lapse objectively, an objective lapse in our world would be a mere accident of matter, so change is best seen as appearance.
Rotating Universes in General Relativity Theory (1952)
Gödel's lecture to the International Congress of Mathematicians (Cambridge, Massachusetts, 1950; published 1952) moves from the static, time-travel-permitting world of 1949 to expanding, spatially finite, homogeneous rotating universes that could describe our own. Mostly without proofs, he gives their symmetry groups, the exact condition for closed timelike lines, how rotation evolves with expansion, existence theorems and observable signatures. His key result: for every value of the cosmological constant, including zero, there are ∞⁸ such rotating solutions, some arbitrarily close to the standard isotropic model and some with a perfectly good world time, so rotation is no exotic feature of general relativity.
The setting and three postulates
Assumptions: units with c = 1; field equations with cosmological term λ; galaxies close together have small relative velocities; only gravitation acts, so matter is pressureless dust with world lines that are geodesics. Rotation relative to the compass of inertia is the vector w, orthogonal to the matter velocity v, built from the curl of v; in a local inertial system it reduces to the Newtonian angular velocity.
Postulates for a rotating universe (suggested by observation and theory)
- Spatial homogeneity: a symmetry carries any world line of matter to any other.
- Finite space: the space of world lines of matter is compact.
- Non-constant density ρ: indispensable, because a red-shift growing linearly with distance implies expansion, rotating or not (provided dimensionless constants like e²/hc are the same everywhere).
General properties
- Tilted slices. ρ = const defines 3-spaces that, in a rotating universe, cannot be orthogonal to the matter world lines.
- An observable test: in an expanding, homogeneous, finite universe, rotation holds iff at large distances there are more galaxies in one half of the sky than in the other. Near isotropy the effect is computed in terms of r, w and Hubble's constant; it is "extremely small" for plausible values, but the constants are too uncertain to conclude.
- Symmetry group: cannot be 4-parameter (no rotationally symmetric rotating universes, even without finiteness); it is 3-parameter, compact, non-commutative (a field invariant under a transitive commutative group has zero curl), hence isomorphic to the right (or left) translations of a 3-sphere of constant positive curvature, possibly with rotations by π (the "symmetric" case). Space is a spherical or elliptic 3-space. (Today: Bianchi type IX.)
- Expansion is deformed. Splitting the metric into space-metric and time-metric relative to matter defines the quadric (ellipsoid) of expansion. Without closed timelike lines, it is never rotationally symmetric about w: expansion is always coupled with deformation, a second observable property.
- Spiral galaxies. In anisotropic expansion a condensation tends to become oblong, rotating about a short axis; its slower outer parts bend it into a spiral: a theory of spiral structure Gödel leaves for "quantitative elaboration".
Rotation, time and closed timelike lines
Rotation lives in the time-metric. A spatially homogeneous universe rotates iff the local simultaneity of co-moving observers is not integrable (does not define a simultaneity in the large).
- Closed timelike lines appear only if rotation exceeds a limit: roughly where the linear velocity of rotation reaches c, i.e. |w| ≈ c/R for world radius R.
- Exact criterion (when the family of constant-density spaces is not closed): no closed timelike lines iff the spaces of constant density are spacelike.
- Equivalence: for these solutions, no closed timelike lines iff a world time exists (t increasing along every future timelike line). The constant-density spaces then give a metric world time, the only one invariant under the symmetry group.
How rotation changes as the universe expands
Theorem (13), valid with or without postulates I–III, needing only that matter moves on geodesics:
- A. The vortex lines (tangent to w) always connect the same particles.
- B. |w| grows or shrinks in proportion to the contraction or expansion of matter orthogonal to w (measured by the cross-section of a thin co-moving cylinder around a vortex line): the law of conservation of angular momentum, as in Newtonian mechanics.
- Galaxy formation: the same law governs condensations forming under gravity (while gas and radiation pressure are negligible), so collapsing clouds spin up.
- Precessing axis: w is parallel-transported along matter world lines only when it lies on a principal axis of the expansion quadric, which in general (except the symmetric case) fails. Galaxies formed at different times would then have different spin directions, possibly explaining the irregular orientation of galactic axes that seemed to refute a cosmic origin of their rotation.
Existence, method and stationary solutions
| Result | Content |
|---|---|
| Existence | For any λ (including 0) there are ∞⁸ rotating solutions satisfying I–III; likewise with or without a world time |
| Freedom | Angular velocity arbitrary, even given ρ and the mean world radius |
| Near-isotropy | With λ = 0, rotating solutions arbitrarily close to the isotropic (Friedmann) one |
| Selection problem | Find natural ones, e.g. Expanding from a point and contracting to a point |
| Method | Homogeneity reduces to one world line: ordinary differential equations from a Hamiltonian principle, mechanics with finitely many degrees of freedom; symmetric case: 3 degrees (g₁, g₂, g₃) with a rotation constant; general case: 8th order system |
| Stationary homogeneous | All expressible by elementary functions; none with λ = 0 |
| Stationary with λ > 0 | Rotating, finite space, no closed timelike lines, some arbitrarily near Einstein's static universe; particles orbit each other in rotating ellipses (world lines not equidistant) |
Critical lens.
- Few proofs. Most theorems are stated without proof; the full computations were reconstructed later (the Bianchi IX analysis by Ozsváth and Schücking, and others), and some claims were refined.
- The spiral-galaxy theory never received the quantitative test Gödel hoped for; spiral arms are now explained by density waves and tidal effects.
- The observational tests he proposed are the right kind: hemispheric asymmetry and anisotropic expansion are exactly what later CMB analyses constrain.
Since then. Collins and Hawking (1973) and Barrow, Juszkiewicz and Sonoda (1985) bounded cosmic vorticity using CMB isotropy; with Planck data the ratio of rotation to expansion rate is limited to below roughly 10⁻⁹–10⁻¹⁰, and Bianchi IX-type rotation is strongly disfavoured (Saadeh et al. 2016). Gödel reportedly searched galaxy catalogues himself for a preferred sense of rotation; modern surveys (e.g. Galaxy Zoo) find no significant large-scale handedness, though claims of spin asymmetry recur and remain contested. Gödel's spatially homogeneous approach, reducing Einstein's equations to Hamiltonian ODEs, became the standard Bianchi cosmology method (Misner's mixmaster universe is Bianchi IX).
Takeaway. Rotation is generic in general relativity: a vast family of realistic expanding models rotates, closed timelike lines need fast rotation, and slow rotation would leave observable traces in galaxy counts and anisotropic expansion.
The Dialectica Interpretation: Troelstra's Guide
Anne S. Troelstra introduces Gödel's Dialectica paper (1958, in German, for Bernays's 70th birthday) and its long-delayed English revision (1972, printed here for the first time). Gödel interprets intuitionistic arithmetic HA in a quantifier-free theory T of computable functionals of finite type, so that arithmetic, classical as well as intuitionistic, is justified by notions "as intuitively clear as possible". Troelstra's verdict: the technical result is a landmark that seeded functional interpretations, normalization proofs, bar recursion and proof mining, but the philosophical gain is real yet "not clear-cut", since the logic eliminated from arithmetic reappears in the definition of the functionals.
History of the two versions
1941: Gödel lectures on the interpretation at Princeton and Yale ("In what sense is intuitionistic logic constructive?", 15 April 1941). Original aim, per Kreisel: show that intuitionistic proofs of existential theorems give explicit realizations; a technical aim was an underivability result in intuitionistic predicate logic.
1958: Dialectica paper, presented already as a foundational contribution.
1965–67: an English translation (by Boron) planned; Gödel revises and is satisfied by January 1967.
1968: dissatisfied with the philosophical introduction, rewrites it, then gives up and adds notes a–n instead. To Bernays: "In those days … it was chiefly the mathematical result that was important to me, while now it is the other way around."
1970: sent to the printer after prompting from Bernays and Scott; Gödel rewrites notes h and i in proof, but never returns the proofs.
to 1972: minor corrections continue; the paper stays unpublished. Gödel's health had been poor since 1968, and the notes "lack the sureness of touch" of his earlier work (Kreisel 1980).
The aim: a liberalized Hilbert programme
- Hilbert's finitism deals with concretely representable, surveyable configurations (school arithmetic). The general notion of a function N → N is not finitary; still more abstract is Heyting's explanation of the logical operators via constructive proofs: p proves A ∨ B if p = (0, p′) with p′ a proof of A or (1, p′) with p′ a proof of B; p proves A → B if p transforms any proof of A into a proof of B. So A ∨ ¬A fails.
- Accepting Heyting's explanation justifies HA, and with the negative translation (Gödel 1933e) also PA. Gödel (note 6): even without a clear idea of constructive proof, we do not doubt that intuitionistic laws hold for it.
- Why go beyond finitism. The second incompleteness theorem and experience with all known consistency proofs show some abstract notion is needed. To Bernays (1969): restricting Hilbert's finitism to "visualizable" objects is "quite unnatural".
- Gödel's middle path. Not the abstract notion of proof, but something more definite: computable functional of finite type, accepted as sufficiently clear to justify T, an essentially logic-free theory.
The system T
Ingredients of Gödel's T (Troelstra's reconstruction)
- Types: 0 (natural numbers) and, for types σ, τ, the type σ → τ of functionals; type 1 = 0 → 0, type 2 = 1 → 0. Many-place functions reduce to one-place ones by Schönfinkel's device.
- Language: variables for every type, application, an equality predicate =σ for each type, assumed decidable.
- Logic: intuitionistic propositional calculus with equality; with decidable prime formulas this equals classical propositional logic. No quantifiers.
- Axioms: Peano axioms for 0 and successor; induction rule; constants for explicit definition (combinators K, S or λ-abstraction); recursors Rσ at every type, giving primitive recursion in higher types.
- T₀ (suggested by note i): only numerical equations as prime formulas, higher-type equalities replaced by replacement schemas; enough for the main theorem.
A key expressive fact. Higher-type primitive recursion defines functions far beyond ordinary primitive recursion, e.g. The Ackermann function; the type-0 functions of T are exactly the provably total functions of PA, those defined by recursion on ordinals below ε₀.
The translation D
To each formula A of arithmetic Gödel assigns Aᴰ = ∃x ∀y AD(x, y), with AD quantifier-free and x, y strings of variables of finite type.
The clauses (Aᴰ = ∃x∀y AD, Bᴰ = ∃u∀v BD):
- Prime: Aᴰ = AD = A.
- A ∧ B: ∃x,u ∀y,v [AD(x,y) ∧ BD(u,v)].
- A ∨ B: ∃z,x,u ∀y,v [(z = 0 → AD(x,y)) ∧ (z = 1 → BD(u,v))]: the witness z records which disjunct holds.
- ∀z A: ∃X ∀z,y AD(Xz, y): a functional X producing witnesses uniformly in z.
- ∃z A: ∃z,x ∀y AD(x,y).
- A → B: ∃U,Y ∀x,v [AD(x, Yxv) → BD(Ux, v)]: U turns witnesses for A into witnesses for B, and Y turns a counterexample to B into a counterexample to A. This is the "dialectical" clause.
Main theorem (I): if HA ⊢ A, then T ⊢ AD(t, y) for some terms t not containing y. For quantifier-free A, Aᴰ = A, so if T is correct, 1 = 0 is unprovable: a consistency proof for HA, and via the negative translation for PA.
Motivating the implication clause (Spector 1962). Classically, A → B, i.e. ∃x∀y AD → ∃u∀v BD, becomes ∀x∃u∀v∃y (AD → BD) through steps that use: intuitionistic logic; independence of premiss (IP′); a generalized Markov's principle (M′); and twice the axiom of choice (AC). Hence the interpretation validates exactly AC, IP′ and M′ beyond HA:
- IP′ demands a witness chosen independently of the proof of the premise, which the proof interpretation does not require.
- M′ generalizes Markov's principle (accepted by the Russian constructivists for primitive recursive C).
- Troelstra's caution: Gödel (note h) called his interpretation more constructive because it validates Markov's schema, but Markov fails in coherent intuitionistic theories such as lawless sequences, which Gödel himself (note c) thought close to finitistic.
Two delicate points in the proof: induction needs a generalized induction rule (derivable in T, note i1); and axioms like A → A ∧ A need characteristic terms for prime formulas, i.e. definition by cases. Gödel told Bernays (1970) that what is needed is "the decidability of intensional equations between functions"; for arithmetic only numerical equations are needed, so the higher-type equality issue was, in Kreisel's words, a "red herring".
The no-counterexample interpretation. If PA ⊢ A and A′ is a prenex form, the negative translation and (I) give terms that refute every attempted counterexample: Kreisel's interpretation (1951–52), a generalization of Herbrand's theorem to arithmetic. Gödel already knew in the early 1940s that Herbrand's proof needed correction.
Extensions to higher-type arithmetic
| System | Soundness of D | Note |
|---|---|---|
| HAω₀ (quantified T₀), I-HAω (with equality functionals), WE-HAω (weakly extensional) | Holds: H ⊢ A implies qf-H ⊢ AD(t, y) | Plus AC, IP′, M′ characterize D (Kreisel 1959, Yasugi 1963) |
| HAω (intensional, no decidable equality) | Fails (Howard) | Would give a weak decidability of equality |
| E-HAω (full extensionality) | Fails (Howard) | No functional realizes D of extensionality; indirect route via Luckhardt 1973 |
Three models of T
- Computable functionals (Gödel's intended model). Type 0: the numbers; type σ → τ: "a well-defined mathematical procedure" taking computable functions of type σ to type τ, a primitive notion parallel to constructive proof (note 6). Gödel struggled with the wording: "it seems to be very difficult (or impossible) to make this more precise and yet to maintain it to its full extent". Bernays noted that "intuitionistically demonstrable" made the notion depend on intuitionistic proof, so Gödel wrote "constructively evident", still dissatisfied.
- HRO, hereditarily recursive operations. Gödel numbers of partial recursive functions mapping hereditarily recursive objects of type σ to those of type τ; equality is equality of codes. The defining predicates climb the whole arithmetical hierarchy as types grow, so the "reductive gain" is modest. This is the Turing-based model of notes g and h.
- Term model NF. Closed terms in normal form; equality is literal identity (so decidable); proved via Tait's (1967) computability predicates. Note h's "reductive proofs" fit this model: an equation is reductively provable if both sides reduce to the same normal form.
Troelstra's assessment (4.4). A certain impredicativity is unavoidable: functionals of type 1 may be defined via functionals of much more complex types, just as an intuitionistic proof may pass through more complex statements. Making the model concrete (HRO, NF) does not remove it; it reappears in the correctness arguments. Gödel eliminated the logic "except for the logic hidden in the precise definition of the intended class of functionals". "There is some reductive gain though it is not clear-cut; we think it falls short of Gödel's aims." Gödel disagreed to the end: in 1974 he wrote that the route to T passes through "much narrower (and in principle decidable) concepts of 'provable' and 'implies'", so there is no circularity.
Research flowing from 1958
| Theme | Results |
|---|---|
| Extensions | Transfinite induction (Kreisel 1959); analysis via bar recursion of finite type (Spector 1962; Howard 1968, Luckhardt 1973); abstract constructive ordinals (Howard 1972); game quantifier (Friedrich 1984–85); full classical analysis and type theory with variable types (Girard 1971–72, the origin of System F and reducibility candidates); predicative analysis (Maaß 1976) |
| Normalization of T | Computability predicates (Tait 1967, Dragalin, Girard, Vogel); ordinal assignments below ε₀ (Hinata, Diller, Howard), another route to Gentzen's consistency proof; infinite terms (Tait 1965) |
| Applications | Kreisel's constructive reading of analysis; conservativity of AC, IP′, M′; closure under Markov's rule (later by Friedman–Dragalin); subsystems of arithmetic (Parsons 1970) and analysis (Feferman 1971, 1977) |
| Related interpretations | Diller–Nahm (1974, bounded quantifiers, no decidable equality needed); modified realizability (Kreisel); Stein's interpolating family; Shoenfield's variant for PA directly; all yield the same realizations (Mints, Stein) |
Since then. The Dialectica interpretation is now a working tool. Kohlenbach's proof mining (monograph 2008, and a large literature since) uses its monotone variant to extract explicit, uniform bounds from non-constructive proofs in nonlinear analysis, fixed-point theory, ergodic theory (rates of metastability, Avigad–Gerhardy–Towsner) and convex optimization, including bounds for algorithms used in machine learning. De Paiva's Dialectica categories (1989) gave the first categorical models of linear logic; Pédrot (2014) turned Dialectica into a program translation for dependent type theory; and System T itself is the textbook core of typed functional programming (Girard's System F underlies type inference in languages such as Haskell and OCaml).
Takeaway. Gödel replaced "constructive proof" by "computable functional of finite type" and proved arithmetic consistent relative to it; the reduction's philosophical value is debatable, but its technical progeny, from bar recursion to proof mining, is immense.
A Hitherto Unutilized Extension of the Finitary Standpoint (1958) and the Spector Postscript (1962)
The Dialectica paper itself is only a few pages long. Starting from Bernays's observation that a consistency proof for number theory must go beyond Hilbert's finitism, Gödel splits the finitary attitude into a constructive element and a specifically finitistic (spatiotemporal) element, drops the second, and shows that the single abstract notion of computable function of finite type, with only explicit definition and simple recursion, suffices to prove the consistency of arithmetic. The proposal replaces the abstract notions previously used for this purpose, intuitionistic logic and the constructive theory of ordinals, by a notion closer to computation: functions of higher type built by substitution and primitive recursion.
Why finitism must be extended
- Bernays's point: since consistency cannot be proved by means weaker than the system's own, a proof for classical number theory must leave finitary mathematics, whose evidence rests on what is intuitive (Hilbert 1926). So abstract notions are required: notions "essentially of second or higher order", relating not to concrete sign combinations but to mental constructs (proofs, meaningful statements), with insights drawn from their meaning, not their combinatorial properties.
- No strict proof, but no doubt. Without a precise notion of "evident" Bernays's claim is unproved; practically it is certain, especially after Gentzen showed all recursions on ordinals below ε₀ are formalizable in number theory.
- Why ε₀ is not intuitive. Induction up to, say, ω² can be made intuitive, but for ε₀ "we can no longer survey the various structural possibilities" of descending sequences. Knowledge comes only abstractly, through the notion of accessibility, defined by our ability to give an informally understood proof that an inference is valid. (Note 3: Ackermann's formal reading of "accessible" still needs abstract notions to validate the induction.)
- Open question: is the need for abstraction merely practical (we cannot imagine complex combinatorial situations) or theoretical? If the latter, once the notions are made precise, a strict proof should exist. (Note 4: Kreisel's reflective extension of finitism, iterating abstract notions about finitary formalisms, uses abstraction in an essentially weaker form.)
Two components of the finitary attitude
- The constructive element: we may speak of mathematical objects only insofar as we can exhibit them or produce them by a construction. Kept.
- The finitistic element: the objects must be intuitive, "in the last analysis spatiotemporal arrangements of elements whose characteristics other than their identity or nonidentity are irrelevant". Dropped.
- Previous practice: adjoin parts of intuitionistic logic (whose objects are meaningful statements and proofs) or the theory of ordinals. Gödel's alternative: computable functions of finite type.
The notion of computable function of finite type
Definition
- The computable functions of type 0 are the natural numbers.
- If the notions for types t₀, t₁, …, tₖ are understood, a computable function of type (t₀, t₁, …, tₖ) is "an operation, always performable (and constructively recognizable as such)" assigning to each k-tuple of computable functions of types t₁ … tₖ one of type t₀.
- This notion is "immediately intelligible", given the lower types; letting t vary yields the notion needed.
Two remarks that carry the philosophy.
- Note 5: "One may doubt whether we have a sufficiently clear idea of the content of this notion, but not that the axioms given below hold for it." The same "apparently paradoxical" situation holds for intuitionistic proof; within limits the two notions are interchangeable as primitives. To avoid smuggling in the notion of proof, it must be "immediately apparent from the chain of definitions that the operations can be performed", as for all functions of T.
- Note 6: Turing defined computable function of the first order by machines. "But, had this notion not already been intelligible, the question whether Turing's definition is adequate would be meaningless."
The system T and the interpretation
- Axioms of T: identity (identity of functions is intensional, definitional equality), Peano's third and fourth axioms, substitution, definition by explicit terms and by simple induction on a number variable, and mathematical induction. Formally almost primitive recursive arithmetic, except that variables and constants may be of any finite type. Two-valued propositional logic on equations, no bound variables.
- Strength: T equals recursive number theory with induction up to every ordinal below ε₀.
- Interpretation: each formula F of Heyting's arithmetic gets F′ = (∃y)(z) A(y, z, x), A quantifier-free, by six rules on the logical operators.
- Heuristic for implication: "F′ implies G′" is identified with the existence of computable functions that map witnesses of the antecedent to witnesses of the consequent, and counterexamples to the consequent to counterexamples of the antecedent.
- Modesty: "we do not claim that Definitions 1–6 reproduce the meaning of the logical particles introduced by Brouwer and Heyting"; how far they can replace them needs further study.
- Main claim: if F is provable in Heyting's system Z, then T defines functions Q with A(Q(x), z, x) provable in T, checked axiom by axiom and rule by rule (using a Principia-style axiomatization of intuitionistic logic). For classical number theory the ∨ and ∃ axioms can be omitted (via the negative translation).
- Outlook: stronger systems from the same idea, with transfinite types or the kind of inference Brouwer used for the fan theorem.
The postscript to Spector (1962)
Clifford Spector (1930–1961) proved, during a year at the Institute for Advanced Study (1960–61), that classical analysis has a Dialectica-style interpretation if T is extended by bar recursion at all finite types. He died of leukemia at 30; Kreisel edited the paper and wrote all its footnotes. Gödel's postscript sets the record straight:
- The discussions with Bernays and Gödel came after the main result (§10) was established.
- Spector was then in close contact with Kreisel and wanted to give him "a good deal of credit"; a joint paper had been planned, but Spector took over the elaboration, and the published proof was his.
- Spector alone was working on an extension "in the direction of stricter constructivity".
| Theory | Interpreted in | Ordinal / strength |
|---|---|---|
| HA, PA (Gödel 1958) | T: primitive recursion in all finite types | ε₀ |
| HA + transfinite induction (Kreisel 1959) | T extended accordingly | larger recursive ordinals |
| Classical analysis, Z₂ (Spector 1962) | T + bar recursion of finite type | full second-order arithmetic |
| Abstract constructive ordinals (Howard 1972) | T + ordinal recursion | Bachmann–Howard ordinal |
| Full classical type theory (Girard 1971–72) | System F / Fω | higher-order arithmetic |
Critical lens.
- "Immediately intelligible" bears the weight. Gödel concedes we may lack a clear idea of the notion; Troelstra's guide shows that making it precise reintroduces impredicativity in the correctness proof.
- Bar recursion is far from finitary: Spector's extension trades the evidence of T for a principle justified by bar induction, a highly abstract intuitionistic principle.
- The gain is still substantial: the logical operators disappear; what remains is a calculus of terms, which is exactly why the method became central to program extraction.
Since then. Bar recursion became a computational workhorse: Berardi, Bezem and Coquand (1998) and Berger–Oliva (modified bar recursion, 2005) realize classical countable and dependent choice; Escardó and Oliva (2010s) recast it as computing optimal strategies in sequential games (selection functions), giving an unexpected reading of Spector's construction. Oliva and others unified Dialectica, modified realizability and Diller–Nahm in parametrized functional interpretations; and computer formalizations of Dialectica (e.g. In Coq and Agda) are used in certified program extraction.
Takeaway. Gödel showed that the abstraction needed beyond finitism can be confined to one notion, the computable functional of finite type, and that its simplest principles already prove arithmetic consistent; Spector's bar recursion carried the method to analysis.
What Is Cantor's Continuum Problem? Revised Edition, Supplement and Postscript (1964)
For Benacerraf and Putnam's Philosophy of Mathematics Gödel revised 1947 with over a hundred changes, added a supplement answering the formalist challenge that an undecidable CH becomes meaningless, and appended a postscript on Cohen's independence proof, revised in 1966. The body repeats the 1947 argument in sharper form; the supplement contains Gödel's most famous statement of mathematical intuition as a kind of perception. Its thesis: set theory differs from geometry both mathematically (asymmetric, fruitful extensions) and epistemologically (intuition of sets is perception-like and needs no physical interpretation), so CH keeps a definite meaning even if independent.
What changed in the main text
| Topic | 1947 | 1964 (with 1966 revisions) |
|---|---|---|
| Cardinal notation | "Natural" representation | "Systematic" representation |
| AC (note 2) | As well-founded as the other axioms "in the present state of knowledge" | Well-founded "from almost every possible point of view"; from any model of the other axioms one can define a model of AC; evident for the "pure" concept of set |
| Paradoxes | Serious, "but not for Cantor's set theory" | Serious "not for mathematics, however, but rather for logic and epistemology" |
| Who may accept set theory | Those not limited to constructions or intuition | "Someone who considers mathematical objects to exist independently of our constructions and of our having an intuition of them individually" |
| "Set of" (note 14) | Paraphrases only | A multitude "exists in itself no matter whether we can define it in a finite number of words (so that random sets are not excluded)" |
| Categories (note 12) | Absent | Category theory, by self-applicability, transcends the iterative concept; nothing seems lost if levels are distinguished; otherwise the paradoxes would become a mathematical problem |
| Large cardinals (note 20) | Inaccessibles, Mahlo | Keisler–Tarski axioms "of an entirely new kind"; Scott 1961: one implies non-constructible sets; supported by analogy with Stone's representation theorem; Mahlo cardinals from Lévy's (1960) reflection principle and Bernays (1961) |
| Opposite of V = L (note 23) | "Directly opposite" axiom | A maximum property "similar to Hilbert's completeness axiom in geometry" |
| Ordinal definability | Notes 20, 26 | Omitted entirely |
| Inaccessibility for finite numbers | 0 and 2 strongly inaccessible | New definition gives 0, 1, 2 inaccessible, so the two notions differ for finite numbers, casting doubt on their equivalence (implied by GCH) for infinite ones |
The supplement: new results
- Hajnal (1956): if 2ℵ₀ ≠ ℵ₂ were provable, so would be 2ℵ₀ = ℵ₁; this "could greatly facilitate" a proof of CH, "which, however, probably is not the case".
- Sierpiński (1956): CH is equivalent to the plane being a union of countably many generalized curves (graphs y = f(x) in some coordinate system); if 2ℵ₀ is not inaccessible, the plane is a union of fewer than continuum many. A converse would lend plausibility to 2ℵ₀ = the least inaccessible > ℵ₀, Gödel's 1964 favourite. But caution: this appearance, like Peano curves, stems from geometric intuition of curves applied to non-curves. (1966: "this warning has since been vindicated" by Roy O. Davies (1963).)
- Kuratowski (1948): a strengthening of CH, consistent by the L proof, with various consequences.
Set theory is not like geometry
Errera's analogy versus Gödel's two asymmetries
- Errera (1952): an undecidable CH loses its truth value, as the parallel postulate did once non-Euclidean geometry was shown consistent.
- Mathematical asymmetry. For "there is an inaccessible": the negation has a model definable in the original system; the assertion does not, so it extends the system in a much stronger sense, and it implies new theorems about integers, verifiable by computation case by case. Only the assertion is fruitful; the negation is "sterile outside its own very limited domain". GCH, too, is sterile for number theory and true in an internal model; some other value of 2ℵα might not be. The parallel postulate and its negation are both extensions in the weak sense. (Note 39: the same asymmetry occurs at the lowest levels of set theory.)
- Epistemological asymmetry. A question loses meaning by undecidability only if the axioms are a hypothetico-deductive system with undetermined primitives. Even in geometry, the fifth postulate keeps meaning when the terms refer to rigid bodies and light rays; the decision is then physical. Set-theoretic objects "clearly do not belong to the physical world", and their link with experience is loose.
Mathematical intuition
"Despite their remoteness from sense experience, we do have something like a perception also of the objects of set theory, as is seen from the fact that the axioms force themselves upon us as being true. I don't see any reason why we should have less confidence in this kind of perception, i.e., in mathematical intuition, than in sense perception." Gödel 1964, p. 271
The epistemology in five claims
- Paradoxes are illusions of the senses' kind: "hardly any more troublesome for mathematics than deceptions of the senses are for physics".
- Intuition is not immediate knowledge. As in physics, we form ideas of the objects "on the basis of something else which is immediately given", not primarily sensations.
- Something besides sensations is given even in empirical thought: our idea of an object itself is qualitatively different from sensations, and "by our thinking we cannot create any qualitatively new elements". The mathematical given is "closely related to the abstract elements contained in our empirical ideas". (Note 40: the concept of set and Kant's categories share the function of synthesis, generating unities from manifolds.)
- Not subjective, against Kant: these data "may represent an aspect of objective reality", present in us through "another kind of relationship between ourselves and reality".
- Realism is not even needed here: the "mere psychological fact" of an intuition clear enough to produce the axioms and an open series of extensions suffices to give CH a truth value. What justifies this criterion most is that intuition is needed even for finitary number theory (Goldbach-type statements), since every axiom system leaves infinitely many such propositions undecided.
Fruitfulness, again. Besides intuition there is a "probable" criterion: fruitfulness in mathematics "and, one may add, possibly also in physics". It "may become decisive in the future", but cannot yet be applied to large-cardinal axioms, since little is known of their consequences elsewhere; the simplest case would be number-theoretic consequences verifiable by computation.
The postscript (revised September 1966)
- Cohen settled CH negatively for von Neumann–Bernays set theory with choice, "shortly after the completion of the manuscript".
- For every ℵτ "defined by the usual devices and not excluded by König's theorem", 2ℵ₀ = ℵτ is consistent and an extension in the weak sense (no new number-theoretic theorems). Whether this holds for every definable ℵτ under a precise notion of "standard definition" is open.
- Cohen's work "no doubt is the greatest advance in the foundations of set theory since its axiomatization".
- The new large-cardinal axioms of note 20, as far as precisely formulated, are not sufficient to decide CH (Lévy–Solovay).
Critical lens.
- Access problem. Benacerraf (1973), in the very anthology for which the supplement was written, argued that a causal-style epistemology leaves no way to know abstract objects; Gödel's "something else immediately given" names the gap rather than closing it. Maddy (1990) tried a naturalized version (perceiving small sets), later abandoned for a methodological view.
- "Force themselves upon us" fits the ZF axioms; it fits large cardinals and CH far less, which is why Gödel shifts to fruitfulness for them.
- The asymmetry argument holds up: large-cardinal assertions do have arithmetical consequences (consistency statements, and later Harvey Friedman's natural combinatorial statements), while CH provably has none (Platek, Solovay).
Since then. The supplement is the founding text of mathematical Platonism in analytic philosophy. Its two criteria map onto today's debate on axioms: intrinsic justification (Gödel's "forcing themselves upon us", reflection principles) and extrinsic justification (fruitfulness, Maddy's Defending the Axioms, 2011). Koellner and Woodin argue that the theory of L(R) under large cardinals is "Ω-complete" and generically absolute, vindicating Gödel's programme for the projective level, while CH lies beyond any such argument; Hamkins's multiverse (2012) rejects the premise of a single universe, and Väänänen and others pursue the second-order "internal categoricity" route reminiscent of Zermelo. Gödel's favoured value moved over time: least weakly inaccessible (1964), then ℵ₂ (1970), the value now favoured by forcing-axiom advocates.
Takeaway. In 1964 Gödel kept every forecast of 1947, added the asymmetry argument and the theory of mathematical intuition, and greeted Cohen's proof as confirmation that CH must be decided, if at all, by new axioms grounded in intuition or success.
On an Extension of Finitary Mathematics Which Has Not Yet Been Used (1972)
The English revision of the Dialectica paper, set in type in 1970 but never released, keeps the 1958 argument and adds fourteen lettered notes (a–n) in which the late Gödel sharpens the philosophy: what Hilbert's "Anschauung" really restricts, why accessibility proofs only look concrete, how far Kreisel's idealized finitism reaches, and how a narrow notion of "reductive proof" can replace Heyting's general concept of proof. The new claim of 1972 is that his interpretation of intuitionistic logic "in no way presupposes Heyting's" and is "constructive and evident in a higher degree", because it eliminates quantification over "any proof".
What the revision adds
- Note a (provenance): not a literal translation of 1958; Boron's translation revised, many passages rephrased, "the meaning has nowhere been substantially changed". Thanks to Dana Scott for supervising the typing "while I was ill" and to Bernays for reading proofs.
- A tighter abstract: the only construction principles needed are primitive recursion on a number variable and explicit definition by a term built from variables and earlier functions, "beginning with the function +1".
- Abstract concepts are those whose content is not properties of concrete objects but "thought structures or thought contents (e.g., proofs, meaningful propositions)", known by reflecting on meanings. Example (note e): "p implies q" as "from a convincing proof of p a convincing proof of q can be obtained".
Finitism, intuition and the ladder of evidence
Note b: Hilbert's restriction is not in the word "finitary". "Concrete intuition" translates Anschauung: substantially Kant's space-time intuition, confined to finitely many discrete objects. This makes finitism "surprisingly weak", excluding things "just as incontrovertibly evident to everybody as finitary number theory": every primitive recursive definition is finitary, yet the general principle of primitive recursive definition is not, because it contains the abstract concept of function. "There is nothing in the term 'finitary' which would suggest a restriction to concrete knowledge. Only Hilbert's special interpretation of it introduces this restriction."
- Why ε₀ needs abstraction. Recursion up to ε₀ would be finitarily provable if the consistency of number theory were. But it cannot be made immediately evident (as for ω²), and stepwise transitions such as α → α² are so small that they would have to be repeated ε₀ times; the same holds for Hilbert's ω-rule insofar as it is concretely evident.
- Note c: accessibility deceives. Gentzen, Lorenzen, Schütte, Kreisel and Takeuti used accessibility (with intuitionistic logic). It creates "the deceptive impression of being based on a concrete intuition of certain infinite procedures, such as 'counting beyond ω'". Such intuition exists but "does not reach very far … certainly no farther than finitism"; fruitful use always needs abstract conceptions, e.g. Gentzen's "insights about infinitely many possible insights". Free choice sequences come closer to Hilbert's finitism.
- Note d: bar induction. An abstract principle about schemes of ramification, proved by Brouwer and Heyting only for integer elements. Spector showed the abstract principle implies the consistency of classical analysis; Brouwer's yields only a subsystem. "No satisfactory constructivistic proof is known" for either. "Perhaps the most promising extension of T" is by higher-type computable functions of constructive ordinals.
- Notes 4 and f: Kreisel's idealized finitism. Reflecting finitarily on finitary formalisms and iterating along previously constructed ordinals reaches exactly ε₀ (Kreisel 1965, Theorem 3.43). Kreisel concluded that ε₀ is the limit of idealized concrete intuition; Gödel: the arguments "would have to be elaborated further in order to be fully convincing", and counting any admissible sequence of steps as one step extends the hierarchy far beyond ε₀, making accessibility constructive "in a much stricter sense" by resolving the impredicative concept of intuitionistic proof into levels of formal proofs.
Computable functionals, Turing machines and reductive proof
The defining clause, 1972 wording. A computable function of type (t₀, t₁, …, tₖ) is "a well-defined mathematical procedure which can be applied to any k-tuple of computable functions of types t₁ … tₖ and yields a computable function of type t₀ as result; and for which, moreover, this general fact is constructively evident". "Well-defined mathematical procedure" is "to be accepted as having a clear meaning without any further explanation".
- Note 5 (Turing): Turing's definition "most certainly was not superfluous", but if "mechanically computable" had lacked a clear prior meaning, asking whether the definition is adequate would be meaningless, "while it undoubtedly has an affirmative answer".
- Note 6: for epistemological significance, the concept of computable function and the insight that T's axioms hold must not implicitly involve intuitionistic logic or Heyting's concept of proof.
- Note g: Turing's functions (higher-type arguments identified with code numbers of machines) also satisfy T; this is the HRO model of Troelstra's guide.
Note h: reductive proof.
- A reductive proof is one where, up to trivial supplements, "the chain of definitions of the concepts occurring in the theorem together with certain axioms about the primitive terms forms by itself a proof, i.e., an unbroken chain of immediate evidences". A definition counts as a theorem asserting existence and uniqueness, including the type of the function defined.
- A narrower notion "computable of type t" replaces "constructively evident or demonstrable" by "reductively provable", which is decidable, so implications can be read as truth functions.
- In the resulting system T′, only reductive proof occurs; proofs are uniquely determined by theorems, so quantification over "any proof" disappears. (Not all proofs in T′ are reductive; the axioms and individual rule instances are.)
Consequence: the interpretation "in no way presupposes Heyting's" and is "constructive and evident in a higher degree", since "it is exactly the elimination of such vast generalities as 'any proof' which makes for greater evidence". It also makes Markov's principle trivially provable for decidable properties.
The system T made precise (notes i–n)
| Note | Content |
|---|---|
| 7 | Equality of functions is intensional: same computation procedure, i.e. identity; always decidable, justifying two-valued logic |
| i | Primitives: 0, +1, =, variables and defined constants of all finite types, application, connectives; induction with parameters of arbitrary type; a principle of disjunctive definition (derivable via recursively defined disjunctive functions); avoiding extensional equality, "an incomparably more intricate concept than logical identity"; the propositional calculus can be dispensed with; Peano axiom group (3) is superfluous |
| j | Heyting arithmetic H: only number variables, primitive recursive functions, induction as a rule; no Gentzen sequents, no ι-operator |
| k | Letters in the definitions denote symbol combinations; brackets denote substitution (Subst) |
| l | The complex clause for F ∨ G secures decidability of ∨ and the rule from p ⊃ r and q ⊃ r to p ∨ q ⊃ r; for quantifier-free F, G, F′ = F |
| m | Ex falso (axiom 7) can be omitted for interpreting classical arithmetic (Johansson 1936, minimal logic) |
| n | Verifications are trivial for most axioms; induction at n is n-fold substitution and modus ponens; the deduction theorem holds; Spector's extension of T by intuitionistic logic with higher-type quantifiers is interpreted in the same way |
1958 versus 1972
- Emphasis: 1958 offers a technical-foundational result; 1972 argues for its epistemic superiority over Heyting's logic.
- Key term: "always performable (and constructively recognizable as such)" becomes "constructively evident", after Bernays objected to "intuitionistically demonstrable".
- New ideas: Anschauung critique (b), accessibility as deceptive (c), Kreisel's ε₀ limit questioned (f), Turing model (g), reductive proof (h).
- Unchanged: the system T, the translation, and the consistency result.
Critical lens. Troelstra judged the notes to lack Gödel's earlier "sureness of touch". Note h claims decidability of "reductively provable" and avoidance of general proof, but the correctness of T′ still requires a proof that every term normalizes (Tait-style), which uses induction over complex predicates: the impredicativity Gödel hoped to banish reappears there. Tait himself later argued that finitism coincides with PRA, a precise answer to the question Gödel left "undecided off hand", and Kreisel's ε₀ analysis remains contested.
Since then. Gödel's note h anticipates proof normalization as computation, the Curry–Howard correspondence and "proofs as programs": a reductive proof is, in modern terms, a computation to normal form. The debate on the limits of finitism continues: Tait (1981) identifies finitism with PRA; Kreisel's ε₀ thesis has defenders and critics; and proof theory now calibrates exactly which abstract principles (bar induction, inductive definitions, reflection) each consistency proof needs, through ordinal analysis, now pushing toward Π¹₂-CA₀ (Rathjen, Arai).
Takeaway. The 1972 notes turn a technical consistency proof into a thesis about evidence: finitism's weakness comes from Hilbert's narrow reading of intuition, and the right extension is a narrow, decidable notion of proof over computable functionals.
Some Remarks on the Undecidability Results (1972a)
Three short remarks, found appended to the galley proofs of 1972, were probably meant as Gödel's last word on the meaning of his incompleteness theorems. Remark 1 states "the best and most general version" of the second theorem; Remark 2 argues that deciding ever harder number-theoretic problems needs ever more complicated axioms, which the axioms of infinity may supply; Remark 3 charges Turing with a "philosophical error": ignoring that the mind "is not static, but constantly developing". The introductory notes are by Feferman (Remark 1), Feferman and Solovay (Remark 2) and Webb (Remark 3). Together the remarks express Gödel's settled view that incompleteness limits formalism, not reason, and that the open question is whether human understanding of abstract concepts can outrun every machine.
Remark 1: outer consistency
Gödel's statement. If number theory Z is recursively one-to-one translatable into S with demonstrability preserved, then the consistency of S (no proposition and its negation both provable), "even of very strong systems", may be provable in S, even in primitive recursive arithmetic. What is unprovable in S is that the rules of the equational calculus, applied to equations between primitive recursive terms provable in S, "yield only correct numerical equations", provided S has this property. This "outer consistency" (for usual systems trivially equivalent to consistency) is exactly what Hilbert's programme needs to justify transfinite axioms. It holds for systems much weaker than Z. (First printed in 1967 as a note to 1932b: "perhaps it has not received sufficient notice".)
Feferman's commentary.
- Why consistency can be self-provable. Whether S ⊢ Con depends on how S is presented. Takeuti (1955): a cut-free Gentzen system proves a weak form of its own consistency (non-provability of 0 = 1). Feferman (1960): a different description of the axiom set (non-effective on its face). Kreisel (1965): a different description of proofs. (Jeroslow 1975: Feferman's trick fits natural "experimental logics".)
- Derivability conditions. Hilbert–Bernays (1939, following a plan Gödel outlined to Bernays on a transatlantic voyage in 1935) proved the second theorem from conditions D1–D3 on ProvS. Each self-proving example violates one: Jeroslow (1973) showed D1 is dispensable; D3 (formalized adequacy for primitive recursive arithmetic) is the critical one, and all three examples fail it.
- Gödel's version reconstructed: with a "literal Gödel sentence" G and primitive recursive term t (Jeroslow 1973; Kreisel–Takeuti 1974), one proves: if S contains PRA and is outer consistent, then an instance of the Π⁰₁ reflection principle (outer consistency) is unprovable in S, avoiding D1 and D3 altogether.
- Assessment: "the best and most general version" fairly, with respect to Hilbert's programme. But Gödel ignores generalizations to non-constructive systems (Rosser 1937, Mostowski 1952) and reflection principles (Feferman 1962, Kreisel–Lévy 1968); systems for real mathematics need modus ponens/cut, so the cut-free case is marginal. More natural and general is Löb's (1955) abstract derivability conditions, set in modal context by Solovay (1976), plus a theory of canonical presentations (Feferman 1982).
Remark 2: complexity of axioms and problems
Gödel's argument
- Theorem: to solve all problems of "Goldbach type" (Π⁰₁: ∀x R(x), R decidable) of complication k, one needs axioms of complication > k, "up to a minor correction" (complication = number of symbols, including those in definitions).
- All present mathematics follows from "a handful of rather simple axioms". So to solve problems statable in a few pages, we must add "a great number of new ones or axioms of great complication".
- Doubt: can evident axioms exist in such numbers or complexity? If not, there are "mathematical yes or no questions undecidable for the human mind".
- Answer: there are "unexplored series of axioms which are analytic in the sense that they only explicate the content of the concepts occurring in them", e.g. axioms of infinity, which "only explicate the content of the general concept of set".
- "Ever more (and ever more complicated) axioms appear during the development of mathematics. For, in order only to understand the axioms of infinity, one must first have developed set theory to a considerable extent."
Feferman and Solovay's commentary.
- What can be proved. In a language with m basic symbols, they prove a version: there are constants c₁, c₂ such that for k > c₂ no finite consistent extension S of a base system with d(S) < (k − c₂)/c₁ proves all true Π⁰₁ statements of complexity < k, with c₁ = ⌈log₂ m⌉ + 1 (about 4 for usual languages). The literal reading (c₁ = 1) they could not establish. Every Π⁰₁ statement is equivalent to a Diophantine one (Matiyasevich; at most 9 unknowns).
- Against the premise. Large-cardinal axioms have not grown enormously in complexity: "new and stronger axioms simply displace old ones", and a few pages state the strongest. Each new axiom does "solve" the Gödel sentence of the old system (it proves a model, hence consistency). But they are not accepted by mathematicians generally (Cohen 1971 opposed; Reinhardt 1974 and Kanamori–Magidor 1978 favoured), and none settles CH.
- Against the conclusion. The two authors (who "disagree about the foundational status" of new axioms) agree, contrary to Gödel, that simple yes-or-no problems will probably never be settled: e.g. Is the last of the first 22100 binary digits of π − 3 a 0? It is beyond feasible computation and offers "absolutely no conceptual foothold".
- Relevance to practice: what matters is the complexity of proofs, not axioms; hard problems may have short proofs once "the right key is found", and complexity is "a shifting matter" as concepts become everyday tools.
Remark 3: Turing's "philosophical error"
"What Turing disregards completely is the fact that mind, in its use, is not static, but constantly developing, i.e., that we understand abstract terms more and more precisely as we go on using them, and that more and more abstract terms enter the sphere of our understanding." Gödel 1972a, Remark 3
- The argument. Turing's 1937 argument that "mental procedures cannot go beyond mechanical procedures" is inconclusive. There may be systematic methods of actualizing the mind's development; though at each stage the number and precision of abstract terms are finite, both, "and, therefore, also Turing's number of distinguishable states of mind", may converge toward infinity during the procedure.
- Examples: forming stronger axioms of infinity, a process "far from being sufficiently understood to form a well-defined procedure"; and systematically constructing, via distinguished sequences αₙ → α, all recursive ordinals of the second number class.
- Admission: a well-defined procedure that could actually be carried out and yield a non-recursive function "would require a substantial advance in our understanding of the basic concepts of mathematics".
- Placement: a footnote to "mathematics" in Gödel's 1964 postscript to 1934, which says the undecidability results "do not establish any bounds for the powers of human reason, but rather for the potentialities of pure formalism in mathematics". A version also appears in Wang 1974.
Webb on Gödel, Church's thesis and Turing
1931: Herbrand admits arbitrary recursion equations, computable "intuitionistically", and argues Gödel's theorem fails for his arithmetic since the diagonal function cannot be numbered; he defines "recursive" functions in a letter to Gödel.
1934: Gödel rejects Church's λ-definability proposal as "thoroughly unsatisfactory", defines general recursive functions (Herbrand's equations plus two rules), and calls the identification with finite computability only a "heuristic principle", his thesis (GT): finitely computable = definable by "recursions of the most general kind".
1936: Kleene's normal form and μ-recursion results; Webb thinks these should have convinced Gödel, but there is no evidence they did.
1936–37: Turing's machines: Gödel is convinced, perhaps (Feferman's conjecture) by their deterministic character, which makes consistency of the definition obvious, unlike the hard Church–Rosser theorem for λ-calculus.
1946: the "kind of miracle": recursiveness is closed under diagonalization.
1964–65: Turing's work gives "a precise and unquestionably adequate definition of the general concept of formal system"; general recursiveness fits (GT) only if "finite procedure" means "mechanical procedure".
1972: Remark 3 on Turing's error.
| Turing's argument (1937, §9) | Content | Gödel's attitude (per Webb, Wang) |
|---|---|---|
| Type I | A human computer has finitely many states of mind; human memory is "necessarily limited" | Rejected as the "philosophical error" |
| Type II | The whole predicate calculus can be simulated by a machine | Accepted |
| Type III | Replace states of mind by a physical note of instructions; each stage fully determined | Accepted (Feferman's suggestion) |
| Wang 1974 | Turing's argument valid given (1) no mind separate from matter and (2) the brain works like a digital computer, or (2′) physical laws have finite precision | Accepts (2), (2′); rejects (1) as "a prejudice of our time", perhaps refutable by showing "there aren't enough nerve cells" for the mind's operations |
Webb's critique of Gödel's objection.
- The infinite-states fallacy. "The mind can think of any number, so it has infinitely many states" is false: thinking of a number is a process through finitely many states with bounded records, exactly Turing's analysis. Gödel's argument differs only by its appeal to abstract terms whose precise understanding creates new states.
- Turing anticipated complexity. Turing himself said that more complicated states "can be avoided by writing more symbols on the tape", and the universal machine concentrates "the complexity of the machine to be imitated … in the tape". The real issue is the complexity of states, not their number.
- Gandy (1980): replace finiteness by local causation; Gödel's non-mechanical intelligence would see states "as a Gestalt" and make global determinations unreachable locally.
- Kreisel (1972): a second Turing "error" is assuming that relations between codes of mental states are mechanical; but Kreisel's examples of non-mechanical rules turned out Turing-computable.
- Turing's analysis is about people: "computer" meant a person calculating (Hodges); Gödel's picture of an analysis of mechanical procedure "shorn of human aspect" is found nowhere in Turing. The deep contribution is the universal machine, trading bounded internal memory for unbounded external memory.
- Conclusion: Gödel saw the difficulty of keeping his theorems general (via Turing) while denying that humanly effective processes are mechanizable, a difficulty measured by "how far into the future of human development he felt he had to look for a way out".
Since then. Remark 3 sits beside Gödel's disjunction from his 1951 Gibbs lecture (published in Collected Works III, 1995): either the mind infinitely surpasses any machine, or there are absolutely undecidable Diophantine problems. Anti-mechanist arguments by Lucas (1961) and Penrose (1989, 1994) go further than Gödel ever did and are widely judged unsound (Feferman 1995, Shapiro); Koellner (2016–18) showed that, in natural formal frameworks for "knowable truth", Gödel's disjunction is provable but each disjunct is independent. Modern AI systems (LLM-based provers, AlphaProof's 2024 IMO results) and growing formal libraries (Lean's mathlib) bring the question back in practical form, though nothing about them escapes Turing's analysis. On Remark 2, Kolmogorov–Chaitin complexity gives sharp versions (Chaitin's incompleteness theorem: no system proves strings much more complex than itself random), and Friedman's concrete incompleteness shows natural finite combinatorial statements that need large cardinals.
Takeaway. Gödel's final remarks sharpen the second theorem for Hilbert's programme, tie undecidability to the complexity of axioms, and leave open, against Turing, whether a mind that keeps understanding new abstract concepts could decide what no fixed machine can.
Remark on Non-Standard Analysis (1974)
Gödel's last publication is a few sentences spoken after Abraham Robinson's talk at the Institute for Advanced Study in March 1973, printed with his permission in the second edition of Robinson's Non-standard Analysis (1974). Gödel predicts that non-standard analysis, "in some version or other, will be the analysis of the future", calls the 300-year neglect of infinitesimals "a great oddity", and links it to another oddity, the unsolved Fermat problem. Jens Erik Fenstad's note places the remark between Robinson's formalism and Gödel's Platonism. For Gödel, infinitesimals are simply "the next quite natural step" after the reals in the growth of the number system, as real as the irrationals, and their late arrival shows how far concrete mathematics lagged behind abstract.
Fenstad's note: how infinitesimals returned
- Banished. Fraenkel (1928): "In this test [founding the calculus], however, the infinitely small has completely failed." This was the canonical view.
- Returned by logic. Robinson (autumn 1960; first reported at a Princeton seminar, November 1960) saw that mathematical logic provides a framework for calculus with infinitely small and large numbers, using non-standard models first built by Skolem (1933–34). Skolem's aim was negative (limits of axiomatics); Robinson turned it positive.
- Two principles make it rigorous. Transfer: the non-standard extension is an elementary extension, so it has the same "algebra" (first-order properties) as the reals. Concurrence (saturation): every internal family of sets with the finite intersection property has a common point, a passage from "∀∃" (local) to "∃∀" (uniform) behind many compactness and uniform-boundedness arguments.
"There are good reasons to believe that non-standard analysis, in some version or other, will be the analysis of the future." Gödel 1974
Gödel's remark
The argument in four steps
- Simplification. Non-standard analysis "frequently simplifies substantially the proofs, not only of elementary theorems, but also of deep results", e.g. The existence of invariant subspaces for compact operators (Bernstein–Robinson 1966, for polynomially compact operators), and "in an even higher degree in other cases".
- Not a fad. This should prevent the misreading of it as "some kind of extravagance or fad of mathematical logicians. Nothing could be farther from the truth."
- Two reasons for the future. Simplification facilitates discovery; and, "even more convincing", arithmetic grows by enlarging the number system (integers, rationals and negatives, irrationals), yet "the next quite natural step after the reals, namely the introduction of infinitesimals, has simply been omitted".
- Two oddities. In coming centuries it will seem "a great oddity" that the first exact theory of infinitesimals came 300 years after the calculus; this may relate to the fact that problems like Fermat's, "written down in ten symbols of elementary arithmetic", are still unsolved after 300 years. "Perhaps the omission … is largely responsible for the fact that, compared to the enormous development of abstract mathematics, the solution of concrete numerical problems was left far behind."
Robinson versus Gödel on what the new numbers are
Formalist and Platonist
- Shared ground (Robinson 1966): infinitesimals "are neither more nor less real than, for example, the standard irrational numbers"; both arise axiomatically or by infinitary processes, and since all measurements are integers or rationals, nothing forces an Archimedean system.
- Robinson's formalism: "From a formalist point of view we may look at our theory syntactically and may consider that what we have done is to introduce new deductive procedures rather than new mathematical entities."
- Gödel's Platonism: no ontological difference between integers, rationals, irrationals and infinitesimals; by "quite natural steps" we come to know what already exists.
Fenstad's comments on four phrases
| Gödel's phrase | Fenstad's comment |
|---|---|
| "The next quite natural step" | The definite article suggests a unique extension; Robinson's hyperreals are not unique (uniqueness needs arbitrary restrictions such as ℵ₁-saturation and size ℵ₁). Non-uniqueness may be "an opportunity to be exploited" |
| "A great oddity in the history of mathematics" | Success presupposes elementary extension and concurrence, insights of logic (Skolem; Maltsev 1936, 1941, first compactness arguments). The reals were tamed by Weierstrass, Dedekind, Cantor; infinitesimals had to "wait their time" |
| "Another oddity" (Fermat) | Problematic: Faltings's (1983) partial success on Fermat used enormous abstract mathematics. Perhaps Gödel hinted at incompleteness and new axioms; but non-standard analysis, presented axiomatically, is a conservative extension (Kreisel 1969) |
| "The analysis of the future" | Support: if the geometric line carries richer point sets, infinitesimals become essential for describing phenomena on many scales, including singular ones (stochastic analysis, mathematical physics: Cutland 1983, Albeverio et al. 1986) |
Critical lens.
- The Fermat link failed as prophecy. Wiles (1995), with Taylor, proved Fermat's Last Theorem through the most abstract modern machinery (elliptic curves, modular forms, Galois representations), the opposite of what Gödel's remark suggests; no infinitesimals were needed.
- Conservativity cuts both ways. Since non-standard methods prove no new standard theorems in their usual axiomatizations, their value is heuristic and economical, not foundational strength.
- Adoption remains limited. Non-standard analysis has not become the analysis; critics (e.g. Connes, on the non-constructive ultrafilter) object to its reliance on non-definable objects.
Since then. Gödel's "in some version or other" proved apt. Nelson's Internal Set Theory (1977) and Hrbacek's relative set theories axiomatize infinitesimals inside set theory; Keisler's Elementary Calculus (1976) teaches calculus with them; smooth infinitesimal analysis (Lawvere, Kock) uses nilpotent infinitesimals in topos theory. The deepest impact is through ultraproducts: Tao, Breuillard–Green–Tao (2012) on approximate groups, and Hrushovski use non-standard limits to turn "hard" quantitative analysis into "soft" qualitative arguments and back, with proof mining extracting the quantitative bounds afterwards, a meeting point of this chapter and Gödel's Dialectica work.
Takeaway. Gödel's final published words endorse infinitesimals as the natural completion of the number system and as a tool that simplifies deep proofs; history vindicated the "some version or other" more than the claim that their absence held back concrete mathematics.
Master Takeaways
Thirty-six years of Gödel's later work, read with the notes of the logicians, physicists and philosophers who knew it best, reduce to a few exact results and one persistent conviction. The results show what the axioms permit (AC, GCH, rotating worlds, a consistent arithmetic); the conviction is that what is true outruns what any fixed system proves, so progress comes from new axioms and new abstract concepts, chosen by intuition or by their fruits.
Master takeaways
- AC and GCH cannot be refuted. The constructible universe L, built from definable subsets, satisfies ZF + AC + GCH, so if ZF is consistent so is ZFC + GCH (1938 to 1940). With Cohen (1963) neither CH nor AC is decided by ZF.
- Independence is not a solution. For a realist CH is true or false; the axioms are an incomplete description of a determinate universe, so independence only shows that new axioms are needed (1947, 1964).
- New axioms have two kinds of warrant. Intrinsic: the iterative concept of set demands further iterations (axioms of infinity). Extrinsic: fruitfulness and verifiable consequences, "as any well-established physical theory". This is still the framework of the debate.
- Classes and concepts are as real as bodies. Gödel's realism (1944) covers sets and concepts; the strong vicious-circle principle holds only for objects we construct, so impredicative mathematics is legitimate.
- Einstein's equations permit time travel. The Gödel universe (1949) rotates, has no cosmic time and contains closed timelike curves; general relativity does not enforce Mach's principle or a global causal order.
- Arithmetic is consistent relative to computable functionals. The Dialectica translation (1958) reduces HA, and via the negative translation PA, to the quantifier-free system T of primitive recursive functionals of finite type, the seed of proof mining and functional interpretations.
- Condensation is the heart of L. Every elementary substructure of an L-level collapses to an L-level; this, not the eight operations, is the transferable insight (1939a), later developed into Jensen's fine structure.
- V = L is a minimality axiom. Gödel first found it a "natural completion" (1938), then judged it false: only a maximum principle, like Hilbert's completeness axiom, fits the concept of arbitrary set (1964 note 23).
- Measurable cardinals refute V = L (Scott 1961) but do not decide CH (Lévy–Solovay); no large-cardinal axiom known can settle it, though they settle the theory of projective sets (Martin–Steel, Woodin).
- HOD gives choice, not CH. Ordinal definability (1946) yields an inner model of ZFC, and V = HOD is consistent with ¬CH (McAloon 1966), as Gödel predicted.
- Computability is the only absolute epistemological notion found so far. Diagonalization does not escape it, a "kind of miracle" (1946); provability and definability stay language-relative.
- The predicative limit is Γ₀. Gödel's hint that orders can be iterated into the transfinite led, through Wang, Spector and Kreisel, to Feferman–Schütte's precise analysis of predicativity.
- Russell's no-class theory fails mathematically. Without reducibility or infinite propositions, ramified type theory cannot even secure arithmetic (the flaw in *89.16 of Principia's Appendix B; Myhill 1974).
- Collapsing ("slingshot") arguments that true sentences share one referent originate with Gödel (1944) and Church; Russell's descriptions "evade" rather than solve the problem.
- Mathematical intuition is perception-like but not immediate. We form ideas of sets from something "immediately given", as with physical objects; the paradoxes are like illusions of the senses (1964).
- CH is arithmetically sterile; large cardinals are not. Inaccessibles prove new number-theoretic theorems, CH and ¬CH prove none (Platek, Solovay): the asymmetry that separates set theory from the parallel postulate.
- Gödel's specific CH arguments failed. The thin-set "paradoxes" persuaded few; the 1970 square-axiom proofs of ℵ₂ and then CH were mistaken; yet his late guess 2ℵ₀ = ℵ₂ is what PFA and Martin's Maximum imply.
- Rotation is generic, time travel is not. Expanding, finite, rotating universes exist for every λ (∞⁸ of them); closed timelike curves need rotation near c/R; slow rotation is observable in principle, and the CMB now bounds it tightly.
- Relativity suggests change is not objective (1949a): if worlds without absolute time are lawful, objective lapse here would depend on the accident of matter. The modal step is the argument's weak point.
- Finitism is narrower than "finitary". Hilbert's restriction to concrete Anschauung makes finitism weak; the constructive element can be kept while the spatiotemporal element is dropped (1958, 1972).
- The logic eliminated returns in the functionals. Troelstra's verdict: Dialectica's reductive gain is real but "not clear-cut"; impredicativity reappears in the correctness of T.
- Bar recursion takes Dialectica to analysis (Spector 1962), now read computationally as optimal strategies in sequential games.
- Self-proved consistency depends on presentation. Cut-free systems and odd axiom descriptions can prove their own consistency; what no system proves is its outer consistency (1972a, Remark 1).
- Harder problems need richer axioms, roughly in proportion to their size (1972a, Remark 2), but large-cardinal axioms displace rather than accumulate, and some feasible-looking questions may never be decided.
- Formal limits are limits of machines, not necessarily of minds. Turing's analysis is right for mechanical procedure; whether a mind that keeps grasping new abstract concepts exceeds every machine is left open (Remark 3; Gödel's disjunction).
- Infinitesimals are a natural extension of number (1974), simplifying deep proofs; their modern life is mostly through ultraproducts and the hard/soft analysis correspondence.
Frameworks and mental models
| Name | What it says | Use it when |
|---|---|---|
| Constructible hierarchy L | Add only definable subsets at each stage | You need the smallest model consistent with the axioms |
| Absoluteness | Some notions mean the same in an inner model and in V | Transferring results between models |
| Condensation / collapse | Elementary substructures collapse to levels of the hierarchy | Counting subsets; proving GCH-type bounds |
| Iterative concept of set | Sets arise by iterating "set of" from given objects | Justifying axioms and explaining why no paradox |
| Intrinsic vs extrinsic justification | Axioms evident from concepts, or accepted for their fruits | Evaluating any new foundational principle |
| Minimality vs maximality | V = L as smallest universe; maximum principles opposite | Choosing between restrictive and generous axioms |
| Three vicious-circle principles | "Definable only", "involving", "presupposing" | Diagnosing impredicativity objections |
| Ordinal definability (HOD) | Definable from ordinals with quantifiers over V | Building choice-satisfying inner models |
| Rotation vs world time | A homogeneous universe rotates iff local simultaneity is not integrable | Testing claims about cosmic time |
| Dialectica translation | A ↦ ∃x∀y AD(x, y) with computable witnesses | Extracting programs and bounds from proofs |
| Witness and counterexample | Implication maps witnesses forward, counterexamples back | Designing contracts between components |
| Outer consistency / reflection | Numerical instances of proved equations are true | Stating what self-verification can never achieve |
| Complexity of axioms | Deciding size-k problems needs axioms of size ≈ k | Budgeting what a rule base can settle |
| Transfer + saturation | Non-standard extensions keep first-order truths and add uniformity | Passing between local and global arguments |
Critical lens on the whole volume.
- Philosophy outruns argument. Gödel's realism is defended by analogy (bodies, perception) and by its fruits (L, HOD); the epistemology of access is gestured at, never worked out, and the theory of concepts he wanted was never written.
- Several prophecies failed. CH is not refuted by any accepted axiom; the thin-set intuitions were not shared; the 1970 proofs were wrong; Fermat fell to abstract mathematics; non-standard analysis did not become standard.
- Several prophecies held. Independence of CH, insufficiency of known large cardinals, HOD and ¬CH, the fertility of functionals of finite type, the importance of rotation and causality in GR, and the enduring weight of the mind versus machine question.
- The notes are excellent but dated and partial. Written around 1985 to 1989 by close colleagues, before the Nachlass (Gibbs lecture, Kant drafts, Carnap paper, shorthand notebooks) appeared in Volumes III to V; some judgments (on motives, on what Gödel knew in 1946) are explicitly conjectural.
- Gödel's own exposition is uneven. The 1940 monograph hides its key idea; the 1952 lecture omits proofs; the 1972 notes lack his earlier sureness. The commentators repair much of this.
Who's who
| Person | Role in the volume |
|---|---|
| Kurt Gödel (1906 to 1978) | Author: L, Platonism, continuum, rotating universes, Dialectica |
| Bertrand Russell | Principia; vicious-circle principle; no-class theory; target of 1944 |
| Albert Einstein | General relativity; Gödel's walking companion; 1949a written for his volume |
| Paul Bernays | Class theory used in 1940; pointed out the need to extend finitism; Dialectica dedicatee |
| Alfred Tarski | Led the 1946 logic session; large cardinals with Keisler; passed on the 1970 paper |
| Paul Cohen | Forcing (1963): CH and AC independent; "greatest advance" since axiomatization |
| Dana Scott | Measurables refute V = L; Boolean-valued models; helped Gödel in 1970 |
| Clifford Spector | Bar recursion: Dialectica for classical analysis (1962) |
| Georg Kreisel | No-counterexample interpretation; predicativity; Spector's collaborator |
| Abraham Robinson | Non-standard analysis (1960); occasion of the 1974 remark |
| Alan Turing | Analysis of mechanical computation; target of Remark 3 |
| Robert M. Solovay | Note on L; independence results; checked the 1970 paper |
| Charles Parsons | Notes on 1944 and 1946 |
| Gregory H. Moore | Note on the continuum problem (1947, 1964) |
| Stephen Hawking | Note on the cosmological papers |
| Howard Stein | Note on relativity and idealism |
| Anne S. Troelstra | Note on Dialectica (1958, 1972) |
| Solomon Feferman | Editor-in-chief; notes on Remarks 1 and 2 |
| Judson C. Webb | Note on Remark 3, Turing and Church's thesis |
| Jens Erik Fenstad | Note on non-standard analysis |
Connect it
- No system certifies itself. Remark 1 sharpens the second theorem: a framework can be presented so that it "proves" its consistency, but never its outer consistency. For AI and model risk, validation must come from an independent layer, not from the model's own reports.
- Minimal versus maximal models. L is the smallest world the rules allow; Gödel argued the real one is maximal. Specifications, ontologies and data contracts likewise admit minimal unintended models; test against instances as well as axioms.
- Extract evidence from proofs. Dialectica and proof mining turn non-constructive arguments into explicit bounds; the same move turns qualitative compliance claims into quantitative, checkable thresholds.
- Witness and counterexample contracts. The implication clause (forward witnesses, backward counterexamples) is a precise template for interface contracts between systems and teams.
- Justify rules by fruits as well as first principles. Gödel's extrinsic criterion is how new standards and controls earn acceptance: by simplifying, unifying and predicting what was already known.
- AI provers inherit every limit here. LLM-based provers and Lean libraries work inside fixed formal systems; Remark 2 says harder questions need richer axioms, and Remark 3 leaves open whether understanding new concepts is itself mechanizable.
About this book
Collected Works II: Publications 1938–1974 by Kurt Gödel, 1990. This is a chapter-by-chapter study of the book, with summaries, maps, tables and diagrams; short quotations keep their page references. It is shared free for personal study, is not for sale, and is not endorsed by the author or publisher. Please read and buy the original.
Insight Editions · rajeshrmahapatra.com/insight-editions