Insight Editions · No. 230
Collected Works I
Publications 1929–1936
Kurt Gödel
Every Gödel publication from 1929 to 1936, from the completeness theorem and the 1931 incompleteness paper to the Princeton lectures and reviews, with the editors’ introductory notes.
A study guide to Collected Works I 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.
Truth outruns proof. First-order logic is complete, but every consistent formal system strong enough for arithmetic is incomplete and cannot prove its own consistency.
All Gödel's publications 1929 to 1936: dissertation, 1931 paper, Princeton lectures, 13 colloquium notes, 33 reviews, plus Feferman's life and the editors' notes.
1906 to 1978. Completeness at 23, incompleteness at 24. 46 notions, 45 primitive recursive. Speed-up beyond any computable bound.
Readers who want the actual proofs and history behind the famous theorems, and architects of formal, AI and assurance systems who meet their limits daily.
The Book on One Page
Volume I of Gödel's Collected Works (Oxford, 1986; editor-in-chief Solomon Feferman, with John Dawson, Stephen Kleene, Gregory Moore, Robert Solovay, Jean van Heijenoort) prints every Gödel publication from 1929 to 1936, German originals facing English translations, each preceded by an introductory note by a leading logician. Read in order, it is the record of one decade in which a single person settled what formal systems can and cannot do: they can capture validity completely, they cannot capture arithmetical truth or certify their own consistency, and their reach is measured by an absolute notion of computability.
The argument of the volume, in seven moves.
- Completeness (1929 to 1930). For first-order logic, valid = provable: every formula is refutable or has a countable model. A by-product, compactness, became the foundation of model theory. The unpublished introduction already warns that consistency is not existence and that problems may be provably unsolvable by stated formal means.
- Incompleteness (1930 to 1931). Arithmetize syntax with Gödel numbers, show every primitive recursive relation is representable, and build a sentence that says "I am unprovable". If the system is ω-consistent, neither it nor its negation is provable; formalizing the argument shows the system cannot prove its consistency. The sentence can be made arithmetical, even a statement about a Diophantine equation.
- Reception (1930 to 1936). Königsberg, where almost only von Neumann understood; Hilbert's ω-rule; Zermelo's resistance; Carnap's and Tarski's reading of the antinomies as proofs that truth is undefinable.
- Intuitionism (1932 to 1933). No finite truth tables for intuitionistic logic, and an infinite chain of intermediate logics; the negative translation puts classical arithmetic inside intuitionistic arithmetic; the S4 reading of intuitionistic logic as a logic of provability, with the warning that provability in a fixed system cannot satisfy it.
- Decision problem (1932 to 1933). The class ∃*∀∀∃* is decidable with the finite model property; ∀∀∀∃* already reduces all of logic. The boundary held, except Gödel's unproved extension to identity, refuted by Goldfarb (1984).
- Computability (1934). The Princeton lectures introduce general recursive functions, Gödel's version of Herbrand's idea, as one road to Church's thesis, which Gödel accepted only after Turing's analysis of mechanical procedure.
- Proof length (1936). Higher types give speed-up beyond any computable function on theorems already provable; and computability, unlike provability, is absolute across systems.
Chapter map
| Ch | Title | One-line payload |
|---|---|---|
| 1 | Gödel's Life and Work | Feferman: a frail exacting genius; realism as the engine; 13 categories of work |
| 2 | A Gödel Chronology | Dawson: results packed into 1929 to 1937; exile via Trans-Siberia |
| 3 | The Dissertation | Valid = provable; consistency ≠ existence; Skolem, Herbrand, Gödel compared |
| 4 | The Published Completeness Theorem | Ten theorems; compactness (Theorem X) |
| 5 | Kleene's Guide to Incompleteness | Hilbert's program; seven steps; Rosser, Löb, Gentzen, Paris–Harrington |
| 6 | On Formally Undecidable Propositions | P, Gödel numbering, 46 notions, Theorems VI and XI |
| 7 | Königsberg 1930 | The announcement; Carnap, Heyting, von Neumann manifestoes |
| 8 | Reviews of 1931 | Hilbert's ω-rule and Feferman's verdict |
| 9 | Intuitionistic Propositional Calculus | No finite matrix; chain of intermediate logics |
| 10 | A Special Case of the Decision Problem | ∀∀∃* decidable; classification; the identity error |
| 11 | On Completeness and Consistency | Theorems for Peano arithmetic; ladder of types |
| 12 | Realizations of the Propositional Calculus | Uncountable Lindenbaum extension |
| 13 | Reviews of 1932 | Church's λ-system; Kalmár; Huntington; Dingler |
| 14 | Parry's Axioms; Independence Proofs | Analytic implication; finite models are too coarse |
| 15 | Geometry in Menger's Colloquium | Spherical embedding; collineations; lattice incompleteness |
| 16 | Intuitionistic Arithmetic | Negative translation: classical ⊆ intuitionistic |
| 17 | Intuitionistic Logic in S4 | Provability reading; Solovay's GL |
| 18 | The Decision Problem, in Full | Finite models via a mod-7 tournament |
| 19 | Reviews of 1933 | Lewis's pluralism; tribute to Hahn |
| 20 | The Princeton Lectures | General recursive functions; β-function; Church's thesis |
| 21 | Reviews of 1934 and 1935 | Skolem's non-standard model; Carnap on truth |
| 22 | Discussion Remark | Income and factor prices in equilibrium |
| 23 | On the Length of Proofs | Speed-up; computability is absolute |
How to read this edition. The source is mostly commentary on short papers: the introductory notes (Feferman, Dawson, Dreben, van Heijenoort, Kleene, Troelstra, Goldfarb, Quine, Webb, Vaught, Parikh) are often longer than the texts they introduce. This edition keeps Gödel's own arguments in full, attributes each interpretation to the note's author by name, and marks with CRITICAL LENS the places where Gödel or a commentator erred, overreached, or was later overtaken. SINCE THEN boxes update the 1986 state of knowledge to 2026.
Gödel's Life and Work
Solomon Feferman's opening essay does two jobs. It tells the story of a frail, private, relentlessly exact man who changed logic in a single decade (1929 to 1939), and it maps the entire Gödel corpus into thirteen categories, from completeness to cosmology. The thread running through both is Feferman's claim that Gödel's mathematical realism was the engine of his results, not a philosophical ornament added later.
Part I: Life and career
Brno, 1906 to 1924
Kurt Friedrich Gödel was born on 28 April 1906 in Brünn (Brno), Moravia, then part of Austria-Hungary, the second son of Rudolf Gödel, a self-made managing director and part-owner of a leading textile firm, and Marianne Handschuh, whose Rhineland family had also come for the textile trade and who had a better-than-ordinary education, partly at a French school. The family belonged to the German-speaking minority in a mainly Czech region. Most of what is known about the childhood comes from his brother Rudolf, four years older, later a successful radiologist.
- "Herr Warum". The family nicknamed Kurt Mr. Why for his constant questioning, an early sign of the inquisitiveness that later became method.
- Rheumatic fever at six or seven. He recovered fully but became convinced he had permanent heart damage. Feferman reads this as the origin of a lifelong hypochondria combined, fatally, with distrust of doctors.
- Religion. He was baptized Lutheran, his mother's faith (his father was "Old" Catholic), attended the Evangelische Volksschule from 1912, and took religion more seriously than his family did.
- School record. At the Deutsches Staats-Realgymnasium (1916 to 1924) he received the highest marks in every subject, excelling in mathematics, languages and religion. Surviving notebooks show striking precision in geometry.
- Politics at a distance. World War I barely touched Brno, but the 1918 collapse of the empire put the city into Czechoslovakia and began to squeeze the German-speaking minority. The family stayed comfortable in their villa.
Vienna and the Circle, 1924 to 1929
In autumn 1924 Gödel enrolled at the University of Vienna, intending to study physics. He became an Austrian citizen in 1929. Post-imperial Vienna was economically shrunken but intellectually volatile, and Gödel soon met the Vienna Circle.
- Switch to mathematics (1926). Two reasons are recorded: his taste for precision and the impression made by the number theorist Philipp Furtwängler.
- The faculty. Professors Furtwängler, Hans Hahn and Wilhelm Wirtinger; associate professor Karl Menger; unsalaried lecturers Eduard Helly, Walter Mayer and Leopold Vietoris.
- Olga Taussky's portrait. She met him in 1925 in Moritz Schlick's seminar on Russell's Introduction to Mathematical Philosophy. Gödel hardly ever spoke but was very quick to see problems and point to solutions; his help was in demand and he explained things slowly and calmly.
- Hans Hahn, analyst, set-theoretic topologist and philosopher of science, became his principal teacher and introduced him to Schlick's group, later called the Vienna Circle, the home of logical positivism. Gödel attended regularly from 1926 to 1928, then drifted away while staying close to Rudolf Carnap.
The Circle shaped his agenda even as he rejected its creed. Its blend of Mach's empiricism and Russell's logicism, filtered through Wittgenstein's Tractatus, made logic and foundations the live questions. Yet Gödel had already formed philosophical views almost diametrically opposed to positivism; by his own later account he was a realist about mathematics by 1925.
The book that set the problem. Feferman names two direct triggers for Gödel's first research: Carnap's lectures on mathematical logic and Hilbert and Ackermann's Grundzüge der theoretischen Logik (1928). Against the massive Principia, the Grundzüge was slim and mathematically direct, and it posed an open question: is the standard axiom system for the first-order predicate calculus complete, that is, does it derive every logically valid formula? Gödel answered yes in summer 1929, aged 23. The doctorate followed in February 1930. Hahn was the nominal adviser, but Gödel later stressed he had finished the work before showing it to Hahn, using his suggestions only for editorial revision.
The decade of results, 1929 to 1939
In 1930 Gödel set out to advance Hilbert's program: proving the consistency of formal mathematics by finitary means. He began with analysis, trying to reduce its consistency to that of arithmetic, and hit an obstacle tied to the paradoxes of truth and definability. The paradoxes did not apply to precisely specified formal languages, but he saw that a non-paradoxical analogue could be run by replacing "true" with "provable". The result:
- First incompleteness theorem. Any formal system S containing enough arithmetic and meeting minimal consistency conditions has an arithmetical sentence A such that neither A nor ¬A is provable. A is in fact true, since it expresses its own unprovability through a coding of S's syntax in arithmetic (Gödel numbering).
- Second incompleteness theorem. A sentence C expressing S's consistency is unprovable in S if S is consistent. If all finitary reasoning could be formalized in one consistent S, Hilbert's program could not be carried out for S or anything stronger.
John von Neumann, only three years older and already famous, was among the first to grasp the significance. Paul Bernays, Hilbert's collaborator, accepted the results but needed repeated correspondence to clear up the proofs. Ernst Zermelo misread truth and proof so badly that he derived a flat contradiction with Gödel's theorem, and Gödel's patient letters in 1931 did not convince him. Feferman's judgment: within a few years the methods came to infuse all of mainstream logic.
The incompleteness paper became his Habilitationsschrift in 1932. Hahn called it epochal, "an achievement of the first order". The Habilitation made him a Privatdozent: the right to lecture, with no salary beyond student fees. He would lecture in Vienna only intermittently.
Rudolf Gödel (father, 1874 to 1929): textile director; died suddenly at 54 in February 1929, leaving the family financially secure.
Marianne Gödel (mother, 1879 to 1966): cultured; moved to a Vienna apartment with both sons, returned to Brno in 1937.
Adele Nimbursky, née Porkert (1899 to 1981): a dancer, previously married, six years older; met at 21, opposed by his father; married 20 September 1938.
Hans Hahn: principal teacher, Circle co-founder, wrote the Habilitation report; died 1934.
Karl Menger: ran the Mathematical Colloquium where Gödel published 13 papers.
John von Neumann: early champion; called Gödel "the greatest logician since Aristotle".
Oswald Veblen: built Princeton mathematics; arranged Gödel's IAS visits and later his escape.
Menger's colloquium, meeting from 1929, became Gödel's real workshop. He helped edit its Ergebnisse eines mathematischen Kolloquiums and published thirteen short papers there from 1932 to 1936: intuitionistic logic, the decision problem, geometry, length of proofs. Over the same years he was an active reviewer for Zentralblatt für Mathematik and, less often, Monatshefte für Mathematik und Physik. He never reviewed again after 1936. At home, the three Gödels went out often, especially to the theatre, and Kurt, said his brother, went out of his way to "hide his light under a bushel" despite growing fame.
Alfred Tarski visited Vienna in early 1930 (Gödel discussed his dissertation with him) and again for the first half of 1935.
Princeton, breakdown and set theory, 1933 to 1938
Money came from America. The Institute for Advanced Study (IAS) was founded in 1930; Abraham Flexner appointed Einstein and Veblen in 1932, and Veblen assembled a "matchless" faculty: James Alexander, Marston Morse, von Neumann, Hermann Weyl. Veblen also arranged postdoctoral visits for rising young mathematicians, Gödel among them.
- 1933 to 1934: first IAS year; spring 1934 lectures on incompleteness (published as 1934). He was lonely and depressed, and after returning to Europe suffered a nervous breakdown and entered a sanatorium.
- 1935: a return visit, postponed to autumn, was cut short after two months by mental illness.
- 1936: more time in sanatoria; he could not teach in Vienna until spring 1937.
The breakdowns coincide with the hardest technical work of his life. Gödel had the idea of the constructible sets early, told von Neumann in 1935 that they model ZF plus the axiom of choice, and then spent two more years proving the generalized continuum hypothesis (GCH) holds there too. A shorthand note in his first workbook records that he "essentially found" the GCH proof on the night of 14 to 15 June 1937. Feferman suggests the strain of this work may explain part of the illness of 1934 to 1937.
The set-theory problem had a long history. Cantor proved the continuum uncountable and conjectured its cardinal is the first uncountable one (CH). Zermelo showed well-ordering ⇔ axiom of choice (AC) in 1904 and axiomatized set theory in 1908; work by Fraenkel, Skolem, von Neumann and Bernays refined the axioms. Gödel's result: AC and GCH are consistent with ZF, so ZF cannot disprove them if ZF is consistent. That gave a minimal guarantee of safety for two contested principles.
Exile, 1938 to 1940
The personal and political worlds shifted together. Friends scattered: Marcel Natkin to Paris, Herbert Feigl to America, Carnap to Prague (1931) and later America. Hahn died in 1934. Moritz Schlick was murdered in 1936 by a deranged former student on his way to a lecture. Menger left for Notre Dame in 1937; Gustav Bergmann and Abraham Wald left in 1938. Austria went from the Dollfuss semi-fascist regime (1934, Dollfuss assassinated by Nazis that year) to Schuschnigg to the Anschluss of March 1938, after which the Vienna Circle finally disintegrated.
Apolitical to a fault. Feferman describes Gödel's stance as "basically apolitical and non-committal": he saw what was happening and ignored its implications. Long after, he blamed his 1939 predicament more on Austrian Schlamperei (sloppiness) than on the Nazi regime. Feferman records this without excusing it, and the reader should note how thin the evidence for Gödel's own reasoning is.
- 1938 to 1939: married Adele (September 1938) and left two weeks later for the IAS (autumn: lectures on AC and GCH), then Notre Dame in spring 1939 (set-theory lectures and an elementary logic course with Menger).
- The trap. Back in Vienna, he was found "fit for garrison duty" despite his conviction that his heart was weak. The Nazis had abolished the Privatdozent post; the replacement Dozent neuer Ordnung required a new application, and his was stalled over his associations with Jewish professors, Hahn above all, and his lack of open support for the regime.
- November 1939: a desperate letter to Veblen. Non-quota US visas and German exit permits were somehow arranged.
- January to March 1940: too dangerous to cross the Atlantic, Kurt and Adele went by train through Eastern Europe, the Trans-Siberian Railway, Manchuria, to Yokohama, by ship to San Francisco, and by train to Princeton.
- Irony. His Dozent application was approved in June 1940, and Vienna's catalogues listed him from 1941 to 1945 as lecturer in foundations with the note "wird nicht lesen" (will not lecture). He never returned to Europe.
Princeton, 1940 to 1978
He became an Ordinary Member of the IAS in 1940, Permanent Member in 1946 and Professor in 1953. His closest friends were Albert Einstein and Oskar Morgenstern, the ex-Viennese economist who co-wrote Theory of Games and Economic Behavior (1944) with von Neumann.
The citizenship hearing, April 1948. Preparing seriously for the routine examination, Gödel studied the US Constitution and told Morgenstern he had found "a logical-legal possibility" by which the USA could become a dictatorship. Morgenstern urged silence. On the drive to Trenton, Einstein told anecdote after anecdote to distract him. When the official remarked that dictatorship was "fortunately not possible in America", Gödel cried out "On the contrary, I know how that can happen!" and the two witnesses had trouble stopping him from explaining. Feferman notes the story is third-hand and translated, so the quotations are approximate.
"They were very different in almost every personal way… But they shared a fundamental quality: both went directly and wholeheartedly to the questions at the very center of things." Ernst Straus, Einstein's assistant, on Einstein and Gödel
The work of the Princeton years, in sequence:
- Early 1940s, logic. Strenuous attempts to prove the independence of AC and CH, with partial success only for AC (in finite type theory), never published. A constructive interpretation of arithmetic (the later Dialectica or functional interpretation) proving its consistency by means beyond finitism; lectured at Yale in 1941, published only in 1958.
- From 1943, philosophy. 1944 on Russell's logic, the first open statement of his platonism; 1947 on Cantor's continuum problem; the 1946 Princeton bicentennial address. Long study of Kant and Leibniz, then Husserl from the late 1950s.
- 1947 to 1951, cosmology. Rotating solutions of Einstein's equations with closed timelike lines, permitting "time travel" into the past. Gödel said the motive came from Kant's philosophy of time, not from talks with Einstein, whose unified field theory project he doubted.
- Breadth. The notebooks show sustained interest in history and theology, even a long fascination with demonology.
As a professor he took Institute business, especially applications from logicians, extremely seriously. Hassler Whitney recalled that it was hard to appoint a logician because Gödel could not "prove to himself" that other candidates should not be members. The IAS became a Mecca for logic largely because of him. William Boone, Georg Kreisel, Gaisi Takeuti, Dana Scott and Hao Wang had deep contact; Clifford Spector and Abraham Robinson impressed him. But he never had students or disciples.
1951: first Einstein Award (shared with Julian Schwinger) and Gibbs Lecture.
1955: National Academy of Sciences. 1957: American Academy of Arts and Sciences.
1968: Royal Society (Foreign Member). 1975: National Medal of Science from President Ford, accepted by Saunders Mac Lane because Gödel was too ill.
1966: refused honorary membership of the Austrian Academy of Sciences, citing a pseudo-legal worry about his US citizenship.
Decline and death
Health worsened from the late 1960s. He refused recommended prostate surgery; in the 1940s he had delayed treatment of a bleeding ulcer so long that only emergency transfusions saved him. In the early 1970s he circulated notes proposing new axioms implying CH is false ("Scales of functions"); errors were found and the notes were withdrawn, and he blamed the oversight on medication. When Adele was disabled by a stroke and moved for a time to a nursing home, his depression returned with paranoia: he feared poisoning and stopped eating. He died in Princeton Hospital on 14 January 1978 of "malnutrition and inanition caused by personality disturbance". Adele died on 4 February 1981; they had no children.
Part II: Works, thought and influence
The thirteen categories of the corpus
Feferman sorts everything in Volumes I and II into thirteen groups, which broadly follow chronology.
| Cat. | Area | Items | Payload |
|---|---|---|---|
| a | Completeness | 1929, 1930, 1930a | Validity = provability; compactness |
| b | Incompleteness | 1930b, 1931, 1931a, 1932b, 1934 | Undecidable sentences; consistency unprovable; general recursiveness |
| c | Speed-up | 1936a | Higher types shorten proofs beyond any computable bound |
| d | Decision problem | 1932a, 1933i | ∃…∃∀∀∃…∃ decidable; one more ∀ gives a reduction class |
| e | Intuitionism | 1932, 1933e, 1933f | No finite truth-table semantics; negative translation; S4 reading |
| f | Propositional calculus | 1932c, 1933, 1933a | Uncountable Lindenbaum extension; relevance; independence |
| g | Geometry | 1933b, c, d, g, h | Menger colloquium notes; one joint paper with Wald |
| h | Set theory | 1938, 1939, 1939a, 1940 | L: consistency of AC and GCH |
| i | Philosophy of maths | 1944, 1946, 1947, 1964 | Realism; ordinal definability; CH likely false |
| j | Functional interpretation | 1958, 1972 | Primitive recursive functionals of finite type, theory T |
| k | Cosmology, time | 1949, 1949a, 1952 | Rotating universes; idealist view of time |
| l | Miscellaneous | 1936, 1972a, 1974 | Wald's equations; anti-mechanism; praise of non-standard analysis |
| m | Reviews | 33 reviews, 1931 to 1936 | Zentralblatt and Monatshefte |
Highlights by category
- (a) Completeness. Gödel proved more than asked: every closed formula is either refutable or has a countable model, a form of the downward Löwenheim–Skolem theorem, extended to countable sets of formulas. The published 1930 dropped the dissertation's philosophical introduction, where he had already raised the possibility of incompleteness, and added compactness: if every finite subset of Σ is satisfiable, so is Σ. Maltsev (1936) and Henkin (1949) extended it to uncountable Σ, and it became the bedrock of model theory.
- (b) Incompleteness. 1931 works with P, Principia plus Peano axioms at the ground type. Key innovations: arithmetization of syntax, the notion of a relation being decidable (entscheidungsdefinit) in S, the proof that every primitive recursive relation is so, and a sentence G "saying" it is unprovable. (i) If S is consistent, G is unprovable; (ii) if S is ω-consistent, ¬G is unprovable. Formalizing (i) gives ⊢ W → G, hence W is unprovable (W = consistency). The second theorem was only sketched; the promised Part II never appeared, and the first full proof came in Hilbert–Bernays 1939. The undecidable sentence can be put in the form of a Diophantine equation with mixed quantifiers.
- Princeton 1934. Lecture notes by Kleene and Rosser introduced general recursiveness from a suggestion by Herbrand. Church proposed λ-definability as the exact meaning of effective calculability; Gödel did not accept "Church's thesis" until Turing (1937) analysed mechanical procedure directly.
- (c) Speed-up. In a hierarchy of systems Sₙ of increasing type, some formulas provable in both Sₙ and Sₙ₊₁ have proofs in Sₙ₊₁ shorter by more than any computable function. Gödel also noted the absoluteness of entscheidungsdefinit across the Sₙ.
- (d) Decision problem. Ackermann had decided ∃…∃∀∃…∃; Skolem had a reduction class ∀…∀∃…∃. Gödel drew the sharp boundary: ∃…∃∀∀∃…∃ decidable, ∀∀∀∃…∃ a reduction class; 1933i added the finite model property. Kalmár and Schütte found some results independently. Gödel's closing claim that the method extends to logic with identity was shown false by Goldfarb (1984).
- (e) Intuitionism. No finite-valued matrix characterizes intuitionistic propositional logic (1932). The negative translation (1933e) shows classical arithmetic is as secure as intuitionistic arithmetic; Gentzen and Bernays had it independently, Kolmogorov in part earlier. 1933f reads intuitionistic logic in S4 with B = "provable", while noting that by the second theorem B cannot be provability in a formal system.
- (f) Propositional calculus. 1932c proves that any consistent set, even uncountable, has a complete consistent extension, using transfinite methods; compactness for propositional logic would follow at once, but Gödel did not draw it. 1933 anticipates relevance logic through Parry's analytic implication; 1933a shows finite truth tables cannot prove every independence result.
- (h) Set theory. L, the constructible hierarchy, is a transfinite extension of Russell's ramified types using arbitrary ordinals. The crux is absoluteness of the definable well-ordering and the lemma that a constructible subset of Lωα lies in Lωα+1, via a downward Löwenheim–Skolem argument and transitive collapse. 1940 uses the class theory BG and V = L, technically less intuitive than 1938's plan, which later logicians preferred. Scott (1961): a measurable cardinal implies V ≠ L.
- (i) Philosophy. 1946 introduces ordinal definability (rediscovered by Myhill and Scott) and suggests large cardinal axioms might decide every set-theoretic question. 1947 argues CH has a definite truth value and is likely false.
- (j) Functional interpretation. Finitary mathematics in Hilbert's sense of concrete intuition almost certainly does not go beyond arithmetic, so consistency needs abstract notions: computable functionals of finite type in a quantifier-free theory T interpreting Heyting arithmetic. Spector (1962) extended it to analysis.
- (k) Cosmology. 1949: first rotating models, violating Mach's principle, non-expanding, with closed timelike lines. 1952 (ICM 1950): expanding rotating models without time travel. 1949a argues for an idealist view of time after Kant and Leibniz.
- (m) Reviews. Thirty-three reviews, 1930 to 1936. Notable: 1931c on Hilbert's ω-rule; 1933m, a tribute to Hahn's real analysis; 1934c on Skolem's non-standard model, which Gödel misprized.
A misstep Feferman names. In reviewing Skolem 1933a, Gödel said a non-standard model satisfying all true arithmetic follows from incompleteness. Feferman corrects him: incompleteness plus completeness yields only a model where some false sentence holds. The right source is compactness, though that argument was not actually made until the 1950s. Skolem's construction, which Gödel did not appreciate, foreshadowed ultrapowers.
The Nachlass
Adele donated the scientific estate to the IAS; John Dawson catalogued it in 1982 to 1984.
- Unpublished manuscripts: a simplified proof of Steinitz's theorem; "Is mathematics syntax of language?" (six versions, meant for the Carnap volume); an expanded Kant–relativity essay; "the true power of the continuum is ℵ₂" (circulated in the early 1970s, withdrawn); and a later attempt proving the opposite, CH, from an axiom about orders of growth.
- Lecture texts: AMS 1933 ("The present situation in the foundations of mathematics"); New York Philosophical Society 1934; AMS 1938 (GCH); Yale 1941 ("In what sense is intuitionistic logic constructive?"); rotating universes 1949; ICM 1950; Gibbs Lecture 1951; an undelivered lecture on undecidable sentences and polynomials.
- Notebooks: over 100, including 16 Arbeitshefte (mathematical workbooks), 14 philosophical and 2 theological, mostly in Gabelsberger shorthand. The 55 index headings include independence of AC and of CH, corrections to Herbrand (Gödel spotted substantive errors that others found only in 1963), consistency and ordinals of analysis, the paradoxes, absolute definability, axioms of infinity.
Gödel's realism
Gödel belongs with Cantor, Frege, Zermelo, Church and in part Bernays among the realists, a position Feferman says matches the working view of the mathematicians' "silent majority" but runs against most developed philosophy since the late 19th century (constructivism, formalism, finitism, nominalism, predicativism, positivism, conventionalism).
Gödel's philosophy of mathematics in six theses
- Independent existence. Mathematical objects exist independently of us, like physical objects.
- Objective truth. Mathematical statements are true or false by objective facts, not by our constructions.
- Explanatory necessity. We posit mathematical objects as we posit physical ones: they are needed for a satisfactory system, as physical objects are needed to explain sense data.
- Mathematical "sense data". Arithmetical instances whose generalizations need axioms beyond arithmetic (Goldbach-type problems, guaranteed by incompleteness) play the role of observations.
- Intuition. A cultivable mathematical intuition gives genuine knowledge and can lead us to accept new axioms.
- Fruitfulness. Axioms can also be justified by their consequences, a weaker warrant than intuition.
Applied to set theory: the iterative conception (the cumulative hierarchy) is consistent and untouched by the paradoxes; ZF and AC are evidently true of it; so CH has a determinate truth value. After Cohen (1963) proved independence, Gödel's expectation was confirmed: new axioms, perhaps large cardinals or ideas yet unknown, must settle it.
Was the platonism there from the start? At the end of 1938 Gödel wrote that V = L "seems to give a natural completion of the axioms of set theory". Martin Davis argues this is not in the spirit of 1947 and that his platonism evolved more gradually than his later statements suggest. Feferman leaves the question open. Gödel's own retrospective claims (in letters to Hao Wang, 1967 to 1968) that realism produced his successes, where Skolem missed completeness and Hilbert failed on CH, are testimony written decades later.
Character and influence
- Style. Each paper has clear purpose, careful organization, great precision and no wasted energy; each solves a problem stated in terms understood at the time. He reworked papers many times for the most efficient presentation.
- Mathematical payloads. He took care to extract results of mathematical interest: compactness, Diophantine incompleteness, non-measurable PCA sets in L (the last suggested to him by Ulam, per Kreisel).
- Truth and computability. He bordered both founding concepts of modern logic. He said incompleteness came from seeing that arithmetic truth is undefinable in arithmetic, crediting Tarski with the exact concept. On computability he held out against Church until Turing gave a direct conceptual analysis, after which he called Turing's work the "precise and unquestionably adequate definition of formal system".
- Tools, not new concepts. He preferred new concepts as instruments: L was "only" Russell's ramified hierarchy with arbitrary ordinals. Only the effective functional of finite type comes close to a new fundamental concept.
- Isolation. Most of the work was done alone, with stimulus from Menger, von Neumann and Bernays. No school, no collaborators on his favourite program, the search for new axioms of set theory, which others took up from the 1960s.
"Archimedes did not invent mechanics, as Gödel did not invent logic. But both of them changed their subjects profoundly." Georg Kreisel, preferring Archimedes to von Neumann's Aristotle
For anyone building on formal systems. Gödel's habit was to state the problem in terms everyone already accepts, then extract the most portable consequence (compactness, Diophantine form) instead of the most philosophical one. Architects of regulated AI systems can use the same discipline: a governance claim earns trust when it is a precise, checkable statement inside an accepted framework, not a broad assertion about what the system "understands".
Since this volume (1986). The Collected Works reached five volumes (III unpublished essays, 1995; IV and V correspondence, 2003). The Gabelsberger notebooks have been under systematic transcription, notably the Max Phil philosophical notebooks, with editions appearing from 2019 onward. John Dawson's biography Logical Dilemmas (1997) and later studies have filled in the illness years Feferman could only sketch.
A Gödel Chronology
John W. Dawson Jr., who catalogued the Nachlass, gives the dated skeleton of Gödel's life, using Gödel's unsent answers to a 1975 questionnaire (the "Grandjean interview"), his workbooks and Carnap's diaries. Read alongside Chapter 1, it shows how tightly the great results cluster between 1929 and 1937 and how much of the rest of the life was voyages, sanatoria, honours and losses.
Brno and Vienna, 1906 to 1929
1906 (28 Apr): born in Brünn, Moravia.
1912 (16 Sep): enters the Evangelische Volksschule, Brünn.
c. 1914: rheumatic fever.
1916: enters the Staats-Realgymnasium (German-language).
1919 to 1921: formal study of Gabelsberger shorthand, the script of his later notebooks.
c. 1920 to 1921: interest in mathematics awakens. c. 1922: first reads Kant.
1924 (19 Jun): graduates; autumn, enters the University of Vienna for physics.
c. 1925: adopts a realist position in philosophy of mathematics.
1926: switches to mathematics; begins attending Schlick's circle.
c. 1927: meets Adele Nimbursky (née Porkert).
1928: Hilbert and Ackermann pose the completeness problem.
1929: first studies Principia mathematica; 23 Feb father dies; 26 Feb released from Czechoslovak citizenship; 6 Jun Austrian citizen; 6 Jul dissertation approved by Hahn and Furtwängler.
1929 (Oct): dissertation to the dean (15th); revised version to Monatshefte (22nd); first meeting of Menger's colloquium (24th).
The annus mirabilis, 1930 to 1931
1930 (6 Feb): Dr. Phil. granted. 14 May: completeness results to Menger's colloquium.
1930 (26 Aug): at the Café Reichsrat, tells Carnap, Feigl and Waismann privately of the first incompleteness result.
1930 (6 Sep): completeness talk at Königsberg (abstract 1930a). 7 Sep: first public announcement of undecidable propositions in the discussion session (1931a).
1930 (23 Oct): abstract 1930b to the Vienna Academy. 17 Nov: 1931 received by Monatshefte.
1930 (20 Nov): von Neumann writes that he has independently found the unprovability of consistency.
Late 1930: IAS formally established.
1931 (Jan): 1931 published. Spring (?): Herbrand suggests a definition of recursive functions (he dies 27 July).
1931 (15 Sep): presents incompleteness to the DMV at Bad Elster; meets Zermelo.
Dozent, Princeton, illness, 1932 to 1937
1932 (25 Jun): 1931 submitted as Habilitationsschrift; 1 Dec: Habilitation granted.
1933 (11 Mar): Dozentur; first course (foundations of arithmetic).
1933 (30 Sep to 6 Oct): crosses on the Aquitania; IAS opens (2 Oct) with Gödel a visiting member to May 1934.
1933 (30 Dec): AMS address, "The present situation in the foundations of mathematics".
1934 (Feb to May): IAS lectures (1934); 18 Apr New York Philosophical Society; 20 Apr Washington Academy, "Can mathematics be proved consistent?"
1934: return on the Rex; elected to the AMS; 24 Jul Hahn dies; autumn, Purkersdorf sanatorium for depression.
1935 (4 May): Vienna course on mathematical logic. 19 Jun: length-of-proofs paper (1936a), last colloquium contribution.
1935 (Sep to Nov): to America on the Georgic; October, tells von Neumann of the AC consistency proof; 17 Nov resigns suddenly from the IAS for depression; returns on the Champlain.
1936: more sanatoria; 22 Jun Schlick murdered.
1937 (May to Jun): Vienna course on axiomatic set theory; night of 14 to 15 Jun, the decisive GCH step.
Marriage, war, escape, 1938 to 1940
1938 (13 Mar): Anschluss. 20 Sep: marries Adele. Oct: sails on the New York; IAS lectures on AC and GCH; 9 Nov results to the National Academy of Sciences (1938); 28 Dec AMS Williamsburg lecture on GCH.
1939 (Jan to Jun): Notre Dame, lecture course and seminar with Menger. Title of Privatdozent abolished; return on the German liner Bremen; called for a military physical.
1939 (25 Sep): applies for Dozent neuer Ordnung. 27 Nov: letter to Veblen: "fit for garrison duty", seeking a non-quota visa.
1939 (15 Dec): lecture at Göttingen on the continuum problem amid frantic visa efforts; 19 Dec exit permits.
1940 (Jan): monograph 1940 published (8th); US visas (12th); Russian transit visas (18th).
1940 (18 Jan to 4 Mar): Trans-Siberian journey; President Cleveland, Yokohama to San Francisco.
1940: Ordinary Member of the IAS; 28 Jun Dozent approval arrives; 15 Nov Brown lecture on CH.
Princeton, 1941 to 1981
1941 (15 Apr): Yale, "In what sense is intuitionistic logic constructive?"; spring lectures on the Dialectica interpretation.
1942 (summer): reputed proof of independence of AC in finite type theory, at Blue Hill, Maine.
1943 to 1944: turns to philosophy; 1944 on Russell.
c. 1945: life-threatening duodenal ulcer, saved by transfusions.
1946: Permanent Member (1 Jul); Princeton bicentennial address (17 Dec).
1947: essay on Cantor's continuum problem.
1948 (2 Apr): US citizenship for Kurt and Adele.
1949: IAS lectures (May) and first publication (1949) on rotating universes; buys 129 (later 145) Linden Lane; 1949a on Kant and relativity.
1950 (31 Aug): ICM address, Cambridge, Mass.
1951: Einstein Award with Schwinger (14 Mar); Yale D.Litt.; Gibbs Lecture (26 Dec).
1952: Harvard Sc.D. 1953 (1 Jul): Professor at the IAS.
1955 (18 Apr): Einstein dies. 1957: von Neumann dies.
1958: Dialectica paper, the last new publication. 1959: begins Husserl. 1961: American Philosophical Society.
1963: Cohen proves independence of AC and GCH; Gödel communicates the papers to the PNAS. 1964: revised continuum essay.
1966: 60th-birthday symposium (Ohio State), which he declines to attend; mother dies in Vienna; refuses the Austrian Academy.
1967 to 1968: London Mathematical Society; Amherst Sc.D.; Royal Society.
1970: "Scales of functions" circulated, then withdrawn.
1972 to 1975: Institut de France; Rockefeller Sc.D.; Robinson dies (1974); National Medal of Science (1975).
1976: retires as professor emeritus.
1977: Adele hospitalized; Morgenstern dies (26 Jul); Bernays dies (18 Sep); Gödel hospitalized at Adele's urging (29 Dec).
1978 (14 Jan): dies at Princeton Hospital of "malnutrition and inanition"; memorial (3 Mar) with Weil, Wang, Kochen, Whitney.
1981 (4 Feb): Adele dies; the Nachlass is bequeathed to the IAS.
The chronology makes one pattern hard to miss: the deaths of Morgenstern and Bernays in 1977 and Adele's hospitalization removed Gödel's last supports, and he died within months. The great results, by contrast, fill only eight years, from the dissertation (1929) to the GCH step (1937).
The Dissertation: Completeness of the Calculus of Logic
Gödel's 1929 doctoral dissertation proves that the standard axioms of first-order logic derive every valid formula, and so turns the vague hope of Hilbert and Ackermann into a theorem. Burton Dreben and Jean van Heijenoort's introductory note explains why it took fifty years after Frege for anyone to ask the question, and how close Skolem and Herbrand came. The unpublished introduction holds the surprise: a year before the incompleteness theorem, Gödel already warns that consistency cannot be equated with existence because a problem might be provably unsolvable by precisely stated formal means.
Why nobody asked for fifty years
Remove quantification over functions from Frege's 1879 system and you get a complete axiomatization of first-order logic. Yet the question of completeness first appeared in print only in Hilbert and Ackermann 1928. Dreben and van Heijenoort blame two traditions, each of which made the question unaskable.
Logicism (Frege, Russell, Whitehead): logic as universal. All deductive reasoning, including analysis and much of set theory, was to happen inside one formalism. There was no outside vantage point from which to survey a system: Sheffer's "logocentric predicament". A system was justified inductively, by its ability to derive ordinary mathematics. Principia even doubted that one could prove a set of undefined ideas minimal.
Algebra of logic (Boole, Peirce, Schröder, Löwenheim): semantics without systems. Quantified formulas were central, but no formal system existed. Löwenheim 1915 works purely with truth of formulas in domains; there are no axioms or rules whose completeness could be asked about.
To pose semantic completeness, one needed both: Frege's formal system treated as an object of mathematical study, and the algebraists' model theory applied to it.
- Post 1921 proved the Principia propositional calculus complete, by truth tables he treated as a decision procedure for provability rather than a semantics. He also proved Post completeness: adding any unprovable formula makes everything provable. Trying in 1920 to 1921 to extend the method to quantifiers, Post conjectured that "a complete symbolic logic is impossible", foreshadowing incompleteness by about a decade. His stance followed C. I. Lewis's "heterodox" view of a mathematical system as marks manipulated by rules independent of meaning.
- Bernays 1926 (from his 1918 Habilitationsschrift) spoke openly of "universally valid" formulas and proved propositional completeness via conjunctive normal forms, plus Post completeness. His independence proof for the propositional axioms broke with Russell, who doubted logical axioms could be shown independent.
- The 1920s agenda was not completeness but the decision problem (from Schröder and Löwenheim). Bernays's 1927 survey ignores quantificational completeness.
- Hilbert at Bologna, September 1928, posed a Post-style completeness for number theory: adding an unprovable formula should yield contradiction. For logic, he said, the rules were known to suffice only "through experiment".
- Hilbert and Ackermann 1928 finally asked whether their axioms derive all formulas correct in every domain, adding that sufficiency was known "purely empirically".
The question as printed was empty. Hilbert and Ackermann defined "logical formulas" on p. 54 as formulas provable from the logical axioms alone, so asking whether all "logical formulas" are derivable was circular. The semantic notions "universal validity" and "satisfiability" for quantified formulas only appear on p. 72, with the decision problem. The 1938 second edition replaced the phrase with allgemeingültige Formeln. Gödel answered the question that was meant, not the one that was printed.
The suppressed introduction
The dissertation (approved 6 July 1929 by Hahn and Furtwängler) opens with a philosophical section that the published version (1930) dropped. Dreben and van Heijenoort note it is pure speculation whether Hahn's advice or Gödel's own caution removed it.
- Two equivalent forms. Completeness says every valid formula is derivable; equivalently, every consistent first-order axiom system has a realization. The second form is a "theoretical completion" of the usual way of proving consistency: either derive a contradiction or exhibit a model; the method can never fail in principle.
- Against Brouwer. Brouwer had stressed that consistency does not yield a constructible model. Gödel (who may or may not have heard Brouwer's March 1928 Vienna lectures, arranged by Menger) sides with him on that point.
- Against "consistency = existence". A rival view, usually ascribed to Hilbert though unnamed, defines existence as consistency, making completeness pointless. Gödel objects: that definition presupposes every problem is solvable. If some problem about the reals were proved unsolvable, there would be two non-isomorphic models of the real-number axioms, contradicting the provable categoricity of those axioms. And unsolvability proofs cannot be excluded, because "provable", "consistent" and so on only have exact meaning relative to precisely delimited means of inference.
- Carnap's footnote. If "logical consequence" is replaced by Russellian formal implication, model existence for consistent systems becomes trivial, since a false proposition implies everything. Gödel credits the observation to an unpublished Carnap manuscript.
This is the first written trace of incompleteness. The remark that formal unsolvability might be provable is aimed at Hilbert's optimism and also at Brouwer. Dreben and van Heijenoort add a correction: Gödel blurs first- and second-order logic here, since categoricity of the reals holds only under the standard second-order interpretation. The blur does not undercut his real target, the claim that existence is consistency.
On using classical means to prove completeness
Gödel uses the law of excluded middle for infinite collections without apology (though not the non-denumerable infinite in the main proof). He anticipates the objection that completeness is a kind of decidability, so assuming excluded middle begs the question, and answers in three steps.
- Only intuitionists read excluded middle as "every problem is decidable".
- Even on that reading it asserts solvability by any means imaginable, while the theorem shows derivability by specific, enumerated rules. (A footnote doubts that such sweeping "solvability" even makes sense.)
- An intuitionistic completeness proof would mean something different and would require solving the decision problem. Completeness, unlike consistency, did not arise from foundational controversy and could be posed in naive mathematics, so no special restriction on methods is called for.
The logical system
The system is Principia's restricted functional calculus (*1 and *10) in Hilbert–Ackermann notation. Primitives: ∨, ¬, (x); &, →, ~ (equivalence) and (E) are abbreviations. "Extended sense" adds identity.
Gödel's axioms and rules
- X ∨ X → X
- X → X ∨ Y
- X ∨ Y → Y ∨ X
- (X → Y) → (Z ∨ X → Z ∨ Y)
- (x)F(x) → F(y)
- (x)[X ∨ F(x)] → X ∨ (x)F(x)
- x = x (identity)
- x = y → [F(x) → F(y)] (identity)
Rules: (R1) detachment; (R2) substitution for propositional and functional variables; (R3) from A(x) infer (x)A(x); (R4) renaming of free or bound individual variables. The universal domain must be non-empty, or Axiom 5 fails.
Gödel separates syntactic notions (provable, refutable, normal expression, where signs enter "purely as figures in space") from semantic ones (satisfiable in a domain, valid in a domain, valid). He also introduces individual constants and functional constants for "applied" axiom systems, giving Hilbert's geometry without the continuity axioms as an example of a first-order axiom system.
Six lemmas taken from Hilbert–Ackermann
- Propositional completeness: every propositional formula is refutable or satisfiable (Axioms 1 to 4 are even Post complete).
- Replacement: if A ~ A′ is provable, replacing A by A′ inside B gives a provable B ~ B′.
- Prenex form: every expression is provably equivalent to a normal expression (all quantifiers in front).
- Permuting adjacent existential quantifiers preserves provable equivalence.
- Interleaving prefixes: for F and G with disjoint variables, the quantifier strings can be merged in any order that preserves the order within each.
- The key formula: (x)F(x) & (Ex)G(x) → (Ex)[F(x) & G(x)], derived from Axioms 5, 6, Rule 3 and Hilbert–Ackermann formula 34.
The proof
Step 1: reductions
Soundness is immediate: axioms are valid and rules preserve truth. The work is the converse, proved in the form every formula is either satisfiable or refutable.
- Normal form. By Lemma 3, restrict to prenex formulas.
- No free variables. Replace A by its universal closure; refutability and satisfiability transfer.
- Prefix shape. Pad the prefix so it begins with ∀ and ends with ∃ (add a dummy quantifier).
- Degree. The degree is the number of blocks of universal quantifiers separated by existentials. Degree k+1 reduces to degree k: introduce a new functional variable F and form B, which says that F holds of exactly the tuples where the inner formula (P′)A holds, together with (u)(Ev)F(u, v). B is provably equivalent to a formula B″ of degree k. If B″ is satisfiable, so is (P)A; if B″ is refutable, substituting (P′)A for F turns the remainder into a tautology T and shows (P)A refutable. Gödel notes Skolem used a similar trick for the Löwenheim–Skolem theorem.
So everything rests on degree 1: (x₁…xᵣ)(Ey₁…yₛ)A, with A quantifier-free.
Step 2: derived expressions and the basic alternative
Order the r-tuples of an infinite list of variables x₁, x₂, … by increasing sum of subscripts. The n-th derived expression (Pₙ)Aₙ is the conjunction of n copies of A: the k-th copy takes the k-th r-tuple for the universal variables and s fresh variables for the existential ones, all bound by existential quantifiers in front. Exactly the variables x₁ to x₁₊ₙₛ occur in Aₙ.
The bridge to the formal system is Gödel's own contribution: for every n, (P)A → (Pₙ)Aₙ is provable, by induction on n using Lemmas 4 to 6. Dreben and van Heijenoort single this out as "simple, but for completeness essential": it ties Skolem's semantic analysis to derivability.
Replace each atomic component of Aₙ by a propositional variable to get a propositional formula Cₙ. Each Cₙ is either refutable or satisfiable (Lemma 1). Two cases:
- Some Cₙ is refutable. Then ¬Aₙ is provable, so ¬(Pₙ)Aₙ is, and since (P)A → (Pₙ)Aₙ is provable, (P)A is refutable.
- Every Cₙ is satisfiable. There are satisfying systems of every level n, defined on {1, …, 1 + ns}. Each level has only finitely many, and restricting a level-(n+1) system gives a level-n system. So some level-1 system extends to infinitely many higher ones; choose one of those at level 2 with the same property; repeat "in a familiar manner". The union S of the resulting chain S₁ ⊆ S₂ ⊆ … is a system on all natural numbers that satisfies (P)A: every r-tuple appears at some stage n, and Aₙ supplies the witnesses.
Why "in a familiar manner" matters. The step is an instance of König's infinity lemma (1926, 1927): finitely branching, infinitely many nodes, hence an infinite branch. Gödel cites everything else carefully, so Dreben and van Heijenoort argue he means not König's lemma but the folklore argument behind it: some form of choice, or an ordering that avoids choice. Any uniform ordering of the satisfying assignments works, and Skolem 1929 used exactly such an ordering. Unlike Skolem, Gödel never questions the axiom of choice here.
Corollary: every formula is refutable or satisfiable in a denumerable domain, which yields the Löwenheim–Skolem theorem as a by-product.
Step 3: identity
With "=" the countable-domain version fails ((x)(y)(x = y) has only one-element models), so the claim becomes: A is provable or ¬A is satisfiable in an at most denumerable domain. Replace "=" by a fresh relation G and add K′, the reflexivity and substitutivity conditions on G for every functional variable in A. If K′ → A′ is provable, substituting "=" back gives A. Otherwise K′ & ¬A′ has a model, G is an equivalence relation compatible with all functions, and quotienting by its classes turns G into true identity.
Step 4: independence of the axioms
Gödel extends Bernays's arithmetical-interpretation technique: assign values so that all axioms but one take the "designated" value 0, rules preserve it, and the omitted axiom does not.
- Axioms 1, 3, 4: Bernays's tables, with quantifiers and individual variables erased and functional variables treated as propositional ones.
- Axiom 2: same, but functional variables restricted to values 0 and 1.
- Axiom 5: let (x)0 = (x)1 = 0; with F = 1, Axiom 5 takes value 1.
- Axiom 6: give every formula of the form (x)A(x) value 0, otherwise (x) has value 1; a provable formula then fails.
- Rule 3: (x)0 = (x)1 = 0 keeps axioms at 0 under Rules 1, 2, 4.
- Rule 4: needed only if axioms use one fixed variable; Gödel shows it cannot be weakened to renaming free variables only.
- Axioms 7 and 8: 7 holds for the universal relation, 8 for the empty relation, each failing for the other (in domains of at least two individuals).
Step 5: countable sets of formulas
The theorem extends to any at most denumerable system of formulas: it is satisfiable or has a finite refutable subsystem. The proof interleaves the derived expressions of all formulas along a diagonal. Consequence for axiomatics: every first-order axiom system, finite or countable, either is inconsistent or has a model, and every proposition A meaningful for the system is either derivable or consistent with it via a model of the axioms plus ¬A.
Skolem, Herbrand, Gödel: who had what
Gödel's own verdict, decades later. To van Heijenoort (1963): he was "practically sure" he did not know Skolem 1923a when writing the dissertation. To van Heijenoort again (1964): Skolem implicitly proved "either A is provable or ¬A is satisfiable" with an informal "provable" but never formulated it, which is why Hilbert and Ackermann did not mention it. To Hao Wang (1967): completeness is "an almost trivial consequence of Skolem 1923a", but nobody, including Skolem, drew the conclusion.
- Skolem 1920 proves Löwenheim's theorem with the axiom of choice (Skolem functions on an infinite model). Skolem 1923a avoids choice for foundational reasons, and so must handle the "all Aₙ satisfiable" side by ordering truth assignments and taking a limit, exactly Gödel's case 2. Skolem uses "consistent" and "satisfiable" interchangeably, but he does so in 1920 too, so that alone does not make 1923a a completeness proof.
- Skolem 1928 comes closest: searching for an n with Aₙ unsatisfiable becomes a proof procedure that replaces Frege–Hilbert systems; combined with 1928a and 1929 one can extract soundness and completeness of that procedure. Yet in 51 logic papers (1913 to 1963) Skolem never once mentions completeness.
- Herbrand (1928 to 1929) introduced conjunctive expansions but, as a finitist, refused to conclude ℵ₀-satisfiability when all expansions are consistent; he concluded only that ¬F is not provable. On the other side he showed ¬F has a cut-free proof with the subformula property. Gödel later found errors in Herbrand's proofs that others identified only in 1963.
1879: Frege's system; 1915: Löwenheim; 1920, 1923a: Skolem's two proofs; 1921: Post's propositional completeness; 1926: Bernays; 1928: Hilbert–Ackermann question; 1929: Gödel's answer, aged 23.
50 years between Frege's system and the first printed completeness question.
Later developments
- Henkin 1949 gave a different proof: extend a consistent set with witness constants for existential formulas, then to a maximal consistent set (Lindenbaum's procedure, anticipated by Gödel's 1932c), and read off a model. It depends only on general properties of provability and works for uncountable languages, where Gödel's proof does not.
- Arithmetized completeness. Bernays (Hilbert–Bernays 1939) translated Gödel's proof into number theory using arithmetization of syntax: every consistent first-order system S has an arithmetical model. Kleene reformulated it: adding an unprovable quantificational schema to logic makes number theory ω-inconsistent (Kleene 1952, Theorem 36).
- How complex must the model be? Kleene: predicates in Σ₂ ∩ Π₂. Putnam (1961, 1965): in the Boolean closure of the r.e. Predicates. Kreisel (1953) and Mostowski (1955): not always recursive; Putnam (1957): not always in Σ₁ ∪ Π₁.
Completeness today. Completeness for first-order logic is routinely machine-verified: formalizations exist in Isabelle/HOL (Archive of Formal Proofs), Coq (Forster, Kirst and Wehr, 2021, analysing which parts are constructive) and Lean (the Flypitch project of Han and van Doorn, 2019, which went on to verify the independence of CH), and the Henkin-style proof is now the textbook default. The dissertation's own philosophical introduction, unpublished until this volume (1986), is now read as the earliest evidence of Gödel's path to incompleteness.
Completeness is what makes automated reasoning possible. Because valid = provable, the valid first-order formulas are recursively enumerable: a machine can list every proof. Every resolution prover, SMT solver and proof assistant that checks enterprise rules or regulatory logic relies on this. What completeness does not give is a decision procedure: a search may run forever on an invalid formula, which is why production rule engines restrict themselves to decidable fragments.
The Published Completeness Theorem and Compactness
The 1930 paper in Monatshefte für Mathematik und Physik, received 22 October 1929, is the dissertation rewritten as a sequence of ten numbered theorems, minus the philosophy and plus one new result. That result, Theorem X, is the compactness theorem: a countable set of first-order formulas is satisfiable if and only if every finite subset is. It drew little notice in 1930 and became the foundation of model theory. The Königsberg abstract 1930a compresses the whole to one paragraph.
Opening and setup
Gödel frames the question through Whitehead and Russell: they built logic and mathematics from evident axioms by purely formal inference, so one must ask whether the system suffices for every logico-mathematical proposition, or whether some true propositions, perhaps provable by other principles, cannot be derived. The propositional case was settled by Bernays 1926. A footnote thanks Hahn for "several valuable suggestions". The axiom system is that of Principia *1 and *10, minus the associative principle, which Bernays showed redundant.
- Validity defined. A formula is valid if every substitution of propositions and functions yields a truth; by known theorems, "valid in every domain" equals "valid in the denumerable domain". For formulas with free variables, valid means the universal closure is valid and satisfiable means the existential closure is satisfiable, so "A valid" ⇔ "¬A not satisfiable" without exception.
- Notation. Prefixes (P), (Q), (R); German letters for n-tuples of variables.
- Seven lemmas, stated without proof as well known or easy: tuple quantifier laws (1), reordering (2), substituting tuples (3), interleaving prefixes (4), normal form (5), replacement (6), propositional completeness (7).
The chain of theorems
| Thm | Statement | Role |
|---|---|---|
| I | Every valid formula is provable | The goal |
| II | Every formula is refutable or satisfiable (in the denumerable domain) | Equivalent form actually proved |
| III | If every A*-expression is refutable or satisfiable, so is every expression | Reduce to closed prenex formulas, prefix ∀…∃ |
| IV | Degree k case implies degree k+1 case | Induction on quantifier blocks |
| V | Every formula of degree 1 is satisfiable or refutable | Core case |
| VI | (P)A & (Pₙ)Aₙ → (Pₙ₊₁)Aₙ₊₁ provable, so (P)A → (Pₙ)Aₙ | Bridge to provability |
| VII | With identity, valid ⇒ provable (valid in every domain) | Extended language |
| VIII | With identity, refutable or satisfiable in a finite or denumerable domain | Quotient construction |
| IX | A countable set is satisfiable or has a finite refutable subsystem | Strong completeness |
| X | A countable set is satisfiable iff every finite subset is | Compactness |
Differences from the dissertation
- Ordering. Variables start at x₀, r-tuples ordered by increasing subscript sum "and for equal sums according to some convention". The n-th satisfying system lives on {0, …, ns}.
- Theorem VI is proved in two parts: (I) (P)A → (P₁)A₁, and (II) the step (P)A & (Pₙ)Aₙ → (Pₙ₊₁)Aₙ₊₁, using Lemma 1(b) with the substitution of (Eyₙ₊₁)A(xₙ₊₁; yₙ₊₁) for F.
- The limit argument is shorter. Satisfying systems of each level are finite in number and each level-(n+1) system contains a level-n system as a part; "it follows by familiar arguments" that an infinite chain exists. The limit system makes φₚ hold of a tuple iff it holds in some (hence every later) Sₘ.
- Identity (Theorems VII, VIII): conjoin A with (x)(x = x) and the substitutivity instances of Axiom 8 for each functional variable, replace "=" by G, and identify elements in the same G-class.
- Independence is proved by substitution rather than tables for Axioms 5 and 6: replace (x)F(x) components by X ∨ ¬X (for Axiom 5) or X & ¬X (for Axiom 6); identity axioms via the empty and universal relations, as before. Gödel says the rules are also non-redundant but does not pursue it.
Valid = provable reduces the non-denumerable to the denumerable. Gödel's single remark about uncountability: "valid" quantifies over the non-denumerable totality of all functions, while "provable" needs only the denumerable totality of formal proofs. In modern terms, completeness shows that the set of valid formulas is recursively enumerable. This echoes a remark in Hilbert and Ackermann about the decision problem.
Compactness, Theorem X
Theorem X: a denumerable system of formulas is satisfiable if and only if every finite subsystem is. Theorem IX (strong completeness) follows at once by Theorem II applied to finite conjunctions.
- Proof idea. Reduce every formula to degree-1 normal form (the reductions preserve satisfiability of subsystems). Interleave the instances of all formulas into a single sequence Bₙ, so that the existential closure of Bₙ is a consequence of the first n formulas. If every finite subsystem is satisfiable, every Bₙ is satisfiable, and the limit argument of Theorem V gives a model of the whole system.
- What changed. In the dissertation, the generalization used provability (statement (VII) of the note). Here provability is discarded: "is a consequence of" replaces "provably implies". Dreben and van Heijenoort observe that this brings Gödel's compactness argument very close to Skolem's suggested argument in 1923a.
- Axiomatic reading. Every finite or countable axiom system whose quantifiers range only over individuals is either inconsistent or has a model; the example again is Hilbert's geometry without continuity.
Dissertation 1929. Philosophical introduction (Brouwer, consistency vs existence, possible unsolvability); completeness; identity; independence; extension to countable systems via provability.
Paper 1930. No philosophy; ten theorems; the uncountable-to-countable remark; independence via substitutions; compactness (Theorem X) stated and proved semantically, with strong completeness as its corollary.
The Königsberg abstract (1930a)
Gödel presented the results at the second conference on the epistemology of the exact sciences, Königsberg, 6 September 1930. The abstract says only that the completeness of the Principia axioms had been settled for the propositional calculus and that "the speaker shows how this theorem can be extended" to the restricted functional calculus (formulas without bound functional variables). The following day, in the discussion session, he announced incompleteness (Chapter 7).
What Gödel did not see. Feferman stresses that Gödel never used compactness himself, and its mathematical value is clearer in hindsight. Later, in reviewing Skolem's non-standard model (Chapter 21), he attributed it to incompleteness instead of to his own compactness theorem. The theorem's career came through others: Maltsev 1936 (uncountable languages, with algebraic applications), Henkin 1949, Robinson's model theory and non-standard analysis (1961), which Gödel praised in 1974.
What compactness is used for (the standard modern toolkit)
- Non-standard models of arithmetic: add constant c with axioms c > 0, c > 1, …; every finite part is satisfiable, so the whole is.
- Non-standard analysis: infinitesimals by the same move over the reals.
- Upward Löwenheim–Skolem (with Maltsev's generalization): theories with infinite models have models of every larger cardinality.
- Non-definability: "finite", "connected graph", "torsion" are not first-order expressible.
- Transfer: a first-order sentence true in all fields of characteristic 0 holds in characteristic p for all large p.
Compactness as an engineering intuition. A specification written in first-order logic cannot pin down "finite" or exclude infinite pathological models. When a policy or ontology (OWL, a banking data model) seems to admit strange models, compactness is often the reason. The practical response is to restrict to finite-model reasoning or decidable description logics, and to test specifications against counter-models rather than trusting that axioms say only what was meant.
The Incompleteness Announcement and Kleene's Guide
Stephen C. Kleene's introductory note is a reader's map to the most cited logic paper of the century, written by the man who took the notes for Gödel's 1934 lectures. It places 1931 inside Hilbert's program, reconstructs the proof in seven steps, and follows the results into Rosser's sharpening, the unsolvability of the decision problem, Gentzen's consistency proof and Paris–Harrington. Gödel's abstract 1930b, presented to the Vienna Academy on 23 October 1930, states the four headline theorems before the paper appeared. Its second theorem already says that no consistency proof for the system can be formalized in the system itself, even with all of Principia's logic available in the metamathematics.
Dates and documents
7 September 1930: informal announcement at Königsberg (1931a).
23 October 1930: abstract 1930b presented by Hans Hahn to the Vienna Academy of Sciences.
17 November 1930: full paper 1931 received by Monatshefte für Mathematik und Physik.
22 January 1931: note 1932b recasts the results for Peano arithmetic instead of simple type theory (Chapter 11).
1967: English translation by van Heijenoort, approved by Gödel, who added the short bracketed interpolations that appear in this edition.
Hilbert's program, the target
Hilbert's proposals of 1918 and 1922 answered the crisis caused by the set-theoretic paradoxes with a two-part plan.
Hilbert's program in two parts
- Formalize. Specify the symbols, formulas, axioms and rules of a formal system S covering a chosen portion of classical mathematics, so that proofs are mechanical manipulations of forms. Anything borrowed from meaning must be added as an explicit axiom or rule.
- Prove consistency finitarily. Since the objects of S are finite (symbols, strings, strings of strings), study S in a new discipline, proof theory or metamathematics, using only finitary (finit) methods: no completed infinities, only the potentially infinite sequence 0, 1, 2, …, and show that no proofs of both A and ¬A exist.
Kleene's framing of why this seemed reasonable: mathematics runs from the clearly envisioned natural numbers up through reals and higher cardinalities, notions that outrun intuitive meaning. The paradoxes proved that idealized reasoning can go wrong, so Hilbert wanted the idealized part secured by the concrete part. He also hoped S would be complete: for every closed formula A, either A or ¬A provable.
How Gödel found the theorems
After the dissertation Gödel tried to prove the consistency of analysis, by reducing it to number theory: interpret set variables as ranging over arithmetically definable sets. He saw that this needed the truth of number theory, not merely its consistency of number theory. Thinking about Richard's paradox and the Liar, he saw that truth in number theory is not definable in number theory, while provability is. So if all provable formulas are true, some true formulas are unprovable. Kleene's verdict: the result "shook to its foundations Hilbert's program for foundations without quite demolishing it."
Kleene's seven steps
- Choose the system P. Principia without ramification (essentially Ramsey's simple type theory) superposed on Peano's axioms, natural numbers as the lowest type; induction stated with a type-2 variable. Peano himself said his axioms can be found in Dedekind 1888.
- Gödel-number it. Distinct odd numbers for primitive symbols; a sequence n₁, …, nₖ maps to 2n₁ · 3n₂ · … · pₖnₖ. A sequence of sequences gets the same treatment one level up. "Formula" and "proof" acquire numerical counterparts, written FORMULA and PROOF.
- Numeralwise expressibility. A relation R(x₁, …, xₙ) is numeralwise expressible in P if some formula R(x₁, …, xₙ) satisfies: if R holds, R(numerals) is provable; if not, ¬R(numerals) is provable. Gödel's word is entscheidungsdefinit (decidable) in P. For constructively defined R this is a finitary notion, usable within Hilbert's metamathematics.
- Define "recursive" functions, now called primitive recursive (Kleene 1936's term), already used by Dedekind, Skolem, Hilbert and Ackermann. Theorems I to IV give closure under substitution, recursion, logical connectives, bounded quantifiers and bounded least-number operator.
- List 46 notions; the first 45 are primitive recursive, built in order from sequence coding up to "x is a PROOF of y".
- Theorem V: every primitive recursive relation is numeralwise expressible in P (proof only outlined).
- Theorem VI: the first incompleteness theorem.
A slight blemish Kleene points out. Gödel defines the degree of a primitive recursive function as the length of its shortest definition and inducts on it in Theorems V and VII. But degree is not effectively computable from a definition (if it were, one could decide (Ex)T₁(a, a, x)), which would undercut Gödel's claims that the proofs are constructive. The fix is trivial: induct on the length of the particular definition in hand.
ω-consistency and what it really needs
A system is ω-consistent if there is no formula A(x) with A(0), A(1), A(2), … all provable and also ¬∀x A(x) provable. Gödel applies it only to one Σ⁰₁ sentence, so what is used is 1-consistency: every provable Σ⁰₁ sentence is true (Σ⁰₁-reflection). ω-consistency implies simple consistency.
The proof of Theorem VI, as Kleene states it. Let R(x, v) be the primitive recursive relation "x is not the Gödel number of a proof in Pκ of the formula with number v, with the numeral for v substituted for its free variable". Let R(x, v) numeralwise express it. Let q be the Gödel number of ∀x R(x, v). The undecidable sentence is ∀x R(x, q): "I am unprovable in Pκ".
- Unprovable (needs only consistency). If ∀x R(x, q) were provable, some x would number its proof, so R(x, q) would be false, so ¬R(x, q) would be provable, and so would ¬∀x R(x, q): contradiction.
- Its negation unprovable (needs 1-consistency). By the first half, every R(x, q) is true, hence each R(0, q), R(1, q), … is provable; then ¬∀x R(x, q) cannot be provable without violating 1-consistency.
- Consequences. If Pκ is consistent, ∀x R(x, q) is a true Π⁰₁ sentence that is unprovable: Pκ is ω-incomplete (Tarski's term). Adding ¬∀x R(x, q) gives a system that is simply consistent but ω-inconsistent, so proving mere consistency, as Hilbert proposed, would not rule out false theorems. Gödel stressed this at Königsberg.
The diagonal lemma, extracted. The construction generalizes: for every formula B(v) there is a sentence C with number q such that C ↔ B(q) is provable. Gödel states it informally in 1934, crediting Carnap 1934a; precise versions appear in Rosser 1939, Feferman 1960 and Smoryński 1977. Incompleteness is the case B(v) = "v is not provable".
How general?
Gödel notes Theorem VI holds whenever (1) axioms and immediate consequence are primitive recursive after numbering and (2) every primitive recursive relation is numeralwise expressible. Footnote 48a gives his diagnosis: "the true reason for the incompleteness inherent in all formal systems" is that types can be continued into the transfinite, while any formal system has at most denumerably many. Adding a higher type lets one define truth for the system, prove all its theorems true, and so decide its Gödel sentence.
Arithmetic and the decision problem
- Theorem VII: every primitive recursive relation is arithmetical (definable with +, ·, =, quantifiers over ℕ). Key tool: the Chinese remainder theorem to code finite sequences. Hence Theorem VIII: the undecidable sentences are arithmetical.
- Theorem X reduces each Π⁰₁ statement to the satisfiability of a first-order formula, uniformly and formalizably in P, giving Theorem IX: first-order formulas whose validity and invalidity are both unprovable.
- Decision problem. Combine Theorem X with a non-recursive Σ⁰₁ set (Kleene 1936) and Church's thesis, and the Entscheidungsproblem is unsolvable, the result of Church 1936a and Turing 1937 (observed in Davis 1965). The method also handles Church's "second form" of the problem.
The second theorem
Theorem XI: if Pκ is consistent, the sentence W expressing its consistency is unprovable in Pκ. The first half of Theorem VI shows informally W → ∀x R(x, q); all that reasoning is elementary number theory, so it should formalize in P, giving ⊢ W → ∀x R(x, q), whence W is unprovable.
Königsberg and von Neumann. At Königsberg Gödel had only combinatorial undecidable sentences. John von Neumann asked whether number-theoretic ones could be built. Gödel replied that they would need concepts quite unlike addition and multiplication, and was astonished soon after to turn the sentence into a polynomial equation under quantifiers (Theorem VIII). In the same period he derived the second theorem from the first; a letter from von Neumann (20 November 1930) proposing the same result arrived shortly afterwards.
- The missing Part II. The detailed proof of ⊢ W → G was promised for a sequel. It was never written, partly because the results won prompt acceptance. The details proved to need more care than expected.
- First full proof: Hilbert and Bernays 1939, pp. 283 to 340, for their number-theory systems Zμ and Z.
- Löb 1955 isolated the elegant derivability conditions (used in Smoryński 1977). Feferman 1960 identified proof predicates satisfying them and gave counterexamples to the second theorem for predicates meeting only some.
- Resistance. Zermelo's letters after Bad Elster (15 September 1931) and critical articles by Perelman (1936), Kuczyński (1938) and Barzin (1940) show the acceptance was not universal.
The Hilbert–Bernays–Löb derivability conditions (modern standard form, with □A for "A is provable")
- D1: if ⊢ A then ⊢ □A.
- D2: ⊢ □(A → B) → (□A → □B).
- D3: ⊢ □A → □□A (provable Σ⁰₁-completeness for provability).
From D1 to D3 and the diagonal lemma: ⊢ Con → ¬□G, so a consistent theory cannot prove Con.
What survives of Hilbert's program
Gödel himself wrote that Theorem XI does not contradict Hilbert's formalism, since there might be finitary proofs not expressible in P. Kleene's gloss: rather than ending the program, the theorem showed where success must come from, some non-elementary method that can still be construed as finitary.
- Before 1931: finitary consistency proofs for fragments of arithmetic by Ackermann (1924), von Neumann (1927) and Herbrand (1931). Every argument accepted as finitary could be formalized in systems much weaker than PA.
- Gentzen 1936: consistency of PA using transfinite induction up to ε₀ (on a primitive recursive well-ordering via Cantor normal form) as the only addition to finitary principles. Ordinal analysis then extended to subsystems of analysis and set theory (Takeuti 1975, Schütte 1977).
- Gödel 1958 (Dialectica): consistency via computable functionals of finite type. His later view: concrete finitary methods are practically certainly insufficient; abstract concepts are needed. "There is nothing in the term 'finitary' which would suggest a restriction to concrete knowledge. Only Hilbert's special interpretation of it makes this restriction."
Gödel's undecidable sentence. Needs ω-consistency (for the negation half); built from a coded proof predicate; mathematically artificial.
Rosser 1936. Needs only simple consistency: "for every proof of me there is a shorter proof of my negation". Kleene notes W → (D ↔ ∀x R(x, q)) is provable in P.
Paris–Harrington 1977. A natural combinatorial statement (a strengthening of the finite Ramsey theorem), Π⁰₂, equivalent to Σ⁰₁-reflection for PA, hence unprovable in PA and even in PA⁺ (PA plus all true Π⁰₁ sentences). Its function outgrows every provably recursive function of PA (Ketonen–Solovay 1981).
The abstract (1930b)
The system S: Peano axioms plus the logic of Principia (natural numbers as individuals), with the axiom of choice for all types, with or without reducibility and ramification.
The four announced theorems
- S is not complete: there are (exhibitable) propositions A with neither A nor ¬A provable, even of the simple form (Ex)F(x) with F a decidable property of numbers. A footnote adds first-order formulas for which neither validity nor a counterexample is provable.
- No consistency proof for S exists even if all of Principia's logic (including choice) is admitted in metamathematics; a consistency proof needs modes of inference not formalized in S. The same holds for Zermelo–Fraenkel and von Neumann's system of classical mathematics.
- Adding finitely many axioms (or infinitely many obtained from finitely many by type elevation) does not yield completeness, provided the extension is ω-consistent. Some consistent extensions are not ω-consistent.
- The same holds for ω-consistent extensions by infinitely many axioms, provided it is metamathematically decidable what counts as an axiom.
The abstract overreaches on Theorem II. As stated, it says no consistency proof exists even using all of Principia in metamathematics, which is just what the paper proves: no proof formalizable in S. The paper itself is more careful and explicitly leaves open finitary proofs not expressible in P. Readers in 1930 could easily take the abstract as a stronger claim than Gödel later defended.
Since Kleene's note (1986). Natural independence results multiplied: Kirby–Paris (1982) on Goodstein sequences and the hydra game, Friedman's finite form of Kruskal's tree theorem, unprovable even in the much stronger system ATR₀. Machine-checked proofs: first theorem by Shankar (1986, Boyer–Moore), O'Connor (2005, Coq); both theorems by Paulson (2014 to 2015, Isabelle); the FormalizedFormalLogic project has mechanized both theorems and provability logic in Lean 4 (write-up on arXiv, 2026). Provability logic GL (Solovay 1976) completes the derivability conditions: GL proves exactly the modal laws of □ that PA proves about itself.
On Formally Undecidable Propositions of Principia Mathematica and Related Systems I
The 1931 paper proves that every sufficiently strong formal system, if consistent in a suitable sense, leaves some arithmetical sentences undecided, and that such a system cannot prove its own consistency. Gödel does it with three inventions that outlived the theorem: arithmetization of syntax, primitive recursive functions as a calibrated class of computable functions, and the self-referential construction. The undecidable sentence says, in effect, "I am not provable", and it is true, so truth in arithmetic outruns provability in any such system.
Section 1: the idea
Opening claim. Mathematics has been formalized so thoroughly that any theorem can be proved by "a few mechanical rules". The two most comprehensive systems are Principia mathematica (with axioms of infinity, reducibility and choice for all types) and Zermelo–Fraenkel set theory as developed by von Neumann. One might conjecture they decide every question they can express. They do not: both contain relatively simple problems in the theory of integers (footnote 4: using only ¬, ∨, ∀, =, + and · over the natural numbers) that the axioms cannot decide. The cause is not the special systems but a wide class, including all extensions by finitely many axioms that do not make false arithmetical sentences provable.
The sketch with the Richard construction. Formulas are finite sequences of signs and proofs finite sequences of formulas; replace signs by natural numbers and metamathematical notions become arithmetical notions, so "formula", "proof array" and "provable formula" are definable in PM. Arrange the class signs (formulas with one free number variable) in a sequence R(n), and write [α; n] for the result of substituting the numeral for n into class sign α. Define
n ∈ K ≡ ¬Bew[R(n); n]
(Bew = "is provable"). K is definable in PM, so some class sign S expresses it, and S = R(q) for some q. Then [R(q); q] is undecidable: if provable, it is true, so q ∈ K, so it is not provable; if its negation were provable, then q ∉ K, so Bew[R(q); q], and both it and its negation would be provable.
- The antinomies. The analogy with Richard's paradox "leaps to the eye", and with the Liar: the sentence says of itself that it is unprovable. Footnote 14: any epistemological antinomy would serve.
- No vicious circle (footnote 15). The sentence initially asserts only that a well-defined formula (from the q-th class sign by a certain substitution) is unprovable; only afterwards, "so to speak by chance", does it turn out to be the sentence itself.
- The sentence can be written down (footnote 13): a later interpolation warns that without PM's abbreviations the formula and the number q would be of "entirely unmanageable lengths".
- Two assumptions to eliminate. The sketch needs (1) enough expressive power to define provability and (2) soundness: every provable formula is true. The precise version replaces (2) by "a purely formal and much weaker one", ω-consistency.
- The undecided sentence is decided after all. Since [R(q); q] says it is unprovable and is unprovable, it is true. This "curious situation" leads to Section 4.
Section 2: the system P and the proof
The system P
P = the logic of PM superposed on the Peano axioms, numbers as individuals, successor as primitive. Gödel notes the Peano axioms and other changes only simplify the proof.
- Constants: ¬ (not), ∨ (or), Π (for all), 0, f (successor), parentheses.
- Variables of every type n: type 1 for numbers (x₁, y₁, z₁, …), type 2 for classes of numbers, type 3 for classes of classes, and so on. Relations are reduced to classes of ordered pairs (Kuratowski-style pairs as classes of classes), so no relation variables are needed.
- Signs and formulas. Type-1 signs: a, fa, ffa, … where a is 0 (giving numerals) or a variable. Elementary formula: a(b) with a of type n+1, b of type n. Formulas close under ¬, ∨ and generalization xΠ(a). Sentential formula = no free variables; class sign = exactly one free individual variable.
- Subst a(v|b) substitutes b for free v; type elevation raises every variable's type by the same amount.
The axioms of P (abbreviations ., ⊃, ≡, (Ex), = as usual)
- Peano (I): ¬(fx₁ = 0); fx₁ = fy₁ ⊃ x₁ = y₁; x₂(0) . X₁Π(x₂(x₁) ⊃ x₂(fx₁)) ⊃ x₁Π(x₂(x₁)) (induction with a class variable).
- Propositional (II): all substitution instances of p ∨ p ⊃ p; p ⊃ p ∨ q; p ∨ q ⊃ q ∨ p; (p ⊃ q) ⊃ (r ∨ p ⊃ r ∨ q).
- Quantifier (III): vΠ(a) ⊃ Subst a(v|c) (instantiation, with the usual freeness proviso); vΠ(b ∨ a) ⊃ b ∨ vΠ(a) for v not free in b.
- Comprehension (IV): (Eu)(vΠ(u(v) ≡ a)) for u of type n+1 not free in a. This plays the role of reducibility.
- Extensionality (V): x₁Π(x₂(x₁) ≡ y₂(x₁)) ⊃ x₂ = y₂ and all its type elevations. Identity x₁ = y₁ is defined, as in PM *13, by x₂Π(x₂(x₁) ⊃ x₂(y₁)).
Rules: c is an immediate consequence of a and b if a is (¬(b)) ∨ (c) (modus ponens), and of a if it is vΠ(a) (generalization). Substitution is unnecessary because all instances are already in the axiom schemata, a device from von Neumann 1927. The provable formulas are the smallest class containing the axioms and closed under immediate consequence.
Gödel numbering
| Sign | 0 | f | ¬ | ∨ | Π | ( | ) | Variable of type n |
|---|---|---|---|---|---|---|---|---|
| Number | 1 | 3 | 5 | 7 | 9 | 11 | 13 | pⁿ, p a prime > 13 |
A sequence n₁, …, nₖ gets 2n₁ · 3n₂ · … · pₖnₖ (pₖ the k-th prime); a proof, a sequence of formulas, is numbered the same way from the formulas' numbers. Φ(a) denotes the number of a. Every metamathematical relation R has an arithmetical shadow R′, written in SMALL CAPITALS: VARIABLE, FORMULA, AXIOM, PROVABLE FORMULA. Undecidability then reads: there are SENTENTIAL FORMULAS a such that neither a nor the NEGATION of a is a PROVABLE FORMULA.
Recursive functions, Theorems I to IV
A function φ is recursively defined from ψ and μ if
φ(0, x₂, …, xₙ) = ψ(x₂, …, xₙ) φ(k+1, x₂, …, xₙ) = μ(k, φ(k, x₂, …, xₙ), x₂, …, xₙ)
and recursive (today: primitive recursive) if it ends a finite sequence of functions each of which is a constant, the successor x + 1, obtained by substitution, or by recursive definition from earlier ones. The length of the shortest such sequence is its degree. A relation R is recursive if some recursive φ satisfies R(x̄) ⇔ φ(x̄) = 0; such relations are decidable in the ordinary sense (footnote 28).
- Theorem I: substitution and recursive definition preserve recursiveness.
- Theorem II: if R, S are recursive, so are ¬R and R ∨ S (hence R & S).
- Theorem III: if φ, ψ are recursive, so is φ(x̄) = ψ(ȳ).
- Theorem IV: bounded quantifiers (Ex)[x ≤ φ(ȳ) & R(x, ȳ)] and (x)[x ≤ φ(ȳ) → R(x, ȳ)] and the bounded least-number operator εx[x ≤ φ(ȳ) & R(x, ȳ)] preserve recursiveness. The proof builds an auxiliary function χ by recursion that "jumps" to n+1 exactly at the first n where R holds.
The 46 definitions
Starting from +, ·, exponentiation, <, =, Gödel defines 46 notions, each from earlier ones by Theorems I to IV, every quantifier carrying an explicit bound to guarantee recursiveness. The first 45 are recursive; the 46th, Bew(x), is the one notion "of which we cannot assert that it is recursive".
| Nos. | Notions | What they build |
|---|---|---|
| 1 to 5 | x/y, Prim(x), n Pr x, n!, Pr(n) | Divisibility, primes, n-th prime |
| 6 to 10 | n Gl x, l(x), x * y, R(x), E(x) | Sequence coding: n-th term, length, concatenation, singleton, bracketing |
| 11 to 17 | n Var x, Var(x), Neg(x), x Dis y, x Gen y, n N x, Z(n) | Variables, negation, disjunction, generalization, numeral for n |
| 18 to 23 | Typ, Elf(x), Op, FR(x), Form(x) | Signs of type n, elementary formulas, formula sequences, FORMULA |
| 24 to 31 | v Geb n, x; v Fr n, x; v Fr x; Su x(n|y); k St v, x; A(v, x); Sb(x v|y) | Bound and free places, substitution |
| 32 to 33 | Imp, Con, Aeq, Ex; n Th x | Defined connectives; type elevation |
| 34 to 42 | Z-Ax, A-Ax, Q(z, y, v), L₁-Ax, L₂-Ax, R-Ax, M-Ax, Ax(x) | Each axiom schema, then AXIOM |
| 43 to 45 | Fl(x, y, z), Bw(x), x B y | IMMEDIATE CONSEQUENCE, PROOF ARRAY, "x is a PROOF of y" |
| 46 | Bew(x) ≡ (Ey) y B x | PROVABLE FORMULA (unbounded ∃, so not shown recursive) |
The bound for Form(x) is a nice detail: a formula sequence for x need not be longer than the number of subformulas, at most l(x)(l(x)+1)/2 ≤ [l(x)]², so its number is below (Pr([l(x)]²))x·[l(x)]².
Theorem V: representability
Theorem V. For every recursive relation R(x₁, …, xₙ) there is a RELATION SIGN r with free variables u₁, …, uₙ such that for all n-tuples: R(x̄) → Bew(Sb(r with numerals for x̄)) and ¬R(x̄) → Bew(Neg Sb(r with numerals for x̄)). Gödel stresses this states, "without reference to any interpretation", the vague fact that every recursive relation is definable in P.
The proof is only outlined: induction on degree, proving it for relations x₁ = φ(x₂, …, xₙ), since substitution and recursive definition can both be reproduced formally in P. Signs so obtained are called recursive. Footnote 39 gives the intuition: for a recursive relation, P can decide each instance from its axioms.
Theorem VI: the first incompleteness theorem
Let κ be a class of FORMULAS; Flg(κ) is the closure of κ plus the AXIOMS under IMMEDIATE CONSEQUENCE. κ is ω-consistent if there is no CLASS SIGN a with Sb(a v|Z(n)) ∈ Flg(κ) for every n and also Neg(v Gen a) ∈ Flg(κ).
Theorem VI. For every ω-consistent recursive class κ of FORMULAS there are recursive CLASS SIGNS r such that neither v Gen r nor Neg(v Gen r) belongs to Flg(κ).
Gödel's proof in his own notation.
- Define the κ-analogues Bwκ(x), x Bκ y and Bewκ(x), all recursive except Bewκ (since κ is recursive).
- Define Q(x, y) ≡ ¬[x Bκ Sb(y 19|Z(y))]: x is not a κ-proof of the result of substituting y's own numeral into y. Q is recursive, so by Theorem V a RELATION SIGN q (free variables 17 and 19) represents it.
- Put p = 17 Gen q (a CLASS SIGN in variable 19) and r = Sb(q 19|Z(p)) (a recursive CLASS SIGN in variable 17).
- Then Sb(p 19|Z(p)) = 17 Gen r: substituting p's numeral into p yields 17 Gen r, the sentence "for all x, Q(x, p)", that is, "no x is a proof of me".
- 17 Gen r is not κ-PROVABLE. If n were a κ-proof of it, then ¬Q(n, p), so by representability Neg Sb(r 17|Z(n)) is κ-provable; but from 17 Gen r, Sb(r 17|Z(n)) follows: κ is inconsistent.
- Neg(17 Gen r) is not κ-PROVABLE. By 5, no n is a κ-proof, so Q(n, p) holds for every n, so Sb(r 17|Z(n)) is κ-provable for every n; with Neg(17 Gen r) also provable, κ would be ω-inconsistent.
- The proof is constructive (intuitionistically unobjectionable): given a formal decision of 17 Gen r, one can actually exhibit an ω-inconsistency.
- Decidable relations. Gödel now defines a relation as decidable (entscheidungsdefinit) if a RELATION SIGN satisfies the conditions of Theorem V. Every recursive relation is decidable; the theorem needs only κ to be ω-consistent and decidable.
- With mere consistency: one still gets a property r for which neither a counterexample nor a universal proof can be given.
- Consistent but ω-inconsistent systems exist: adjoin Neg(17 Gen r) to κ. Footnote 46 notes this presupposes P is consistent.
- Finite extensions are recursive, so even with the axiom of choice or the generalized continuum hypothesis added, not all propositions are decidable, if these are ω-consistent.
- Only two properties of P were used: (1) axioms and immediate consequence are recursively definable; (2) every recursive relation is definable in the sense of Theorem V. Hence the result holds for ZF, von Neumann's set theory, and Peano arithmetic with recursive definitions (Problem III of Hilbert 1929a), and the undecidable sentences have the form (x)F(x) with F recursive.
Section 3: arithmetical and logical forms
A relation is arithmetical if definable from +, · and ∨, ¬, (x), = with quantifiers over natural numbers only (no set or function variables). Examples: x > y ≡ ¬(Ez)(y = x + z) and x ≡ y (mod n) ≡ (Ez)(x = y + zn ∨ y = x + zn).
Theorem VII: every recursive relation is arithmetical. Induction on degree for relations x₀ = φ(x̄). Substitution is easy. For recursion, φ(0, …) = ψ, φ(k+1, …) = μ(k, φ(k, …), …), write the value as the last term of a sequence f with f₀ = ψ(…) and fk+1 = μ(k, fk, …). Sequences are not arithmetical objects, so replace a sequence by a pair (n, d) coding fk = [n] mod (1 + (k+1)d). Lemma 1: any finite sequence f₀, …, fk−1 is so coded: take d = l! where l bounds k and the fᵢ; the moduli 1 + (i+1)l! Are pairwise coprime (a common prime would divide (i₁ − i₂)·l! And hence l!, impossible), so the Chinese remainder theorem supplies n. This is the device later called Gödel's β-function.
- Theorem VIII: every system of Theorem VI contains undecidable arithmetical propositions, since the equivalence of each (x)F(x) with an arithmetical form is provable in P. The same holds for set theory and its ω-consistent recursive extensions.
- Theorem IX: these systems contain undecidable problems of the restricted functional calculus: formulas whose validity and whose having a counterexample are both unprovable. Footnote 55 links back: in 1930 he showed every formula is provably valid or has a counterexample, but the counterexample's existence is not always provable.
- Theorem X: every problem (x)F(x) with F recursive reduces to whether a certain first-order formula is satisfiable.
Proof of Theorem X. Allow function variables φ, ψ, … (eliminable by PM's descriptions plus uniqueness clauses). Take F(x) ⇔ Φ(x) = 0 with a defining sequence Φ₁ = successor, …, Φₙ = Φ. Write the recursion and substitution equations as formulas (18) to (20), add (21): successor is injective and never yields 0, and (22): (x)Φₙ(x) = 0. Replace each Φᵢ by a function variable and 0 by a variable x₀; call the conjunction C.
- If (x)Φ(x) = 0 holds, the actual functions satisfy (Ex₀)C.
- If (Ex₀)C is satisfied in some domain, take the smallest subdomain containing the witness a and closed under Ψ₁. By (21) it is isomorphic to ℕ with a ↦ 0 and Ψ₁ ↦ successor; the equations force the Ψᵢ to be the Φᵢ, and (22) gives (x)Φ(x) = 0.
Footnote 61: Theorem X implies that Fermat's and Goldbach's problems would be solvable if the decision problem for first-order logic were solved.
Section 4: the second incompleteness theorem
Theorem XI. Let κ be any recursive consistent class of FORMULAS; then the SENTENTIAL FORMULA stating that κ is consistent is not κ-PROVABLE. In particular, the consistency of P is not provable in P, provided P is consistent.
The sketch. Define Wid(κ) ≡ (Ex)(Form(x) & ¬Bewκ(x)): some formula is unprovable. The first half of Theorem VI used only consistency, so (23) Wid(κ) → ¬Bewκ(17 Gen r), which by the definitions means (24) Wid(κ) → (x)Q(x, p). Everything in Section 2 up to Theorem VI, and this implication, uses only methods formalized in P; let w express Wid(κ). Then w Imp (17 Gen r) is provable in P. If w were κ-provable, so would be 17 Gen r, and by (23) κ would be inconsistent.
- Constructive again: from a κ-proof of w one can actually derive a contradiction in κ.
- Set theory and classical mathematics. The proof carries over word for word to set theory M and von Neumann's classical mathematics A: no consistency proof formalizable in them.
- Not a refutation of formalism. "Theorem XI … do[es] not contradict Hilbert's formalistic viewpoint", since it is "conceivable that there exist finitary proofs that cannot be expressed in the formalism of P".
- ω-consistency can be replaced in Theorem VI by: "κ is inconsistent" is not κ-provable. Some consistent κ do prove their own inconsistency.
- The sequel. Results "in full generality" and the full proof of XI were promised for Part II; hence the "I" in the title. A later bracketed note explains that prompt acceptance made Gödel change his plan.
The 1963 note
On 28 August 1963 Gödel added that Turing's work gives "a precise and unquestionably adequate definition of the general notion of formal system", so the theorems hold in full generality: every consistent formal system containing a certain amount of finitary number theory has undecidable arithmetical propositions and cannot prove its own consistency. In his opinion "formal system" should mean nothing else: systems whose reasoning can "be completely replaced by mechanical devices". The "transfinite generalizations of formalisms" he had suggested in a 1946 Princeton lecture are "radically different".
46 defined notions, 45 of them primitive recursive. 11 theorems (I to XI). 7 primitive constants with odd codes 1 to 13.
4 sections; 1 promised sequel never written. Received 17 November 1930; published January 1931; Gödel aged 24.
What 1931 left loose. (1) Theorem V and the second theorem are only sketched; the first rigorous proof of the second theorem waited for Hilbert–Bernays 1939. (2) The induction on degree is non-constructive (Kleene). (3) ω-consistency is a stronger hypothesis than needed, removed by Rosser 1936. (4) "Formal system" lacked a general definition until Turing. (5) Popular readings that the theorem shows minds outstrip machines (Lucas 1961, Penrose 1989) go far beyond anything in the paper; Gödel's own later view was a careful disjunction: either the mind is not a machine, or there are absolutely undecidable problems.
For AI and assurance work. Three exact lessons transfer. (1) Self-certification is limited: a sufficiently rich system cannot certify its own consistency, so assurance of an AI pipeline or rule engine must come from outside it (independent validation, a stronger meta-system, human review). (2) Specification is incomplete: any recursively axiomatized policy rich enough for arithmetic leaves true cases it cannot settle, so escalation paths are a design necessity, not a failure. (3) Arithmetization is the pattern behind "code as data": Gödel numbering is the ancestor of every system that inspects, rewrites or verifies its own programs, including LLM agents that write and check code.
Incompleteness and machine mathematics today. Matiyasevich (1970), completing work of Davis, Putnam and Robinson, showed every r.e. Set is Diophantine, so Gödel's sentence can be a statement that a single polynomial equation has no solution: Gödel's "mixed quantifiers" collapse to one block. Machine-verified proofs now cover both incompleteness theorems (Isabelle 2015, Lean 4). AI provers (DeepMind's AlphaProof, IMO 2024; gold-medal level systems in 2025; Lean-verified solutions to open Erdős problems in 2026) work inside formal systems to which all of Gödel's limits apply: they search for proofs of provable statements and can never settle every true one.
Königsberg 1930: The Announcement and the Three Manifestoes
On 7 September 1930, at the end of a roundtable in Königsberg, an almost unknown 24-year-old from Vienna said that one can give true arithmetical propositions unprovable in classical mathematics. John Dawson's note reconstructs the scene: three manifestoes for logicism, intuitionism and formalism, Gödel's dissertation talk the day before, and a discussion dominated by Hahn and Carnap. Gödel moves in a few sentences from "it remains conceivable" to "one can even give examples", and almost nobody in the room except von Neumann noticed. His later reviews of the three keynote lectures (1932e, f, g) show how he read the rival programs.
The conference
The second Conference on Epistemology of the Exact Sciences (Königsberg, 5 to 7 September 1930) was organized by Reichenbach's Gesellschaft für empirische Philosophie with the Verein Ernst Mach, allies of the Vienna Circle, and announced in Erkenntnis, edited by Hans Reichenbach and Rudolf Carnap.
Friday 5 September: hour addresses by Carnap ("The basic ideas of logicism"), Arend Heyting ("The intuitionistic grounding of mathematics") and John von Neumann ("The axiomatic grounding of mathematics"). Friedrich Waismann added an unannounced talk on Wittgenstein's view of mathematics.
Saturday 6 September: addresses by Reichenbach, Heisenberg and Neugebauer; three 20-minute talks, including Gödel on completeness (1930a). The abstract mentions neither compactness nor the paper 1930, whose offprints were shipped only on 19 September.
Sunday 7 September: roundtable on the foundations of mathematics, chaired by Hans Hahn, with Carnap, Heyting, von Neumann, Gödel, Arnold Scholz, Kurt Reidemeister; a stray Nachlass page shows Emmy Noether and a "v. Geilen" also spoke.
Same week: Hilbert opened the following assembly of German scientists with "Naturerkennen und Logik", ending "Wir müssen wissen. Wir werden wissen."
What Gödel said
First segment, subjunctive. Formalism adjoins to meaningful propositions transfinite pseudo-assertions that round out the system, like points at infinity in geometry. This presupposes that any meaningful theorem proved by a detour through the transfinite is contentually correct, a demand usually replaced by consistency. Gödel's point: the two are not equivalent. From consistency of a system A (say classical mathematics) one gets only that not-p is not formally provable; it "remains conceivable" that not-p could be established by contentual (intuitionistic) considerations not representable in A. For narrow meaningful propositions (finitary numerical equations) this cannot happen, but for a statement (Ex)F(x) with F finitary (the negation of Goldbach's conjecture has this form) it could, "even if one had demonstrated the consistency of the formal system of classical mathematics. For of no formal system can one affirm with certainty that all contentual considerations are representable within it."
Von Neumann's interjection: it is not settled that all intuitionistically acceptable proofs are formally representable.
Second segment, indicative. "(Assuming the consistency of classical mathematics) one can even give examples of propositions (and in fact of those of the type of Goldbach or Fermat) that, while contentually true, are unprovable in the formal system of classical mathematics. Therefore, if one adjoins the negation of such a proposition to the axioms of classical mathematics, one obtains a consistent system in which a contentually false proposition is provable."
The announcement is aimed at a specific Hilbertian assumption: that consistency guarantees soundness for real (meaningful) statements. Gödel shows it fails exactly at the Σ⁰₁ level (statements like "there is a counterexample to Goldbach"), the same level that ω-consistency and 1-consistency protect in 1931.
The Postscript
Solicited by the Erkenntnis editors after 1931 appeared, the Postscript gives the results cleanly:
- Complete means every expressible proposition is formally decidable from the axioms; complete with respect to a class 𝔄 means every member of 𝔄 is decidable.
- No system with finitely many axioms is complete even for arithmetical propositions (those built from +, ·, = over the naturals, with connectives and quantifiers over natural numbers only), under the assumption that no false arithmetical proposition is derivable. With infinitely many axioms the same holds if the axiom scheme meets very general conditions. Examples: Principia (with reducibility, choice, infinity), Zermelo–Fraenkel, von Neumann's set theory, Hilbert's school's systems.
- Consistency in the Hilbertian sense is a combinatorial property of sign systems, expressible in the symbols of the system. For all systems above, the consistency assertion is itself undecidable in the system: consistency proofs need methods not formalized in the system.
- The careful conclusion: for a system formalizing all finitary forms of proof, a finitary consistency proof would be impossible, but "it seems questionable whether one of the systems hitherto set up, say Principia mathematica, is so all-embracing (or whether there is a system so all-embracing at all)."
Why so tentative, and who understood
Dawson lists reasons for the hedged opening: Gödel was a newcomer at a Circle-oriented meeting; he habitually avoided controversy; he later told Hao Wang (1967) of logicians' "prejudice" against the concept of objective mathematical truth, which he side-stepped by a strictly syntactic treatment in 1931; the paper was not yet submitted; the second theorem came later; and, per Wang, he had not yet put the sentence in arithmetical form.
John von Neumann: grasped it at once, pressed Gödel after the session, and on 20 November 1930 wrote from Berlin announcing the unprovability of consistency, three days after 1931 had been received by the journal.
Rudolf Carnap: had been told before Königsberg (at the Café Reichsrat, 26 August) but still found the result hard to understand months later; his Königsberg remarks show no grasp of it.
Kurt Reidemeister: followed Gödel with a few summarizing questions; no discussion of the announcement is recorded.
Hans Reichenbach: his conference summary in Die Naturwissenschaften did not mention Gödel at all.
W. V. Quine (1979): completeness was "a welcome reassurance"; incompleteness "an upset of firm preconceptions and a crisis in the philosophy of mathematics".
2 days between Gödel's public announcements of completeness (6 September) and incompleteness (7 September).
14 May 1930: earlier talk on completeness at Menger's colloquium (15th meeting).
1931 did not appear in Erkenntnis, officially as too technical, though Dawson suspects Gödel's attitude to the Circle also played a part.
Gödel reviews the three manifestoes
Carnap: the logicist's way (1932e)
- Two theses: (1) every mathematical notion is explicitly definable from logical ones; (2) every theorem is deducible from logical principles. Illustrated with natural and real numbers.
- Infinity and choice are existential, so not logical, but needed in proofs. Carnap's fix, following Russell: add them as hypotheses to the theorems that need them.
- The essential difficulty is impredicative definition. Russell's ramified types avoid apparent circularity but cannot treat the reals without reducibility, "today generally regarded as inadmissible". Carnap drops ramification, arguing impredicative definitions are not circular. He rejects Ramsey's justification as resting on "conceptual absolutism (Platonism)".
- Carnap's alternative: read "every hereditary property belonging to zero belongs to n" not extensionally ("every single one", numerical generality) but as "it logically follows that the property belongs to n" (specific generality, terms from Felix Kaufmann). Paradoxes expressible in logical symbols are already blocked by simple type theory, as Ramsey showed.
Heyting: the intuitionist's way (1932f)
- Mathematics as a function of the intellect: no objective existence independent of thought. Hence no pure existence proofs and no excluded middle where the decision cannot actually be made.
- Brouwer's real numbers and choice sequences: a choice sequence stands not for an individual real but for the totality of possible reals (or a subset, if a rule restricts choice). Sketch of the theorem: if a whole number is assigned to every real, all reals get the same number (continuity).
- Propositions vs assertions: a proposition expresses an expectation (intention); an assertion is its fulfilment. "C is rational" expects integers a, b with C = a/b. Excluded middle would require a general decision method. "p holds" and "p is provable" are different intentions with the same assertion; their negations differ, so Heyting concludes a proof that a question is undecidable in principle is entirely possible.
Von Neumann: the formalist's way (1932g)
- Goal: vindicate classical mathematics while taking intuitionist doubts seriously; the formalist agrees transfinite inference is contentually suspect.
- The move: treat classical inference not as contentual thinking but as a "formula game" whose formulas and moves are finitary objects. Formalism takes over the logicists' description of classical procedure.
- Justifying the game: every verifiable numerical formula derivable in the game must be correct when calculated. That is exactly consistency, to be proved by intuitionistically unobjectionable means. So far consistency had been shown only for restricted subsystems.
- Gödel's dry closing line: the lecture "characterizes the state of affairs at the time of the Königsberg conference"; the impossibility of consistency proofs by means weaker than those formalized in the system "is not yet taken into account".
Logicism (Carnap): mathematics = logic; problem: impredicativity, axioms of infinity and choice. Gödel's result: no single system captures all arithmetical truth, so "derivable from logic" depends on which system.
Intuitionism (Heyting): mathematics = mental construction; undecidability in principle is possible. Gödel's result: formal undecidability is proved constructively.
Formalism (von Neumann): mathematics = formula game justified by finitary consistency. Gödel's result: consistency is not provable inside the system, and consistency does not ensure Σ⁰₁-soundness.
Testing versus proving consistency. Gödel's Königsberg point maps onto model risk practice: showing that a model or rule set never contradicts itself does not show its outputs on real cases are correct. Consistency checks are necessary hygiene, but validation against ground truth from outside the system is a separate obligation.
Reviews of 1931: Hilbert's ω-Rule and Five Other Books
Gödel's first six reviews (1931b to g) range from Peano's axioms to Greek mathematics, but one matters historically. Reviewing Hilbert's "Die Grundlegung der elementaren Zahlenlehre", Gödel describes Hilbert's new semi-infinitary rule, an early form of the ω-rule, introduced to recover completeness for number theory. Solomon Feferman's note asks whether Hilbert was reacting to Gödel and concludes the evidence is equivocal, but that the rule trades a precisely defined formal system for one built on the vague notion of "finitary proof", the step Gödel privately told Carnap compromised Hilbert's program.
Neder 1931: on the construction of arithmetic (1931b)
Ludwig Neder improves Peano's axioms in two ways and argues two theses about number extensions.
- Successor as a relation. Replace the function "the successor of" by the relation "x follows immediately upon y", to separate the existence and uniqueness claims hidden in "the successor".
- Independence of his axioms is proved. Reflexivity, symmetry and transitivity of identity (his second primitive) are derived, not postulated.
- Thesis 1 (partly Russell's): extend number systems by constructing an entirely new domain containing an isomorphic copy of the old one, not by adjoining "new" numbers.
- Thesis 2: introduce negatives only after fractions and irrationals, partly because cuts in the positive rationals are simpler.
- Reals à la Capelli (1897): a real is a pair M₁/M₂ of non-empty sets of rationals with every element of M₁ ≤ every element of M₂ and, for each δ > 0, elements a ∈ M₁, b ∈ M₂ with b − a < δ. Neder derives the arithmetic of non-negative reals in full.
Hilbert 1931: the foundation of elementary number theory (1931c)
Feferman's note: did Gödel provoke the rule?
The timeline. Gödel announced incompleteness at Königsberg (7 September 1930); Hilbert gave his famous "Naturerkennen und Logik" address immediately afterwards at the main assembly. Bernays (Hilbert's assistant since 1917) wrote to Gödel on 24 December 1930 asking for galleys, having heard from Courant and Schur of surprising results, and on 18 January 1931 called them "a considerable step forward" and described Hilbert's new paper, based on a December 1930 Hamburg talk. A follow-up (Hilbert 1931a) was presented to the Göttingen Academy on 17 July 1931. Neither paper mentions Gödel. Gödel and Hilbert never corresponded and never met.
Bernays 1935: Hilbert had already given up the original completeness problem before Gödel's results were known, and turned to the ideas of 1931.
Bernays to Constance Reid, 1966: Bernays had voiced doubts about completeness of number theory; Hilbert was "angry", and angry again at Gödel's results, then responded "in a positive way" with the new rule. (Curiously, Bernays himself had conjectured completeness in a 1930 paper.)
Feferman: the two accounts "do not quite jibe". Bernays's other memories describe "violent arguments" rooted in Hilbert's conflict between resisting Kronecker's restrictions and suspecting Kronecker "had probably been right", so that he fought Kronecker "with his own weapon of finiteness".
What Hilbert proposed
Hilbert's completeness goals for number theory (from his 1928 Bologna problems)
- (C1) Every statement shown consistent with the system is provable in it.
- (C2) If a statement is shown consistent, the same cannot be shown for its negation.
The new rule (Hilbert 1931): if a quantifier-free A(x) has been shown (finitarily) to be a correct numerical formula for every particular numeral z, then (x)A(x) may be taken as a new premise. Call the extended system Z*, where Z is first-order Peano arithmetic with primitive recursive definitions.
- Consistency claimed for Z* by extending Ackermann (1924) and von Neumann (1927), with no details.
- Completeness for universal statements. If (x)A(x) is consistent with Z*, each instance A(z) is correct (else ¬A(z), being a correct numerical formula, is provable and contradicts (x)A(x)), so the rule gives (x)A(x): C1 holds. C2 then follows from consistency.
- Not for existential ones. C2 is trivial for (Ex)A(x), but C1 is not shown, and indeed fails by 1931 if Z* sits inside an ω-consistent formal system.
Two weaknesses Feferman exposes. (1) The Ackermann–von Neumann proofs established consistency only for a weak subsystem Z₀ with restricted induction (noted by Bernays 1935), so Hilbert's argument works only for the correspondingly weakened Z₀*; it is "cheap" once consistency is granted. (2) The rule depends on the vague concept of finitary proof, replacing a combinatorially exact system with an imprecise one. Gödel told Carnap (memo of 21 May 1931) he saw this as compromising Hilbert's program; in print he politely called it a "substantial supplement".
Gödel's review reports: besides the formalist standpoint and historical remarks, the lecture adds a rule "structurally of an entirely new kind", sketches its consistency, and yields Theorems (1) and (2) for (x)A(x) with A containing no other variable, and at least (2) for (Ex)A(x).
The ω-rule and its descendants
1927: Tarski considers a frankly infinitary rule in a lecture (published 1933).
1931: Hilbert's finitarily restricted rule; Bernays mentions a version in his letter of 18 January.
1934 to 1935: Carnap's rule DC2, hence "Carnap's rule" in Rosser 1937.
1937: Rosser studies the formalized ω-rule (idea credited to Kleene): infer (x)A(x) when Z proves that every instance is provable. The result is still recursively axiomatizable, so incomplete, even after finite iteration.
1962: Feferman and Feferman–Spector iterate it into the recursive transfinite: completeness or incompleteness depends on the path chosen through the ordinal notations.
The full ω-rule (from A(0), A(1), A(2), … infer ∀x A(x), with infinitely many premises) does yield a complete theory of arithmetic, but its proofs are infinite trees, so it is no longer a formal system in Gödel's 1963 sense. Every attempt to keep proofs finite brings incompleteness back. That trade-off, not any single rule, is the lasting lesson of 1931c.
Four shorter reviews
Betsch 1926, Fictions in mathematics (1931d). Prize-winning, mostly historical. On genuine fictions (contradictory but expedient assumptions) the answer is always no, and all of Vaihinger's claims are shown erroneous. Whether unreal fictions (assumptions not matching reality) occur depends on one's foundational stance; conventionalism and Mill-style empiricism allow them the widest scope. Fictions as tentative assumptions or provisional definitions play a large role in history.
Becker 1930, On modal logic (1931e). Starts from C. I. Lewis's strict implication (primitives and, not, impossible), where iterating "not" and "impossible" yields infinitely many irreducible modalities that cannot be linearly ordered by strength. Becker adds axioms to get a system with a linear ordering and arrives at three calculi for different kinds of necessity. Gödel's criticism: formally unobjectionable but with essential gaps: no proof the systems differ from each other and from Lewis's, nor that the six or ten basic modalities cannot be reduced further; the link to Brouwer–Heyting logic is doubtful. (Two years later Gödel himself gave the right connection, Chapter 17.)
Hasse and Scholz 1928, The foundational crisis in Greek mathematics (1931f). The Pythagoreans first used infinitely small magnitudes to handle irrationals; Zeno's paradoxes (the arrow) showed this untenable, precipitating a foundational crisis and the rigorous theory of Eudoxus. Zeno appears as an early champion of rigour, compared to Weierstrass. An appendix criticizes Spengler. Gödel praises its clarity, sharpness and terse suggestiveness.
Von Juhos 1930, The problem of mathematical probability (1931g). Purges probability of empirical impurities: physical draws become "arbitrary acts of choice", absolutely random and not spatio-temporal. Probability = (arguments making a propositional function true) / (arguments making it meaningful); the physical notion is relegated to an appendix. Gödel reports without comment.
The ω-rule today. Infinitary proof theory made the ω-rule central: Schütte used it for cut-elimination in ordinal analysis of PA (giving ε₀ again), and Buchholz's operator-controlled derivations extended the method to strong subsystems of analysis. The question of Hilbert's motives is still read through Bernays's two conflicting accounts; the edition of Hilbert's lectures on the foundations of arithmetic and logic, 1917 to 1933 (Ewald and Sieg, 2013) gives much more context but no decisive answer.
On the Intuitionistic Propositional Calculus
Asked by Hahn whether Heyting's intuitionistic propositional logic H could be a many-valued logic with finitely many truth values, Gödel answered no in less than a page, and in passing opened a field. His formulas Fₙ and matrices Sₙ produce an infinite descending chain of logics strictly between classical logic and H, the first result in the theory of intermediate logics. A. S. Troelstra's note identifies the chain and its later axiomatizations; Gödel's last line states, without proof, the disjunction property.
The two theorems
H is the system of Heyting 1930; A is the ordinary (classical) propositional calculus.
Theorem I. There is no realization with finitely many elements (truth values, with designated values) in which exactly the formulas provable in H are satisfied.
Theorem II. Infinitely many systems lie between H and A: there is a monotonically decreasing sequence of systems, each containing H and contained in A.
The proof
The formulas. Let Fₙ = ⋁₁≤ᵢ<ₖ≤ₙ (aᵢ ≡ aₖ): the disjunction, over all pairs among n propositional variables, of their equivalences.
Fₙ holds in every small realization. In any realization with fewer than n elements that satisfies all theorems of H, some two of a₁, …, aₙ receive the same value e (pigeonhole). The corresponding disjunct becomes e ≡ e ∨ b, which is designated because a ≡ a ∨ b is provable in H.
The matrices Sₙ. Elements {1, 2, …, n}, designated element 1 (so 1 is "true" and n is "false"):
- a ∨ b = min(a, b), a ∧ b = max(a, b);
- a ⊃ b = 1 if a ≥ b, and a ⊃ b = b if a < b;
- ¬a = n for a ≠ n, and ¬n = 1.
What Sₙ does. It satisfies all theorems of H and Fₙ₊₁ (and every Fᵢ with larger index), but not Fₙ (or any Fᵢ with smaller index): assign the n variables the n distinct values.
S₃ in full (1 = true, 3 = false; rows a, columns b for a ⊃ b):
| a ⊃ b | b = 1 | b = 2 | b = 3 | ¬a |
|---|---|---|---|---|
| a = 1 | 1 | 2 | 3 | 3 |
| a = 2 | 1 | 1 | 3 | 3 |
| a = 3 | 1 | 1 | 1 | 1 |
The middle value 2 is "not false but not proved": ¬2 = 3 and ¬¬2 = 1, so ¬¬a ⊃ a fails at a = 2 (value 2), and a ∨ ¬a at a = 2 is min(2, 3) = 2, undesignated. Excluded middle and double negation elimination both fail, as intuitionism requires.
- Consequence for Theorem I. A finite characteristic matrix with fewer than n elements would satisfy Fₙ, so Fₙ would be provable in H. But Sₙ shows no Fₙ is provable in H. So no finite matrix works.
- Consequence for Theorem II. The logics of S₂, S₃, S₄, … are strictly decreasing (each separated from the next by an Fᵢ), all containing H and contained in A. S₂ is classical logic.
- Disjunction property. The note ends: A ∨ B is provable in H only if A or B is. Gödel gave no proof; Gentzen 1935 supplied one (via cut elimination).
Troelstra's commentary
- Lₙ = the formulas valid on the n-element linearly ordered Heyting algebra (Gödel's Sₙ). The chain is L₂ = A ⊋ L₃ ⊋ L₄ ⊋ … ⊋ H.
- Dummett's LC (1959): the logic of the linear Heyting algebra of order type ω, axiomatized by adding to H the linearity axiom (P → Q) ∨ (Q → P), equivalently (A ∨ B) ↔ [((A → B) → B) ∧ ((B → A) → A)].
- Thomas (1962) gave finite axiomatizations: Lₙ = LC + Fₙ₊₁.
- Theorem I follows from Theorem II, since a logic characterized by a finite matrix and containing H has only finitely many proper strengthenings.
- Gödel's result is the first contribution to intermediate logics, now an extensive field (surveys: Hosoi and Ono 1973, Minari 1983), studied mainly for their algebraic theories.
Names that grew out of this one page
- Gödel–Dummett logic (LC, G): linear intuitionistic logic; also the t-norm fuzzy logic with min as conjunction.
- Gödel algebras / Gödel chains: the Sₙ and their limit on [0, 1].
- Gödel's n-valued logics Gₙ: the finite-valued Lₙ.
- Disjunction property: a hallmark of constructive systems, later the existence property for intuitionistic arithmetic.
Fuzzy and graded reasoning. The Gödel t-norm (truth of A ∧ B = the minimum, implication as in Sₙ) is one of the three basic fuzzy logics alongside Łukasiewicz and product logic, and appears in fuzzy rule engines and scoring systems where a chain of conditions should be only as strong as its weakest link, a natural semantics for risk flags that must all hold.
Since then. Kripke semantics (1965) made intermediate logics geometric: LC is the logic of linear Kripke frames. Hájek's Metamathematics of Fuzzy Logic (1998) placed Gödel logic among the t-norm logics; first-order Gödel logics over sets of truth values in [0, 1] were classified by Baaz, Preining and Zach (2000s), with axiomatizability depending on the topology of the truth-value set.
A Special Case of the Decision Problem
Warren Goldfarb's note covers Gödel's work on the decision problem for prefix classes of first-order logic. In 1932a Gödel shows that formulas with prefix ∃…∃∀∀∃…∃ are decidable, and in 1933i that ∀∀∀∃…∃ is a reduction class and that the decidable class has the finite model property. Two adjacent universal quantifiers are not enough for undecidability; three are. Goldfarb then tells the story of Gödel's closing claim about identity, which he himself refuted in 1983.
Background: decidable classes and reduction classes
A class of formulas is decidable if an effective procedure determines satisfiability for each member. Before the mid-1930s, decidability was shown by procedures evidently effective, but undecidability could not be proved; instead one showed reduction classes, classes to which the decision problem for all of first-order logic reduces. Their undecidability followed once Church (1936a) and Turing (1937) showed full first-order logic undecidable. Gödel's classes are prefix classes of closed prenex formulas in pure quantification theory (predicate letters of any degree, no constants, functions or identity).
| Prefix class | Status | Who |
|---|---|---|
| ∃…∃∀…∀ | Decidable | Bernays–Schönfinkel 1928 |
| ∃…∃∀∃…∃ | Decidable | Ackermann 1928a |
| ∃…∃∀∀∃…∃ | Decidable, finite model property | Gödel 1932a, 1933i; Kalmár 1933; Schütte 1934 |
| ∀…∀∃…∃ | Reduction class | Skolem 1920 |
| ∀∀∀∃…∃ | Reduction class | Gödel 1933i |
| ∀∀∀∃ | Undecidable | Surányi 1950 |
| ∀∃∀ | Undecidable | Kahr, Moore and Wang 1962 |
| ∀∀∃ with identity | Undecidable | Goldfarb 1984 |
The complete classification (pure logic, no identity): a prefix class is undecidable if and only if it allows either two universal quantifiers separated by an existential (∀∃∀) or three universal quantifiers governing an existential (∀∀∀∃). Everything else is decidable. Gödel's two results supply the upper edge of the decidable side and a near-optimal reduction class.
The decidability proof (1932a)
The method grows out of the completeness proof of 1930.
- Reduce ∃…∃∀∀∃…∃ to ∀x₁∀x₂∃x₃…∃xₙ F, eliminating the leading existentials in the known way (Ackermann 1928a).
- Tables. Assume first only binary predicates φ₁, …, φₛ. Let A be the atomic formulas φᵢ(x₁, x₁) and B all φᵢ(xₚ, xq) with p, q ∈ {1, 2}. A truth assignment to A (an 𝔄ᵢ) describes one element; an assignment to B (a 𝔅ⱼ) describes an ordered pair. A model yields the finite sets 𝔓 of 1-element types and 𝔔 of pair types that occur.
- Two conditions. (I) For any two 1-types in 𝔓 there is a pair type in 𝔔 extending both. (II) For every pair type in 𝔔 there are n − 2 further elements and values making F(x₁, …, xₙ) true while all 1-types and pair types used stay in 𝔓 and 𝔔.
- Decision. There are finitely many candidate pairs (𝔓, 𝔔), so one can check whether any satisfies I and II. If none does, F is unsatisfiable. If one does, F is satisfiable: build a model in stages, at each stage adding n − 2 new witness elements for every pair, using II to fix their relations to the pair and I to fix relations to everything else.
- Higher-arity predicates: use all ways of placing x₁, x₂ in the argument places.
The lacuna. In the inductive construction Gödel overlooked the case where x and y take the same value. He noted it himself in 1933i. Kalmár handles it by an extra closure condition; Gödel instead passes to a formula G = ∀x∀y∃z̄ J equivalent to F, the prenex form of ∀x∀y(∃z̄ H ∧ ∃z̄ H′) with H′ = H[y := x], so that only distinct pairs need witnesses. The Gödel–Kalmár–Schütte criterion is the same in essence for all three authors; Gödel states it compactly in his review of Kalmár (1933l).
The reduction proof (1933i)
Starting from Skolem's ∀…∀∃…∃ form, Gödel cuts the universal quantifiers in stages: conjoin clauses asserting a one-one correlation of elements with pairs of elements, so one universal quantifier ranging over "pair-elements" can do the work of two. Encoding the correlation itself needs three universal quantifiers, so the count cannot go below three. Goldfarb: an adaptation of Löwenheim's 1915 pairing trick (showing binary predicates form a reduction class), with care to minimize new quantifiers.
Finite controllability
A class is finitely controllable if every satisfiable member has a finite model; such a class is decidable (search models and proofs in parallel). Gödel's main theorem in 1933i: ∀∀∃…∃ is finitely controllable, hence (Ackermann's reduction preserves finite satisfiability) so is ∃…∃∀∀∃…∃. Combined with the classification, every decidable prefix class has the finite model property.
How the finite model is built. From a set T of (n+2)-tables meeting the criterion, construct a finite universe and correlate several distinct n-tuples with each pair of distinct elements, each tuple tagged by a table in T. Two combinatorial lemmas ensure: no tuple is correlated with both (a, b) and (c, a); and if (c₁, …, cₙ) serves (a, b), then neither a nor b occurs in tuples serving pairs (cⱼ, d) or (cⱼ, cₖ). This allows a consistent definition of all relations, so the cᵢ act as witnesses for every pair. Later proofs (Schütte 1934a, Ackermann 1954, Dreben 1962, Dreben–Goldfarb 1979) reuse Gödel's devices, especially Lemma 2; Gurevich and Shelah (1983) first avoided them. Lemma 1 was generalized by Aanderaa–Goldfarb 1974, Lemma 2 by Erdős 1963.
The identity story
1933: last sentence of 1933i: the same method shows finite controllability with identity, no details given.
Mid-1960s: Stål Aanderaa finds examples where the Gödel–Kalmár–Schütte criterion fails for formulas with "=".
24 May 1966: Burton Dreben writes to Gödel. 19 July 1966: Gödel has no notes, but recalls adding an equivalence relation leaving the predicates invariant: "No difficulty arose."
3 April 1970: Dana Scott relays Gödel's recollection: rewrite with "sharp" quantifiers (each variable's value distinct from earlier ones); Gödel claims his method applies unchanged.
Early 1970s: the problem is recognized as open.
1983: Goldfarb proves the ∀∀∃ class with identity undecidable (1984, 1984a).
Gödel's error, diagnosed. Goldfarb builds a satisfiable ∀∀∃ formula with identity forcing every model to contain an ω-sequence on which a binary relation is successor: no finite model, and enough structure to encode halting problems. His guess at the slip: Gödel's lacuna fix replaced F by G using the equivalence of F with ∀x∀y(x ≠ y → ∃z̄ J); with "=" present one must replace x = y by falsity in J, after which F is no longer equivalent to ∀x∀y∃z̄ J. In the identity-free case Gödel never argued step (1), probably thinking it obvious, and in 1933 simply overlooked the difference that "=" makes.
The Gödel class today. The full map of decidable fragments is in Börger, Grädel and Gurevich, The Classical Decision Problem (1997). Gödel's class without identity is NEXPTIME-complete. Its descendants matter in practice: the Bernays–Schönfinkel class (EPR) is the basis of several SMT and verification tools, and the two-variable fragment and guarded fragment (both with finite model property) underpin description logics used in ontologies and data governance.
Choosing a logic for rules. When regulatory or business rules are encoded in logic, the prefix of the quantifiers decides whether a solver always terminates. Gödel's boundary is a concrete warning: rules of the form "for every pair of entities there exists a witness" stay decidable; add a third universally quantified entity, or equality in the wrong place, and decidability can be lost.
On Completeness and Consistency
Dated 22 January 1931, this short note restates both incompleteness theorems for first-order Peano arithmetic with primitive recursive definitions (Z), removing the dependence on type theory, and gives the clearest early statement of the hierarchy of systems. Each step up in type proves the consistency of the previous system and decides its Gödel sentence, but brings new undecidable arithmetical sentences; in set theory, axioms of infinity play the role of higher types. A 1966 remark shows Gödel worrying about exactly what "S contains Z" must mean for the second theorem to hold.
The system Z and the theorems
Z = Peano axioms + the schema of definition by recursion on one variable + first-order logic; only number variables, so induction is a rule of inference.
The two theorems of 1932b
- Incompleteness. Any formal system S with finitely many axioms, whose only rules are substitution and implication, and which contains Z, is incomplete (has undecidable propositions, in particular propositions of Z), provided S is ω-consistent: no property F with (Ex)F(x) and all of ¬F(0), ¬F(1), … provable.
- Consistency. In every such S, the proposition that S is consistent (more precisely, its arithmetical equivalent under a one-one numbering of formulas) is unprovable.
Generalization. Both hold for infinitely many axioms and other rules, provided that, numbering formulas by length and then lexicographically, the class of axiom numbers and the one-step consequence relation are definable and decidable in Z (for every tuple, Z proves R or ¬R). Gödel adds: "At present no decidable number-theoretic relation is known that is not definable and decidable already in Z."
That last remark is an early, informal version of the conviction that entscheidungsdefinit in Z captures all effectively decidable relations, five years before Church's thesis. Feferman notes (Chapter 1) that being numeralwise decidable in a formal system did turn out to be equivalent to general recursiveness.
The hierarchy
- Ladder of types. Enlarge Z by variables for classes of numbers, classes of classes, and so on, with comprehension axioms; the sequence continues into the transfinite. The consistency (ω-consistency) of each system is provable in every later one.
- Undecidables move but never vanish. The Gödel sentence of a system becomes decidable in a higher one; the higher system gets new ones by the same construction. All are number-theoretic (expressible in Z) but decidable only higher, for example in analysis.
- Set theory. In a type-free foundation, axioms of cardinality replace type extensions: certain arithmetical statements undecidable in Z are decided by an axiom asserting sets of cardinality greater than every αₙ, with α₀ = ℵ₀, αₙ₊₁ = 2αₙ.
1931. System P (types + Peano); ω-consistency; recursive axiom classes; footnote 48a on transfinite types as "the true reason".
1932b. First-order Z; finitely many axioms or Z-decidable axiom sets; explicit ladder of types and cardinality axioms; the claim that Z already decides every known decidable relation.
Gödel's 1966 remark
Footnote 1 defined "S contains T" as: everything expressible (provable) in T is expressible (provable) in S. On 18 May 1966 Gödel added:
- The definition is imprecise, and the straightforward precise version is not sufficient for the second theorem. The right condition: S is an extension of T, every formula, axiom and rule of T being one of S.
- Translations are dangerous. If Z is merely recursively one-one translatable into S with provability preserved, then the consistency even of very strong S may be provable in S, and even in primitive recursive arithmetic.
- What stays unprovable is "outer" consistency: that the equational calculus (substituting primitive recursive terms, replacing equals) applied to equations provable in S yields only correct numerical equations. This is what Hilbert's program actually needs to justify transfinite axioms, and for usual systems it is trivially equivalent to consistency.
- Weaker bases suffice: Theorem 1 and this result hold for primitive recursive arithmetic (Z without quantifiers), and, suitably worded, for any recursive translation of p.r. Equations into S under ω-consistency or outer consistency.
Why the remark matters. The second incompleteness theorem is intensional: it depends on how consistency is expressed as well as on which sentence is true. Feferman 1960 made this precise with consistency statements built from non-standard axiom enumerations (Rosser-style or "Feferman consistency") that a theory can prove. Gödel's 1966 caveat anticipates this: the theorem is robust only for natural representations of the system.
Assurance ladders. The type hierarchy is the formal version of a familiar governance pattern: a control can be validated by a stronger layer above it, never by itself, and the top layer is always taken on trust. Designing "who validates the validator" chains for AI models has the same shape, and Gödel's result says the chain cannot close on itself.
A Property of the Realizations of the Propositional Calculus
Answering a letter from Karl Menger, Gödel proves that any algebraic "realization" of the classical propositional calculus, of any cardinality, can be split into a true and a false class that behave exactly like truth and falsity. W. V. Quine's note calls it "a pioneer venture in the metalogic of indenumerable notation": a transfinite version of Lindenbaum's extension lemma, from which propositional compactness for uncountable languages follows immediately. Gödel did not draw that consequence, and Maltsev rediscovered the territory in 1936.
The theorem
Setting. A set 𝔖 of objects p, q, r, … closed under a unary operation ~p and a binary operation p ⊃ q. A proper subset 𝔗 satisfies:
- (I) for all p, q, r in 𝔖, three objects lie in 𝔗 (Łukasiewicz's axioms): (a) (~p ⊃ p) ⊃ p; (b) p ⊃ (~p ⊃ q); (c) (p ⊃ q) ⊃ [(q ⊃ r) ⊃ (p ⊃ r)].
- (II) if p and p ⊃ q are in 𝔗, so is q (modus ponens).
Theorem. There is a partition 𝔖 = 𝔚 + 𝔉 into disjoint classes with 𝔗 ⊆ 𝔚 such that (a) of p and ~p, exactly one is in 𝔚; (b) p ⊃ q is in 𝔉 iff p ∈ 𝔚 and q ∈ 𝔉.
In words: an arbitrary realization of the axioms, however large and however unlike formulas (no "letters", no minimal units), carries a two-valued valuation extending its theorems. 𝔚 and 𝔉 "behave exactly like the classes of the true and the false propositions".
The proof
Transfinite construction. Well-order 𝔖. Define subsets 𝔗α:
- 𝔗₀ = 𝔗.
- At a limit α, 𝔗α = ⋃β<α 𝔗β.
- At a successor: let a be the first element of 𝔖 such that neither a nor ~a is in 𝔗α; set 𝔗α+1 = {x : (a ⊃ x) ∈ 𝔗α}. If no such a exists, 𝔗α+1 = 𝔗α.
By transfinite induction: (A) each 𝔗α satisfies I and II; (B) 𝔗α ⊆ 𝔗β for α < β; (C) x and ~x are never both in 𝔗α. Let ν be the first ordinal with 𝔗ν = 𝔗ν+1, and put 𝔚 = 𝔗ν, 𝔉 = 𝔖 − 𝔗ν.
Sample step (B): since x ⊃ (a ⊃ x) is in 𝔗α (by A), x ∈ 𝔗α gives (a ⊃ x) ∈ 𝔗α, i.e. X ∈ 𝔗α+1. Condition (b) uses that x ⊃ (y ⊃ x), ~y ⊃ (y ⊃ x) and ~x ⊃ [y ⊃ ~(y ⊃ x)] lie in 𝔗ν.
- Transfinite methods are essential (Feferman, Chapter 1): the well-ordering of an arbitrary set uses the axiom of choice.
- Compared with Lindenbaum (reported in Tarski 1930): Lindenbaum extended any consistent set of first-order sentences to a complete one, for countable languages. Gödel's result is limited to propositional logic but works for indenumerably many formulas.
- What Gödel missed. With no extra work it gives compactness for propositional logic of any cardinality. Neither this nor any awareness of Lindenbaum's result appears in the note.
- Maltsev 1936, apparently unaware of Gödel's paper, proved compactness for uncountable first-order languages and showed its algebraic applications. Henkin 1949 built his completeness proof on the Lindenbaum–Gödel extension idea.
Lindenbaum (c. 1928, via Tarski 1930). First-order, countable; enumerate sentences and add each one consistent with what you have.
Gödel 1932c. Propositional, any cardinality; well-order and add, at each stage, the first undecided element as a hypothesis (keep everything it implies).
In modern terms the theorem says every Boolean algebra (indeed every proper filter of the Lindenbaum algebra) extends to an ultrafilter: the Boolean prime ideal theorem. It is now known to be strictly weaker than the axiom of choice (Halpern–Lévy 1971) yet equivalent to the compactness theorem and to completeness for first-order logic in arbitrary languages. Gödel's note is one of its earliest proofs.
Reviews of 1932: Skolem, Church's Early λ-System, Kalmár and Others
The 1932 reviews show Gödel reading across decision procedures, lattice theory, Boolean algebra, and foundations. Two stand out historically. His review of Alonzo Church's 1932 postulates records the system from which, as Kleene's note explains, the λ-calculus and λ-definability were extracted, before the full system collapsed into paradox. And the Kalmár review reports a reduction class close to his own decision-problem work. Gödel's harshest line of the year is for Dingler, whose claimed consistency proof "could at best demonstrate the trivial fact that the elementary rules of computation are consistent".
Skolem 1931: decidable arithmetic of the rationals (1932d)
- Language. Propositional functions built with not, or, and, all, exists from relations A = B and A < B, where A and B arise by iterating addition, multiplication by a rational and "next smaller whole number". Variables range over the rationals (or any domain with these operations satisfying simple conditions).
- Decision procedure by quantifier elimination: every such propositional function is equivalent to an "elementary" one without quantifiers.
- Relativity of well-ordering. Skolem builds an ordered set and a domain of functions, containing the ordering and closed under the logical operations, in which the set is well-ordered (every definable class has a least element), while classes outside the domain lack least elements: well-ordering and "inductive number" depend on the available definitions.
- Second procedure for statements built from constituents a·x₁α₁ · x₂α₂ · … · xₙαₙ = b over the positive integers, extending to integers of any algebraic number field.
Klein 1931 and 1932: abstract connectives and lattices (1932h, 1932j)
Fritz Klein's two papers, as Gödel summarizes them
- 1931: domains with a ∪ b and a ∩ b obeying the class-calculus axioms; complementation as a one-one symmetric mapping interchanging ∪ and ∩. Realizations: classes, propositions, max/min, gcd/lcm. Unique prime decomposition where it exists.
- Characteristic mappings into an Abelian group with {a ∪ b} = {a} + {b} − {a ∩ b}. Examples: number of elements of finite sets; sum and number of divisors (with ∩ = gcd, ∪ = lcm, group operation multiplication). Generalized to n variables, it gives the sieve of Eratosthenes and similar inclusion–exclusion sieves.
- 1932: a "lattice" has commutative, associative ∪ and ∩ with a ∪ b = a·≡·a ∩ b = b and a ∪ a = a. If ∩ distributes over ∪, a unit e exists for ∪, and every element has finitely many parts, then each element has at most one representation a = p₁ ∪ … ∪ pₙ as a join of primary elements over distinct prime elements; with a further decomposability assumption, existence follows too. Independence of the assumptions is studied.
Hoensbroech 1931: content and extension (1932i)
Following a remark of Bolzano, if increasing the content of a notion means adjoining constituents without destroying their connection, then extension need not shrink as content grows: "blue or red" has more content than "blue". The paper classifies kinds of increase (conjunction, disjunction, negation, substitution of a name, adding quantifiers) by their effect on extension.
Church 1932: postulates for the foundation of logic (1932k)
Kleene's note on the λ-system
How λ-definability was born. Church (1932) wanted logic free of Russell's types, avoiding paradox by weakening reductio ad absurdum. He found a modified Russell paradox and revised the system (1933). Both versions used λxM, the function whose value at x is M. At the end of 1933 Church suggested developing the positive integers inside the system. Kleene (work of 1932 to 1933, published 1934 and 1935, using Rosser) took this up with the λ-operator alone, separate from the descriptive operator ι and the rest: the origin of (Church–Kleene) λ-definability.
- Collapse. The full 1933 system was inconsistent: Kleene and Rosser (1935) derived a form of Richard's paradox. Kleene calls the restricted generality operator Π "primarily the villain".
- Rescue. Church and Rosser (1936) proved the λ-calculus alone consistent. Church 1935 sketched a transfinite hierarchy of consistent systems that might yield "a metamathematical proof of the freedom from contradiction of elementary number theory"; the idea was not pursued.
- Gödel's three Church reviews (1932k, 1934e, 1936b) are reportorial.
Gödel's review
- Aim: a formal system for logic and mathematics avoiding the antinomies without type theory or axiomatic set theory, by restricting excluded middle. The set of all sets not containing themselves can be formed, but it cannot be proved either to contain itself or not; "a hypothesis implying a contradiction is false" does not hold generally.
- Open questions (Church's own): whether all antinomies (e.g. Burali-Forti) are avoided and whether the system suffices for mathematics.
- Size: 8 primitive symbols, 35 axioms, 5 rules.
- Restricted generality. Since propositional functions may be neither true nor false for some arguments, "for all" is a two-place operator Π(a, b): for all x with a(x), b(x). No free variables. Substitution and implication merge into one rule: from F(a) and Π(F, G) infer G(a). Derived result: if (∃x)F(x) is provable and G follows from F(x), then Π(F, G) is provable, and G itself if x is not free in G.
A failed logic that became a programming language. The λ-calculus survived because Kleene and Rosser separated the computational core from the logical superstructure that produced the paradox. Every functional language, and the typed λ-calculi behind proof assistants such as Lean and Coq, descend from that move. The same discipline applies to enterprise platforms: isolate the part that computes from the part that asserts, and verify each on its own terms.
Kalmár 1932: a reduction class (1932l)
László Kalmár reduces the decision problem to formulas with prefix (Ex₁)…(Exₘ₋₁)(y₁)(y₂)(Exₘ)(y₃)(y₄)…(yₙ): for each A there is B of this form with A satisfiable (or finitely satisfiable) iff B is. If B is satisfiable in a domain I, so is A; if A is satisfiable in I, then B is in a larger domain I′ whose cardinality is easily computed. B has a few more predicate variables, but only binary ones if A has only binary ones.
Huntington 1932: axioms for the algebra of logic (1932m)
Two new axiom systems for the calculus of classes. The first takes a + b and a′ as primitive and needs, besides commutativity and associativity of +, only
a + a = a and (a′ + b′)′ + (a′ + b)′ = a.
The second uses a ⊃ b (= a′ + b) alone and needs much more complicated axioms. Independence and equivalence with earlier systems are deferred. B. A. Bernstein's 1931 system needs one more axiom to give the ordinary calculus of classes.
Huntington's third axiom and the Robbins problem. Huntington's equation (a′ + b′)′ + (a′ + b)′ = a led Herbert Robbins to ask whether it could be replaced by ((a + b)′ + (a + b′)′)′ = a. The question resisted human effort for sixty years and was settled yes in 1996 by William McCune's automated prover EQP, one of the first major open problems solved by machine. This review sits at the root of that story.
Skolem 1932: symmetric general solutions (1932n)
For a Boolean equation f{aₑ, xₖ} = 0 with coefficients aₑ and unknowns xₖ, a general solution xᵢ = gᵢ{aₑ, uₖ} is symmetric for a permutation group G if each permutation in G is matched by one of the parameters uᵢ leaving the solution system invariant, and normal if moreover it permutes the uᵢ as it permutes the xᵢ.
- Constant coefficients: a symmetric general solution exists iff the equation stays solvable when unknowns are equated within each orbit of G.
- With coefficients: expand in constituents A of the aₑ; the condition is that each constant-coefficient equation fA{xₖ} = 0 has a symmetric solution for the subgroup GA. In general one must add ΣB = 0 over the failing constituents. Normal solvability has the same conditions. A corollary gives when a solution can be symmetric in the unknowns and their complements.
Dingler 1931: philosophy of logic and arithmetic (1932o)
Hugo Dingler opposes unanalysable "basic capabilities" (active logic) to the passive logic of calculi, roughly Hilbert's split between metamathematics and mathematics, and applies them to arithmetic. He offers a formal system supposed to give Hilbert's consistency proof.
Gödel's verdict: the system "in truth, could at best demonstrate the trivial fact that the elementary rules of computation (distributive law, and so on) are consistent". Coming months after 1931, the line is a compact statement of the gap between consistency of quantifier-free calculation (easy) and consistency of arithmetic with induction and quantifiers (impossible by elementary means).
Parry's Axioms and Independence Proofs
Two colloquium remarks from 1933, both prompted by questions in Menger's Vienna circle, both short. The first proposes a definition of "analytic implication" for William Parry's axioms, an early sketch of what is now relevance logic. The second answers Hahn: not every independence result in the propositional calculus can be proved with finite truth-table matrices; Gödel exhibits a formula independent of three axioms that every finite model of those axioms nevertheless satisfies. W. V. Quine's notes place both beside Gödel's 1932 work on intuitionistic logic.
On Parry's axioms (1933)
Parry (1933) had presented a deviant propositional calculus in which a conditional fails to be valid if its consequent contains a new letter: Quine's description of what is now called relevance logic (strictly, Parry's analytic implication).
Gödel's proposed reading. "p analytically implies q" means: q is derivable from p and the axioms of logic, and q contains no notions other than those in p. Once made precise, one should seek a completeness proof for Parry's axioms: every statement valid under this interpretation of → should be derivable.
- The discussion question. Someone, evidently Hahn, asked how many truth values Heyting's intuitionistic propositional calculus has, that is, how many non-equivalent functions of one variable. Example: p ∨ ¬p is equivalent to none of p, ¬p, ¬¬p. Gödel: "At present it is not even known whether there are finitely or infinitely many."
- Gödel's answer came within months: 1932 shows no finite set of truth values characterizes intuitionistic logic (Chapter 9). Quine notes the answer predates the publication of this remark.
Both questions are now settled. The one-variable fragment of intuitionistic logic has infinitely many non-equivalent formulas: the Rieger–Nishimura lattice (1949, 1960) lists them all, generated from p by ∨ and → in an infinite ladder. Parry's system was shown complete for a semantics of content-containment by Fine (1986), and the relevance-logic programme of Anderson and Belnap (Entailment, 1975) grew into a large field with applications in paraconsistent databases and reasoning with inconsistent information.
On independence proofs in the propositional calculus (1933a)
Hahn's question: can every independence proof for a formula of the propositional calculus be done with finite models (matrices), in the sense of Łukasiewicz and Tarski 1930? Gödel: no.
The example
Axioms, with substitution and modus ponens:
- p ⊃ p
- (p ⊃ ~~q) ⊃ (p ⊃ q)
- (~~p ⊃ ~~q) ⊃ (p ⊃ q)
Claim: the formula p ⊃ ~~p is independent of 1 to 3, yet holds in every finite normal matrix satisfying 1 to 3.
Independence by an infinite matrix. Elements: the integers ≥ 0; designated element 0; ~p = p + 1; p ⊃ q = 0 if p ≥ q, 1 if p < q. All three axioms take value 0 and modus ponens preserves 0, but p ⊃ ~~p = p ⊃ (p + 2) = 1: not designated.
No finite matrix works. Let 𝔄 be finite with designated set 𝔄*, satisfying 1 to 3 and closed under modus ponens. Since 𝔄 is finite, the sequence p, ~~p, ~⁴p, … repeats: ~²ᵏ⁻²p = ~²ⁿ⁻²p for some k < n. By axiom 1 the corresponding implication between equal elements is designated; by axiom 3, repeatedly stripping double negations, we get p ⊃ ~²⁽ⁿ⁻ᵏ⁾p ∈ 𝔄*; applying axiom 2 (n − k − 1) times reduces this to p ⊃ ~~p ∈ 𝔄*.
- A non-classical variant. Replacing ~~ by a single ~ everywhere gives a system that is not a subsystem of classical logic but is still consistent (A and ~A never both provable).
- A general invariant. For any set M of propositional formulas closed under substitution there is a least cardinal m ≤ ℵ₀ such that models with m elements (matrices satisfying exactly M) exist. For this system, and for Heyting's calculus, m = ℵ₀. The sets with m = 2 are the fragments of classical logic consisting of all tautologies expressible with one of a certain group of connectives (for example, ⊃ alone).
1932 (intuitionistic logic). No finite matrix characterizes H: some finite-matrix tautology is unprovable.
1933a (independence). No finite matrix separates p ⊃ ~~p from three axioms: finite models are too coarse to witness every independence. Both say the same thing about finite semantics: it can be incomplete for a perfectly decidable syntax.
Testing with finite models. Model checkers and property-based tests search finite structures. Gödel's example is a reminder that a specification can be consistent with a property's failure while no finite test case exhibits that failure. Bounded verification gives evidence, not proof, and some independence results only show up in infinite behaviour, such as unbounded counters or streams.
Geometry in Menger's Colloquium
Five short notes from 1933 show Gödel as a working geometer inside Karl Menger's program for a coordinate-free geometry of metric spaces. He proves a spherical embedding theorem for metric quadruples, recasts Wald's axioms for betweenness as a statement about ℝ³, shows every line-preserving bijection of the real projective plane is a collineation, and co-authors (his only joint paper) a volume-determinant criterion for surfaces. Judson Webb's note finds the logician underneath: Gödel suspected that lattice axioms could not give a complete elementary foundation for projective geometry, an incompleteness analogous to his arithmetic result, later confirmed when Pascal's theorem proved not to be any lattice identity.
Menger's program
Menger wanted to free curvature from "the complicated conceptual machinery" of classical differential geometry: coordinates, parameterizations, differentiability. His tool was n-tuples of points in compact convex metric spaces.
- Curves. By the triangle inequality any metric triple has an isometric copy in the Euclidean plane; its curvature is 1 / (radius of the circumscribed circle). The curvature at a point is the limit of the curvatures of nearby triples. Variants by Franz Alt and Gödel appear in Alt 1933.
- Surfaces are harder: use quadruples, but an isometric Euclidean quadruple may not exist, and when it does, the circumscribed sphere's radius is not obviously meaningful.
Embedding quadruples in a sphere (1933b)
Theorem (answering Laura Klanfer, 37th colloquium). A metric quadruple congruent to four points of ℝ³ but not to four points of a plane is congruent to four points on a sphere with the geodesic (great-arc) metric.
Fixed-point argument. Let T be a non-planar tetrahedron with edges a₁, …, a₆ equal to the six distances, R its circumradius. For x > 0 set aᵢ,ₓ = (2/x) sin(aᵢx/2), the chord of an arc of length aᵢ on a circle of radius 1/x (with aᵢ,ₓ → aᵢ as x → 0). Let T(x) be a tetrahedron with edges aᵢ,ₓ, if it exists, and f(x) = 1/(its circumradius) (0 if planar), so f(0) = 1/R > 0. Let a be the largest aᵢ.
Claim: some x in (0, π/a) has f(x) = x. Let x̄ be the largest number ≤ π/a such that T(x) exists on [0, x̄]; f is continuous there. If x̄ = π/a, the longest edge of T(π/a) is 2a/π, so the circumradius exceeds a/π and f(π/a) < π/a; with f(0) > 0, the intermediate value theorem gives a fixed point. If x̄ < π/a, T(x̄) must be planar (otherwise T would exist slightly beyond), so f(x̄) = 0 < x̄, again a fixed point.
At f(x) = x the tetrahedron T(x) has circumradius 1/x, its edges are chords aᵢ,ₓ, and since x < π/aᵢ its vertices on that sphere are separated by arc lengths exactly aᵢ.
Wald's betweenness as a theorem about ℝ³ (1933c)
Abraham Wald (1931, 1932) characterized Menger's metric betweenness (ab + bc = ac) by six postulates on a ternary relation, including invariance under congruence. Since congruent triples are fixed by their three distances, Gödel codes each triple by the point
(+) x = ab, y = bc, z = ac in ℝ³, landing in the region (*) x, y, z ≥ 0, (x + y − z)(x − y + z)(−x + y + z) ≥ 0.
Betweenness becomes membership in the plane x + y = z within (*), and Wald's theorem becomes:
Wald's axioms, recoded. Let M be a subset of region (*) such that
- Symmetry: (x, y, z) ∈ M ⇒ (y, x, z) ∈ M.
- Asymmetry: (x, y, z) ∈ M ⇒ (z, y, x) ∉ M.
- Transitivity-type closure: if (u, v, w) and (w, x, y) lie in M, then for every z, (u, z, y) and (v, x, z) lie in M whenever they lie in (*).
- Non-emptiness: for every z̄ > 0, some point (x, y, z̄) lies in M.
- Closedness: for every z̄ > 0, the set of (0, z̄, z̄), (z̄, 0, z̄) and all points (x, y, z̄) of M is closed.
Then M is exactly the part of the plane x + y = z inside (*). Gödel suggests the map (+) is worth studying for metric spaces in general.
Points, lattices and universal sentences (1933d)
The remark: one should study the propositions about lattices that, in normal form, contain no existential quantifiers. "Point" and "line" are definable only with existential quantifiers (a point is an element with no non-empty proper part), so they are not definable in this restricted system; Gödel cites Wernick 1929.
Menger's puzzlement, 35 years later. On 2 January 1968 Menger wrote that he did not understand the remark: "P is a point" can be defined universally (every element included in P is P or empty). Gödel replied that any proposition with "P is a point" as a hypothesis would still contain existential quantifiers in normal form, though he granted some propositions about the defined term are expressible in the restricted system.
Webb's reading: incompleteness in geometry
- Menger's "Felder" (fields) were really lattices (term from Birkhoff 1933; "Verband" from Klein 1932): a single class of elements with join and meet, inclusion as incidence, and points defined as elements with no non-empty proper parts, which finally made Euclid's definition logically usable. He aimed to avoid Hilbert's point-line-plane primitives (a new primitive per dimension) and Veblen's reliance on undefined points and set theory.
- Distributivity fails for subspaces of projective space (Korselt, then Menger and Birkhoff); the weaker modular law suffices. Webb compares the independence of distributivity, established by Wernick 1929, to the independence of the parallel postulate.
- All lattice laws are universal; complementation has a mixed prefix. So Gödel's suggestion leads to modular lattices.
- Birkhoff (1935) and Menger (1936) proved every complemented modular lattice is a product of a finite Boolean algebra and finitely many projective geometries: the axioms are "in one sense complete". Birkhoff credits Gödel with the sharper question: are all laws of combination of projective manifolds derivable by ordinary inference? Gödel's caution: every finite field is commutative, yet commutativity fails without finiteness.
Gödel's suspicion was right. Hilbert (1899) had shown Pascal's theorem is equivalent to commutativity of the coordinate field and does not follow from the projective axioms without continuity (nor, in the plane, from Desargues). Schützenberger (1945) expressed Desargues as a lattice identity, but Pascal's theorem is not equivalent to any lattice identity. So the law needed to coordinatize the projective plane is not a consequence of the lattice axioms. Webb's parallel: categoricity of second-order arithmetic does not give a complete first-order theory, and categoricity of projective geometry with continuity does not give a complete elementary lattice foundation.
Line-preserving maps are collineations (1933g)
Theorem. Every one-to-one map φ of the real projective plane E into itself that carries lines to lines is a collineation.
For each conic, its conic-section neighbourhood is the set of points p such that every line through p meets the conic in exactly two points (the conic's interior). These neighbourhoods form an unboundedly fine covering system of E in Menger's sense (for each point and neighbourhood, a smaller open member contains the point). A conic is generated by two projectively related pencils of lines; φ maps perspective pencils to perspective pencils, so it maps conics to conics and hence neighbourhoods to neighbourhoods. So φ preserves the covering system, is continuous, and by the fundamental theorem of projective geometry is a collineation.
Volume determinants and surfaces (1933h, with Wald)
Gödel's only joint paper, with Abraham Wald, from a discussion with Menger. To make precise that Riemannian spaces are locally Euclidean ("Euclidean geometry holds for infinitesimally adjacent points"), use the volume determinant (Cayley–Menger form)
D(p₁, p₂, p₃, p₄) = | 0 1 ; 1 (pᵢpⱼ)² |, i, j = 1 to 4.
- Menger characterized the plane among metric spaces as complete, convex, outwardly convex, with D = 0 for every quadruple.
- For surfaces, D should tend to 0 strongly as quadruples converge. With Sₙ the sum of the n-th powers of the six distances: if F ⊂ ℝ³ has a C² parametrization x(u, v), y(u, v), z(u, v) with a non-vanishing Jacobian (say ∂(x, y)/∂(u, v)) at p₀, then for any four sequences converging to p₀,
lim D(p₁ⁿ, p₂ⁿ, p₃ⁿ, p₄ⁿ) / S₆(p₁ⁿ, p₂ⁿ, p₃ⁿ, p₄ⁿ) = 0.
Menger and Blumenthal (1970) relate this to Wald's eventual solution of the problem of characterizing Gaussian surfaces metrically.
| Note | Question | Gödel's answer |
|---|---|---|
| 1933b | When does a metric quadruple sit on a sphere? | Whenever it embeds non-coplanarly in ℝ³ (geodesic metric) |
| 1933c | Can Wald's betweenness axioms be simplified? | Recode triples as points of ℝ³: a theorem about a region |
| 1933d | Which lattice notions are universal? | Point and line are not; study purely universal theories |
| 1933g | Are line-preserving bijections collineations? | Yes, via conic neighbourhoods and continuity |
| 1933h | How to express local flatness of surfaces? | D / S₆ → 0 for converging quadruples |
Where these ideas went. Menger's metric approach grew into distance geometry (Blumenthal 1953), now used in molecular conformation from NMR distances and in sensor-network localization, where Cayley–Menger determinants test embeddability. Metric notions of curvature without coordinates reappeared in Alexandrov spaces and in Ricci curvature for graphs and metric measure spaces (Ollivier; Lott–Villani–Sturm), active in geometric analysis and in graph machine learning.
On Intuitionistic Arithmetic and Number Theory
Presented to Menger's colloquium on 28 June 1932, this paper turns the usual picture upside down. Intuitionistic logic looks weaker than classical logic, but under the right translation classical arithmetic sits inside intuitionistic arithmetic. Gödel's negative translation shows that every theorem of classical number theory, suitably reread, is an intuitionistic theorem, so classical arithmetic is exactly as consistent as intuitionistic arithmetic. A. S. Troelstra's note traces the anticipation by Kolmogorov, the parallel discovery by Gentzen and Bernays, and the translation's long afterlife in proof theory.
Propositional warm-up
Read Heyting's connectives as their classical namesakes and H ⊊ A: intuitionistic logic is a proper subsystem of classical. But with a different correlation, A sits inside H.
The (∧, ¬) fragment. A classical tautology built from ∧ and ¬ alone has the form ¬A₁ ∧ … ∧ ¬Aₙ (up to equivalence), and each ¬Aᵢ is then a tautology. By Glivenko (1929), H ⊢ ¬A iff A ⊢ ¬A: classically valid negations are intuitionistically provable. So the conjunction is provable in H.
The translation. Map classical connectives to intuitionistic ones by
- ¬p ↦ ¬p, p ∧ q ↦ p ∧ q,
- p ∨ q ↦ ¬(¬p ∧ ¬q),
- p ⊃ q ↦ ¬(p ∧ ¬q).
Then every classically valid formula, translated, holds in H.
Gödel notes (footnote 4) that Glivenko's propositional result itself does not extend to number theory; the translation does.
The arithmetic system
Classical arithmetic Z is Herbrand's 1931 system, with non-logical axiom groups:
Herbrand's axiom groups plus Gödel's logical groups
- A: equality and successor.
- B: all instances of induction.
- C: defining axioms for functions fᵢ, computing values for all arguments, with uniqueness established finitistically; includes all primitive recursive definitions.
- D: all finitistically provable purely universal (Π⁰₁) statements.
- E (Gödel): substitution instances of propositional tautologies.
- F (Gödel): (x)F(x) → F(Z) for numerical expressions Z.
- G (Gödel): equality substitution axioms.
Rules: modus ponens; from A → B infer A → (x)B if x is not free in A. Language: ~, →, ∨, ·, number variables, universal quantifiers only, =, 0, x + 1, function signs fᵢ.
Troelstra: Z is not quite a formal system in the modern sense, since Groups C and D depend on what is finitistically established; modern PA and HA use just A, B and defining axioms, and C, D are inessential to the result.
H′ is the intuitionistic counterpart: Heyting's 1930a formalization of intuitionistic mathematics, extended with number variables x′, y′ (defined via membership in N), the function definitions of Group C (recursion is "unobjectionable for intuitionism") and the statements of Group D.
The theorem and its proof
Theorem I. If A is provable in Herbrand's system Z, its translation A′ is provable in H′. The translation: variables x ↦ x′, function signs and = unchanged, 0 ↦ 1, x + 1 ↦ seq′x, connectives as above, and (x)A ↦ (x′)A′. (∃ is defined in Z; as a primitive it would go to ¬∀x¬A′.)
Lemma 1 (stability). For every translated formula A′, ¬¬A′ ⊃ A′ is provable in H′. Induction:
- Atomic: numerical equations are decidable intuitionistically (A′ ∨ ¬A′), so stable.
- ∧: stability of A′ and B′ gives stability of A′ ∧ B′.
- ¬: ¬¬¬A′ ⊃ ¬A′ holds generally.
- ∀: from ¬¬A′ ⊃ A′ get (x′)(¬¬A′ ⊃ A′), and use ¬¬(x′)A′ ⊃ (x′)¬¬A′.
The translated language uses only ∧, ¬, ∀ (the "negative fragment"), and every formula there is stable.
Lemma 2. For translated A′, B′: ¬(A′ ∧ ¬B′) behaves like implication, (A′ ⊃ B′) ≡ ¬(A′ ∧ ¬B′), using Lemma 1 on B′.
Axioms. Group A translates to Heyting's theorems 10.2 to 10.26; induction (B) follows from Heyting 10.14 with ⊃ replaced by ¬(· ∧ ¬·); C and D were adjoined; E follows from the propositional result; F and G from Heyting 6.3, 5.4, 6.26, 10.01. Rules I and II preserve provability of translations by Lemma 2.
Gödel's conclusions
- Intuitionistic arithmetic is "only apparently narrower" than classical; it contains it under a deviant interpretation.
- Why: the intuitionist's ban on turning a negated universal into an existential has no effect, because absurdity can be applied to universal propositions, producing formulas formally identical to classical ones.
- Where intuitionism really restricts: only in analysis and set theory, and there because of the rejection of impredicative definitions, not of excluded middle.
- Consistency: the result is an intuitionistic consistency proof for classical arithmetic, but not finitary in Herbrand's and Hilbert's sense.
Why this shook the Hilbert school. According to Bernays (1967), the paper showed there were alternatives to finitism as a basis for metamathematics, and that intuitionism goes beyond finitism: Z sits inside H′, yet a finitist justification of Z is hard. Heyting's explanation of the connectives uses abstract notions like "construction", well beyond finite combinatorics.
Troelstra's commentary
A small slip with zero. Z starts the numbers at 0, Heyting's system at 1, and Gödel translates 0 ↦ 1. Then a Group C axiom such as x + 0 = x becomes x + 1 = x, which is false. The easy repair: let the numbers in H′ start at 0 as well. Gödel seems to have overlooked this.
| Version | Translation idea | Status |
|---|---|---|
| Kolmogorov 1925 | Put ¬¬ before every subformula | Full details for →, ¬ only; quantifiers sketched; written in Russian, unknown to Gödel |
| Gödel 1933e | ∨, → and ∃ via ¬, ∧, ∀; atoms unchanged in arithmetic | Full arithmetic |
| Gentzen, Bernays 1933 | Same result, translation preserving → | Gentzen withdrew his paper on learning of Gödel's |
| Kuroda 1951 | ¬¬ after each ∀ and in front of the whole formula | Most economical |
- All variants are intuitionistically equivalent, hence "the negative translation": translated formulas avoid the positive operators ∨ and ∃.
- Another reading: H′ is Z enriched with two new constructive operators ∨ and ∃ besides the classical ones; but double negation elimination fails for formulas with the new operators.
- Extensions. Second-order arithmetic with full impredicative comprehension (Kreisel 1968), type theory (Myhill 1974), set theory (Friedman 1973, Powell 1975); in pure logic atoms must become ¬¬P. These seem to clash with Gödel's claim that intuitionism restricts analysis and set theory, but Gödel's intuitionism excluded impredicativity; the extensions are at best "formally intuitionistic".
- Choice is the limit. With function variables and countable choice, the translation of ∀x∃y A(x, y) → ∃α∀x A(x, αx) is not derivable from choice itself; this obstacle drove the search for bar recursion in extending Gödel's 1958 Dialectica interpretation to analysis.
- Semantics. In a Heyting algebra H, the regular elements ¬¬a form a Boolean algebra R(H), and ‖F‖ in R(H) equals ‖F′‖ in H: the translation is the passage from intuitionistic to Boolean-valued models, generalized to elementary toposes.
The translation in current use. Negative translations combined with Friedman's A-translation (1978) show that classical and intuitionistic arithmetic prove the same Π⁰₂ sentences, so classical proofs of "for every x there is y" contain algorithms. This drives proof mining (Kohlenbach), which extracts explicit rates of convergence from classical proofs in analysis, and double-negation (CPS) translations in programming languages, where Gödel's translation reappears as continuation-passing style (Griffin 1990: classical logic corresponds to control operators like call/cc).
Same theorems, different promises. The negative translation keeps every classical theorem but changes what an existential claim promises: ¬∀¬ asserts "a witness cannot be ruled out", not "here is a witness". In AI explanations and audit trails the distinction is practical: a model that shows a fraud case cannot be excluded has proved something weaker than one that exhibits the transaction. Ask which kind of existence a system is asserting.
An Interpretation of the Intuitionistic Propositional Calculus
In one page Gödel reads intuitionistic logic as classical logic plus a provability operator B, axiomatized by what is now the modal logic S4. Every intuitionistic theorem translates into an S4 theorem, and Gödel conjectured the converse, proved by McKinsey and Tarski in 1948. His last remark is sharper still: B cannot mean "provable in a given formal system", because B(Bp → p) would then let a system prove its own consistency, contradicting the second incompleteness theorem. Troelstra's note follows the result to Kripke semantics and Solovay's provability logic.
The system 𝔖 and the translation
Gödel's system 𝔖 ("p is provable" = Bp)
- Bp → p
- Bp → (B(p → q) → Bq)
- Bp → BBp
plus classical propositional logic for →, ~, ., ∨ and the necessitation rule: from A infer BA.
Translation of Heyting's connectives: ¬p ↦ ~Bp; p ⊃ q ↦ Bp → Bq; p ∨ q ↦ Bp ∨ Bq; p ∧ q ↦ p . Q. Alternatives that work equally well: ¬p ↦ B~Bp, p ∧ q ↦ Bp . Bq.
- Soundness. The translation of every formula provable in Heyting's calculus is derivable in 𝔖.
- Excluded middle fails. The translation of p ∨ ¬p (Bp ∨ B~Bp) is not derivable, nor in general any BP ∨ BQ unless BP or BQ is already provable: a modal disjunction property (proved by McKinsey–Tarski 1948), which yields the disjunction property of intuitionistic logic.
- Conjecture. "Presumably a formula holds in Heyting's calculus if and only if its translation is provable in 𝔖."
- Lewis and Becker. 𝔖 is equivalent to Lewis's strict implication (with Np for Bp, see Parry 1933a) plus Becker's axiom Np < NNp: that is, S4. Gödel's axiomatization was new and led to simpler presentations of modal systems (Lemmon 1977).
- Kolmogorov (1932) gave a different interpretation of IPC, as a calculus of problems, without a precise formalism; Gödel cites it in a footnote.
The incompleteness remark. If B meant "provable in S" for a system S containing arithmetic, then B(Bp → p) would hold; taking p = (0 ≠ 0): B(0 ≠ 0) → 0 ≠ 0, hence ~B(0 ≠ 0), provable in S. That is S proves its own consistency, impossible by 1931. So 𝔖's "provable" must mean provable by any correct means, not provability in a fixed system.
Troelstra's commentary: what was proved later
1948: McKinsey and Tarski prove Gödel's conjecture, IPC ⊢ F iff S4 ⊢ F′, by algebraic (topological) semantics; they also give the variant p⁻ = □p with S4 ⊢ F⁻ ↔ □(F′).
1954, 1958: extension to predicate logic (IQC into QS4) by Maehara (cut elimination) and Rasiowa–Sikorski (algebraic), with (∀xA)′ = ∀xA′ and (∃xA)′ = ∃x□A′.
1963: Hacking: S4 can be weakened to S3.
1965: Kripke semantics for intuitionistic logic, built on Gödel's translation once QS4 semantics existed.
1967: Grzegorczyk's axiom strengthens S4 to Grz, still faithful for IPC (□(□(p → □p) → p) → p).
1968: Prawitz and Malmnäs: proof via normalization of natural deduction.
1976: Solovay: the modal logic of provability in PA is GL (G).
1978: Goldblatt: with (□A)° = A° ∧ □A°, S4 ⊢ F iff GL ⊢ F°, giving a formal-provability interpretation of IPC.
1978, 1984: Mints, Goodman: extension to HA and modal PA.
Solovay's provability logic GL
- All classical tautologies, modus ponens, necessitation (from F infer □F).
- K: □(F → G) → (□F → □G).
- Löb's axiom L: □(□F → F) → □F, valid for provability because of Löb's theorem (1955).
Solovay (1976): F is a theorem of GL iff PA ⊢ Φ(F) for every arithmetical interpretation Φ with □ read as ProvPA. GL proves □p → □□p but not □p → p: exactly the "reflection" Gödel's remark rules out.
S4 (Gödel 1933). B = provability by any correct means. Has Bp → p (reflection). Interprets intuitionistic logic. Semantics: reflexive transitive Kripke frames.
GL (Solovay 1976). □ = provability in PA. Lacks □p → p; has Löb's axiom. Captures exactly what PA can prove about its own provability. Semantics: transitive, conversely well-founded frames.
Why Gödel cared. Troelstra suggests the appeal was an interpretation of intuitionistic logic meaningful from a non-intuitionistic standpoint, as Kolmogorov's was. Heyting's reading of "true" as "provable" points toward it, though Heyting does not prepare one for a classical base logic.
Live research. Artemov's Logic of Proofs (1995 to 2001) realized Gödel's informal B by explicit proof terms (t : A, "t is a proof of A"), finally giving S4 and IPC the provability semantics Gödel sought; in 1938 Gödel had sketched a similar idea in a lecture published only in Volume III. Justification logic grew from it. Provability logic itself now has machine-checked foundations: Solovay's theorem has been formalized as part of the Lean 4 FormalizedFormalLogic project (arXiv write-up, 2026).
Modal operators in AI governance. Systems that reason about what an agent knows, may do, or can prove (epistemic logics for multi-agent systems, deontic logics for policy) are descendants of this note. Gödel's two operators teach a design choice: decide whether "verified" means verified by this system (GL-like: no self-reflection) or verified by some correct method (S4-like). Confusing them produces exactly the self-certification paradox in his last paragraph.
On the Decision Problem for the Functional Calculus of Logic
The full paper behind Chapter 10. Gödel proves that every satisfiable formula of the form ∀x∀y∃z₁…∃zₙ 𝔄 has a finite model (Theorem I), and that the class with three universal quantifiers and only binary predicates is a reduction class for all of first-order logic (Theorem III). The finite-model construction is the paper's real achievement: a domain of quadruples, a Paley tournament on seven points (quadratic residues mod 7) and a pair-colouring lemma together guarantee that witnesses for different pairs never collide. His Kalmár review (1933l) states the decision criterion in four conditions.
Setting and the repaired normal form
Gödel recalls 1932a and Kalmár's detailed treatment by the same method, and Bernays, Schönfinkel and Ackermann's result that one-∀ formulas, if satisfiable, are finitely satisfiable. The aim: prove this for two universal quantifiers, and show three is already the general case.
- Formula (1): ∀x₁∀x₂∃y₁…∃yₘ 𝔄 (leading existentials reduce away, Kalmár 1933, p. 478).
- Models and tables. A model over 𝔍 assigns functions (relations) to the predicate variables on domain 𝔍. A k-th-order table is a model over {1, …, k}; there are finitely many. For elements a₁, …, aₖ, [M | a₁, …, aₖ] is the table recording how the aᵢ are related in M.
- The lacuna repaired. (1) implies the formula with x₂ := x₁; their conjunction has normal form ∀x₁∀x₂∃y₁…∃yₙ 𝔅 (4), with n = 2m. For (4) it suffices to find witnesses for distinct pairs a₁ ≠ a₂. Footnote 4: this passage was "inadvertently not presented" in 1932a but is necessary for the stated conditions to suffice.
The criterion
From a model M of (4), form 𝔓 = all first-order tables [M | a] and 𝔔 = all second-order tables [M | a, b]. They satisfy:
Conditions I and II
- (I) For any R, S in 𝔓 there is T in 𝔔 with [T | 1] = R and [T | 2] = S: any two 1-types can sit together as a pair.
- (II) For every R in 𝔔 there is a table T of order n + 2 with [T | 1, 2] = R, 𝔅T(1, 2, …, n + 2) true, all [T | i] in 𝔓 and all [T | i, k] in 𝔔: every pair type has a witness configuration that stays within the known types.
Theorem I: if (4) is satisfiable, it is satisfiable in a finite domain. It follows from Theorem II: if non-empty 𝔓, 𝔔 satisfy I and II, then (4) has a finite model. Since tables are finitely many, this is also a decision procedure.
Two combinatorial lemmas
Lemma 1 (colouring ordered pairs). For a k-element set, let χ(k) be the least number of classes into which the ordered pairs [a, b] (a ≠ b) can be split so that pairs [a, b], [c, d] in the same class always have a ≠ d and b ≠ c (no pair "chains" into another). Then χ(2k) ≤ χ(k) + 2: colour each half with χ(k) colours, then use one new colour for all pairs from half 1 to half 2 and one for half 2 to half 1. With χ(2) = 2, iteration gives χ(2ᵏ) ≤ 2k, so χ grows only logarithmically, and for any n there is a size where χ(m) · constant ≤ m.
Lemma 2 (a seven-point tournament). On {0, …, 6} let ρ(x, y) hold iff x ≠ y and x − y is a quadratic residue mod 7 (x − y ∈ {1, 2, 4, −3, −5, −6}). Then (1) ρ is asymmetric, and (2) any two x, y have a common z with ρ(z, x) and ρ(z, y): solve x + u² ≡ y + v² (mod 7) with u, v ≢ 0 by factoring (u + v)(u − v) ≡ y − x. Footnote: no such relation exists on fewer than 7 elements. Let σ(x, y) be the least such z.
Why seven. Lemma 2 is the Paley tournament on 7 vertices: a "king" for every pair. Gödel needs a tag that each witness inherits from both members of its pair, yet can never point back in both directions. This little object from number theory is what makes the witness sets of different pairs provably disjoint (fact (11) below). Erdős (1963) later generalized it to tournaments where every k vertices have a common dominator, the start of Schütte's tournament problem.
Building the finite model
- Choices. For each R, S in 𝔓 fix a pair table 𝔖(R, S) from I; for each R in 𝔔 fix a witness table 𝔫(R) of order n + 2 from II.
- Domain. With q = |𝔔|, choose L with 7·n·q·χ(7L) ≤ 7L (possible by Lemma 1). The domain 𝔍 is the set of quadruples [x, y, z, u] with x < 7, y < χ(7L), z < n, u in 𝔔: at most 7L elements. Colour the ordered pairs of 𝔍 by Lemma 1; Z(a, b) is the colour of [a, b].
- E-complexes. An (n+2)-tuple a with a₁ ≠ a₂ is an E-complex if for some T in 𝔔 the witness positions aᵢ₊₂ are the quadruples [σ(a₁,₁, a₂,₁), Z(a₁, a₂), i, T]: the first coordinate comes from the tournament applied to the pair's first coordinates, the second is the pair's colour, the third the witness index, the fourth the pair type. Write A(a) = [a₁, a₂], B(a) = the n witnesses, 𝔔(a) = T. Every distinct pair and every T has an E-complex.
- Key facts. (10) Two E-complexes' witness sets are equal or disjoint. (11) By Lemma 2's asymmetry, an element cannot be a pair member of one complex and a witness of another in the conflicting pattern; so A(a) and B(a) are disjoint and every E-complex has n + 2 distinct elements. Lemma 3: if two E-complexes share enough elements (a set m meeting both witness sets), they have the same pair type and give the shared elements the same positions; the colouring from Lemma 1 rules out reversed pairs.
- Defining M. Using a fixed ordering of each k-element subset (Lemma 4: tables can be assigned independently to distinct subsets), set: (A) a witness x takes the 1-type its E-complex prescribes (else any element of 𝔓); (B) a pair inside some complex's witness set takes the prescribed pair type (else 𝔖([M|x], [M|y])); (C) larger subsets inside a complex take the prescribed table (else arbitrary). Lemma 3 makes all choices independent of which complex is used (18).
- Verification. Lemma 6: every pair of distinct elements gets a type in 𝔔. Lemma 7 (using Lemma 5, which assembles a table from its lower-dimensional parts): if [M | a₁, a₂] = 𝔔(a), then 𝔅(a₁, a₂, …, aₙ₊₂) holds. For any x ≠ y take the E-complex with pair (x, y) and type [M | x, y]: its witnesses satisfy 𝔅. So M satisfies (4) on a finite domain.
The reduction class (Theorem III)
Theorem III. Every first-order formula is equivalent (for satisfiability) to one of the form ∀x₁∀x₂∀x₃∃y₁…∃yₙ 𝔄 in which no predicate has more than two arguments.
- Binary first. By Löwenheim (1915), every formula is equivalent to a binary one; then Skolem's procedure, as used for Theorem IV of 1930, gives a distinguished normal form ∀…∀∃…∃, with an (n+m)-ary predicate replaced by an expression in binary Rᵢ.
- Lowering the universal count. For a form A with n ≥ 4 universal quantifiers, add two new binary relations R₁, R₂ with clauses (21) to (23) saying that xR₁y & xR₂z codes a one-one map from elements x to pairs [y, z]. Then one universal variable u ranging over "pair codes" replaces two of the originals: A and A′ are equisatisfiable.
- Clean-up. Conjunctions of distinguished forms stay distinguished; identity introduced along the way is eliminated by Kalmár's 1929 method or Gödel's from 1930. Iterating reduces to three universal quantifiers, the floor because the pairing clauses themselves need three.
- Final sentence: "Theorem I can also be proved, by the same method, for formulas that contain the identity sign." Chapter 10 tells how Goldfarb showed this false in 1983.
Review of Kalmár 1933 (1933l)
Gödel: Kalmár's solution for two adjacent universal quantifiers "does not differ essentially" from 1932a. After Ackermann's reduction to ∀x₁∀x₂∃x₃…∃xₙ 𝔅, Kalmár takes the set 𝔗 of n-th-order tables realized by satisfying n-tuples. It has four properties:
- (I) every T in 𝔗 makes 𝔅(T, 1, 2, …, n) true;
- (II) for T₀ in 𝔗 and positions ν ≠ ν′ there is T in 𝔗 with [T | 1, 2] = [T₀ | ν, ν′] (every realized pair can head a witness configuration);
- (III) for T₀ in 𝔗 there is T′ with [T′ | 1] = [T₀ | 1] and T′ = [T′ | 1, 1, 3, 4, …, n] (the identical-pair case, the one Gödel's 1932a missed);
- (IV) for T₁, T₂ in 𝔗 there is T with [T | 1] = [T₁ | 1] and [T | 2] = [T₂ | 1].
Existence of a non-empty such 𝔗 is also sufficient for satisfiability; finitely many tables give the decision procedure.
Two loose ends in one paper. 1933i both repairs an error (the identical-pair lacuna of 1932a, via the passage to (4)) and introduces one (the identity claim). The repair was explicit and argued; the new claim had no argument at all. Gödel's 1966 and 1970 recollections suggest he believed it routine, and Goldfarb's diagnosis is that the very trick used for the repair is what breaks with "=".
Finite model theory and descriptive complexity grew from questions like Gödel's: which first-order fragments have the finite model property, and how large must models be? The Gödel class has models of size exponential in the formula, matching its NEXPTIME satisfiability. Gödel's "types" (tables) are the ancestors of the type-based arguments now standard for the two-variable fragment (Grädel, Kolaitis and Vardi 1997, also NEXPTIME-complete).
Reviews of 1933: Kaczmarz, Lewis, and a Tribute to Hahn
Three reviews close 1933. Kaczmarz gives four axioms for arithmetic; C. I. Lewis argues for many alternative logics chosen on pragmatic grounds; and Hans Hahn's rewritten Reelle Funktionen gets the longest and warmest review Gödel ever wrote. Gödel praises Hahn's proofs as given "with a rigor and attention to detail that probably have hardly an equal in the textbooks of mathematics and are not far removed from complete formalization". Feferman reads it as homage to his teacher, who died the next year.
Kaczmarz 1932: axioms for arithmetic (1933j)
Four axioms with primitives "number" and "less than"; their independence and their equivalence with Neder's (Chapter 8) are proved.
Lewis 1932: alternative systems of logic (1933k)
C. I. Lewis's pluralism, as Gödel reports it
- Different logics exist only in the sense that one can take different primitive notions, so the valid propositions differ.
- A logic is fixed by a finite class K of properties (truth values), one property E being assertable; theorems concern truth-functional propositional functions.
- Examples: K = {true, false} gives Principia; K = {certain, certainly false, doubtful} gives Łukasiewicz's three-valued logic; K = {necessary, impossible, true but not necessary, false but not impossible} gives Lewis's strict implication.
- Interpretation of p ⊃ q in three-valued logic: no disadvantage is sustained in converting a wager on p into a wager on q (apart from degree of uncertainty).
- Analyticity: the true statements of a system follow from the meaning of its primitives, so are analytic; the infinitely many systems do not contradict one another.
- Choice among them is psychological and pragmatic, but necessary for doing logic; Lewis leans toward three-valued logic, since some propositional functions are meaningless, neither true nor false, for some arguments.
A review without comment, on a view Gödel opposed. Lewis's conventionalism (logics as pragmatically chosen, truths as analytic by meaning) is close to the Carnap line Gödel later attacked in "Is mathematics syntax of language?". He reports it neutrally. Note also that Lewis's four-valued description of strict implication is not a finite characteristic matrix: Dugundji (1940) proved no finite matrix characterizes S1 to S5, the modal analogue of Gödel's 1932 result.
Hahn 1932: Reelle Funktionen (1933m)
A completely new version of Hahn's Theorie der reellen Funktionen (1921); this first volume excludes set functions (planned for volume 2) and adds a chapter on analytic sets.
Gödel's three praises. (1) Rigour close to Principia-style formalization. (2) Economy: so many explicit theorems that proofs rarely exceed half a page. (3) Abstraction: everything stated with the fewest assumptions, as abstractly as possible. Plus richness: recent results scattered across journals appear systematically for the first time, with new proofs that will teach "something new to the specialist", especially on Baire functions.
| Ch. | Content | Highlights Gödel singles out |
|---|---|---|
| I | Abstract set theory | Cardinal and ordinal numbers, systems of sets; no background assumed |
| II | Point sets (topological and metric spaces) | Metrizability of regular separable spaces, embedding in Hilbert space; first and second category, residual sets, local versions |
| III | Continuity | Many-to-many maps; upper and lower semi-continuity; extension theorems; every absolute Gδ is homeomorphic to a complete metric space; Whyburn's proof of path-connectedness; uniform convergence; every function on a separable complete space is continuous on a dense set (not always a countable one); Hurewicz's boundedness theorem |
| IV | Borel sets and Baire functions | Abstract setting; parallel between Luzin's separation theorems and interpolation theorems; limits of class-α functions; separately continuous f(x₁, …, xₙ) gives f(x, …, x) of class ≤ n − 1, and conversely |
| V | Analytic sets | Ranges of continuous and semi-continuous functions; multiplicity of values on the Baire null space; relation to Borel sets; implicit Baire functions; Luzin sieves |
Gödel closes: no review could cover the material even approximately, and its richness makes it "eminently suitable as a reference tool".
Why this review matters biographically. Hahn was Gödel's principal teacher (Chapter 1), co-founder of the Vienna Circle, and the referee who called 1931 epochal. He died on 24 July 1934. The review's stress on near-formal rigour and abstraction also mirrors what Gödel valued in his own papers. Analytic sets returned in Gödel's set theory: in 1938 he noted that V = L implies a non-measurable PCA (Σ¹₂) set of reals exists.
Descriptive set theory now. Hahn's chapters on Borel, analytic and projective sets became modern descriptive set theory, where Gödel's L and later large cardinals decide questions about projective sets: under projective determinacy (Martin–Steel 1989, from Woodin cardinals) all projective sets are Lebesgue measurable, the opposite of what holds in L.
The Princeton Lectures: On Undecidable Propositions of Formal Mathematical Systems
From February to May 1934 Gödel lectured on incompleteness at the Institute for Advanced Study; Stephen Kleene and J. Barkley Rosser took the notes, which Gödel approved and later emended for Martin Davis's 1965 reprint, adding a Postscriptum (3 June 1964). The lectures restate 1931 with cleaner tools: a second-order arithmetic, abstract conditions any system must meet, an explicit link to the Liar and to Tarski's undefinability of truth, and a Diophantine form of the undecidable sentence. They also introduce the Herbrand–Gödel general recursive functions, one of the founding definitions of computability, although in 1934 Gödel did not believe they captured all effectively computable functions. Only Turing's analysis convinced him. Kleene's note tells the story of Church's thesis from the inside.
§1 Formal systems, defined constructively
A formal mathematical system has undefined terms (symbols), formulas (finite sequences), meaningful formulas, axioms, and rules of inference defining immediate consequence. The requirement: rules and the definitions of meaningful formula and axiom must be constructive, decidable by a finite procedure. Proof, provable and complete (every closed formula or its negation provable) are defined as usual. In §6 "constructive" is replaced by the precise "recursive"; in the 1964 Postscriptum by "mechanical" in Turing's sense.
§2 Recursive (primitive recursive) functions
Gödel's bracketed note: what is called "recursive" here (except in §9) is now primitive recursive.
- Generation. From x + 1, constants and identity (projection) functions Uⁿⱼ(x₁, …, xₙ) = xⱼ, close under composition (scheme 1) and primitive recursion (scheme 2). The projections replace 1931's informal "omission of variables".
- Representing function. A relation is recursive if its representing function (0 if it holds, 1 if not) is. Recursive functions are computable by a finite procedure; recursive relations are decidable.
- Footnote 3, the famous conjecture. "The converse seems to be true if, besides recursions according to the scheme (2), recursions of other forms (e.g., with respect to two variables simultaneously) are admitted. This cannot be proved, since the notion of finite computation is not defined, but it serves as a heuristic principle." Later bracket: "now outdated; see the Postscriptum."
- Closure theorems I to III (proved in full, unlike 1931): negation via α(x) (α(0) = 1, α(x+1) = 0) and disjunction via a recursion; =, <, ≤ via truncated subtraction x ∸ y; bounded quantifiers and the bounded least-number operator via a running product π(x, y) = ρ(0, y)·ρ(1, y)·…·ρ(x, y).
§3 The formal system: second-order arithmetic
The 1934 system
- Variables: propositions p, q, r; numbers x, y, z; one-place number functions f, g, h (higher types mentioned but not used).
- Constants: 0, successor N, ~, ∨, &, →, ≡, Π (all), Σ (exists), ε (Hilbert's selection operator: εx[F(x)] is some x with F(x), if any), =, parentheses.
- Expressions of the I-st kind (terms): 0, number variables, N(A), f(A), εx(A). II-nd kind (formulas): propositional variables, A = B, connectives, and Π, Σ over all three kinds of variables.
- Three substitutions: Subst[A, x := term], Subst′[A, f := G(x)] (effectively λxG(x), with care for nested f(…f(…)…)), Subst[A, p := formula].
Axioms. A1 to A8 propositional: (p → q) → ((q → r) → (p → r)); ((~p) → p) → p; p → ((~p) → q); definitions of &, ∨, ≡ and two ≡-elimination laws. B1 to B3 identity: x = x; x = y → f(x) = f(y); (x = y) & (y = z) → z = x. C1, C2 Peano: ~(0 = N(x)); N(x) = N(y) → x = y.
Rules. 1 modus ponens; 2a, b and 3a, b move Π and Σ across implications (t not in A or B); 4a to 4c substitution of terms, of G(x) for f (Rule 4b), and of formulas for p; 4d from A → F(x) infer A → F(εx[F(x)]); 5 induction: from F(0) and F(x) → F(N(x)) infer F(x); 6 renaming bound variables.
- ε yields Σx F(x) → F(εx F(x)) (footnote 15), the essential property of ε, though not that εx F(x) is the least witness. An ε for functions would give the axiom of choice for classes of functions of integers.
- Kleene: this is full second-order arithmetic ("analysis"). Rule 4b gives full comprehension: if ΠxΣy B(x, y) is proved, let G(x) = εy B(x, y); then ΣgΠx[g(x) = G(x)], a function exists for every definable law, in particular the representing function of any formula C(x). Propositional quantifiers are eliminable via function quantifiers.
- Kleene's observation: Gödel could have noted that much weaker function existence (arithmetical comprehension without parameters, conservative over first-order arithmetic) suffices for the incompleteness proof.
§4 Gödel numbering and metamathematics as arithmetic
"For the considerations which follow, the meaning of the symbols is immaterial, and it is desirable that it be forgotten."
- Numbers 1 to 13 for the 13 constant symbols; integers > 13 ≡ 0, 1, 2 (mod 3) for propositional, number and function variables respectively.
- Sequences coded by 2k₁ · 3k₂ · … · pₙkₙ, as in 1931.
- Recursive metamathematics: x | y, Prim(x), Pr(n), n Gl x, L(x), concatenation x * y, bracketing ℰ(x), Neg(x), Imp(x, y), u Gen x, variable classes, MI(x), MII(x), M(x) (terms, formulas, meaningful formulas), a relation for each rule, Ax(x), "x is a proof", x 𝔅 y ("x proves y").
- Consistency as arithmetic: (x, y, z) ~[x 𝔅 z & y 𝔅 Neg(z)].
§5 Representation and the undecidable sentence
z₀ = 0, z₁ = N(0), z₂ = N(N(0)), … are the numerals. A formula G represents φ if G(zₘ, zₙ, …) = zφ(m, n, …) is provable for all arguments; H represents a relation R if H(z̄) is provable when R holds and ~H(z̄) when it fails.
Representing primitive recursion with function variables. Successor, constants and projections are immediate; composition is substitution. For φ defined by recursion from ψ and χ, use
K(w₁, …, wₙ) = εy Σf [f(0) = G(w₂, …) & Πx(f(N(x)) = H(x, f(x), w₂, …)) & y = f(w₁)]
"the value at w₁ of the function f satisfying the recursion equations". The function variable f carries the whole computation history, which is why a second-order system makes Theorem V almost trivial. (Bracketed remark: the detailed proof is not even needed; if some recursive function were not represented, undecidable propositions would arise anyway unless the system proved a false numerical statement.)
The sentence. Let B(u, v) represent x 𝔅 y and S(u, v) represent 𝔖(x, y), the number of the formula obtained by substituting the numeral zy for the free w in formula x. Let U(w) = Πv[~B(v, S(w, w))] and let p be its number. Then U(zₚ) has number 𝔖(p, p): it says "no v proves me".
- If U(zₚ) were provable, by some k: B(zk, S(zₚ, zₚ)) provable; but from ΠvF(v) every F(zk) follows, so ~B(zk, S(zₚ, zₚ)) too: contradiction.
- If the system is consistent, every ~B(zk, S(zₚ, zₚ)) is provable; if ~U(zₚ) were also provable the system would be contradictory "in the weaker sense" (ω-inconsistent).
Gödel notes this version follows an informal argument of Herbrand (1931) and is a little shorter than 1931's.
Second theorem. With Contrad the formula (x, y, z)[~{x 𝔅 y & z 𝔖 Neg y}] expressing consistency, the argument formalizes to ⊢ Contrad → U(zₚ). So Contrad is unprovable unless the system is contradictory.
§6 Five conditions for any system
When the argument applies
- Recursiveness: under a numbering like the above, the class of axioms and the immediate consequence relation are recursive (the precise replacement for "constructive").
- Numerals: formulas zₙ for each n, with n ↦ (number of zₙ) recursive.
- Negation and representability: a symbol ~ (or formula F(x) acting as negation) such that every recursive relation of two variables is represented by some R(v, w).
- Universal instantiation: a symbol Π (or formula G) such that from ΠvF(v) each F(zk) is provable, for recursive F.
- Freedom from contradiction in two senses: (a) never both R(zₚ, zq) and ~R(zₚ, zq); (b) never all of ~ΠvF(v), F(z₀), F(z₁), … (ω-consistency for recursive F).
Then Πv~R(v, zₚ) is undecidable. The unprovability of consistency follows under further conditions "satisfied by all systems of the type under consideration which contain a certain amount of ordinary arithmetic".
§7 The paradoxes and truth
The Epimenides on 4 May 1934. Suppose A makes, on 4 May 1934, the single statement "Every statement A makes on 4 May 1934 is false." It cannot be true, and it cannot be false (A made no other statement). Whitehead and Russell's cure, that no proposition may speak about itself, is "too drastic": Gödel's self-referential sentences are arithmetic propositions with only recursively defined functions, "undoubtedly meaningful".
- Diagonal lemma, in general form: for any metamathematical property f expressible in the system, if F(S(w, w)) has number p, then F(S(zₚ, zₚ)) says of itself that it has f. Gödel's later bracket credits Carnap 1934a with first noting this.
- The paradox resolved: A must say "false in language B", and "false statement in B" cannot be expressed in B. "The paradox can be considered as a proof that 'false statement in B' cannot be expressed in B." Brackets credit Tarski (1933a, 1944) and Carnap 1934.
- Heuristic incompleteness proof. Let α = the class of numbers of true formulas, β = provable formulas. β is expressible (ΣvB(v, zk)) but α is not, so α ≠ β; if β ⊆ α (soundness), some proposition is true but not provable, and its negation is false and unprovable. Footnote 26: precise for any system with well-defined meanings and correct axioms containing arithmetic, but gives no individual undecidable instance.
§8 Diophantine form
Theorem. There is a polynomial equation F = 0 with integer coefficients and a quantifier prefix (P) over the natural numbers such that the undecidable proposition is equivalent to (P)(F = 0). Equivalently, it has the form (x)(P)[Q = R] with Q, R polynomials with natural-number coefficients.
Two steps.
- Every recursive function is arithmetical. Successor, constants, projections, composition are easy. For recursion use β(c, d, i) = the least non-negative residue of c mod 1 + (i + 1)d, defined by z ≡ c (mod 1 + (i + 1)d) & z < (i + 1)d with x ≡ y (mod z) as (Et)[x = y + tz ∨ y = x + tz] and x ≥ y as (Et)[x = y + t]. Lemma: for any f(0), …, f(l), pick s > l and all f(i); with d = s!, the moduli 1 + s!, 1 + 2s!, …, 1 + (l + 1)s! are pairwise coprime (a common prime would divide (i − j)s!, but i − j ≤ l < s divides s!), so the Chinese remainder theorem gives c with β(c, d, i) = f(i). This is the now-standard "Gödel β-function" (the name comes from these lectures).
- Prenex polynomial normal form. Every arithmetical expression is equivalent to (P)[Q = R]: atomic formulas are already so; combine A ∨ B via (Q − R)(Q′ − R′) = 0 rewritten as QQ′ + RR′ = QR′ + RQ′, and A & B via (Q − R)² + (Q′ − R′)² = 0; push negations through the prefix (an inequality Q ≠ R becomes an existential equation). Footnote 29: over the integers, x ≥ y can use four squares (Lagrange).
- No complete theory of Diophantine analysis. The Diophantine sentence is decidable in the next higher type, which has its own undecidable one, and so on "[including transfinite iterations describable in set theory, such as occur, e.g., in the higher axioms of infinity]". So "[on the basis of the principles of proof used in mathematics today] there can be no complete theory of Diophantine analysis", not even for problems (P)[F = 0].
- Contrast with decidable fragments: Presburger (1930) decided arithmetic with + only; Skolem sketched one for × only. With both + and × no general decision method can be established.
- Footnote 29a (later): the usual axioms about all sets do not carry further, since they also hold in sets of some definite rank (Lévy 1960a); intuitionistic principles have so far proved weaker.
§9 General recursive functions
Some definitions by induction escape primitive recursion. Example (double recursion):
φ(0, y) = ψ(y); φ(x + 1, 0) = χ(x); φ(x + 1, y + 1) = φ(x, φ(x + 1, y))
which, as Ackermann (1928) showed for a similar function, is not primitive recursive. This raises "the question what one would mean by 'every recursive function'".
From Herbrand's suggestion to Gödel's definition
Herbrand (private letter, 1931): if a system of functional equations in known functions ψ₁, …, ψₖ and an unknown φ has exactly one solution for φ, then φ is recursive.
Gödel's two restrictions:
- Each equation's left side has the form φ(ψᵢ₁(x₁, …, xₙ), …, ψᵢₗ(x₁, …, xₙ)).
- For each tuple of numerals k₁, …, kₗ there is exactly one m such that φ(k₁, …, kₗ) = m is a derived equation, where derived equations come from: (1a) substituting numerals for all variables in a given equation; (1b) true equations ψᵢⱼ(k̄) = m for known functions; (2a) replacing ψᵢⱼ(k̄) by its value m in a derived equation; (2b) replacing φ(k̄) by m on the right side of a derived equation once φ(k̄) = m is derived.
Equivalently, the arguments can be ordered so that computing φ at any arguments needs φ only at earlier arguments. Result: every such function is arithmetical.
The decisive change is restriction 2. Herbrand asked only that a solution exist uniquely, a semantic condition. Gödel demanded that values be formally derivable by explicit rules, which makes the definition constructive: a computation is a derivation. Footnote 34 (bracket): Kalmár (1955) proved Herbrand's first notion not equivalent in classical mathematics; whether Herbrand's second ("computable", intuitionistically) is equivalent is "a largely epistemological question".
Kleene's note: the birth of Church's thesis
1931: Herbrand's letter to Gödel with the unique-solution idea.
1932 to 1933: λ-definability from Church and Kleene's work on Church's system (Chapter 13).
Feb to Mar 1934: Church proposes to Gödel, privately, that λ-definability captures effective calculability. Gödel is not convinced.
Spring 1934: Gödel's lectures introduce general recursiveness.
1936: Kleene proves general recursiveness ≡ λ-definability; Church publishes his thesis and the unsolvability of the Entscheidungsproblem; Kleene gives the normal form and a non-recursive Σ⁰₁ set; Rosser removes ω-consistency; Post sketches an analysis like Turing's.
1937: Turing's machines: a direct analysis of a human computer's operations. Gödel accepts.
1943, 1952: "Church's thesis" named by Kleene; Kleene's generalized incompleteness via (x)T₁(a, a, x).
1963, 1964: Gödel's notes to 1931 and Postscriptum to 1934: Turing gives the "precise and unquestionably adequate definition" of formal system.
- Footnote 3 is not Church's thesis. Gödel to Davis, 15 February 1965: the conjecture "only refers to the equivalence of 'finite (computation) procedure' and 'recursive procedure'. However, I was, at the time of these lectures, not at all convinced that my concept of recursion comprises all possible recursions; and in fact the equivalence between my definition and Kleene's in Math. Ann. 112 [1936] is not quite trivial."
- Two notions, independently arising, proved equivalent, strengthened the evidence; Church published his thesis in 1936 in terms of either.
- A new kind of undecidability. Gödel: formally undecidable propositions in a system. Church: informally undecidable predicates, no algorithm for all instances. Logicians began speaking of undecidable predicates and theories.
- Absoluteness. Gödel noted in proof of 1936a that numeralwise expressibility is the same in all systems containing elementary number theory, and in 1946 tied it to Turing computability. All the exact notions (later also Post, Markov, Smullyan) were proved equivalent; all rest on Cantor's diagonal method (1891).
- Undecidable ⇒ incomplete (Church 1936; noted by Turing and Kleene): an undecidable system has formally undecidable sentences. Not conversely: dense linear order is incomplete but decidable.
- Essential undecidability. Rosser 1936: undecidability survives consistent extensions; Tarski (1949) named such theories; Tarski, Mostowski and Robinson (1953), Undecidable Theories: interpretability transfers essential undecidability, and finitely axiomatizable essentially undecidable theories make every same-language subtheory undecidable.
- Effective inseparability. Provable and refutable sentences of PA cannot be separated by any recursive set (Kleene 1950, Smullyan 1958); Kreisel reported Gödel regarded this improvement as "very significant".
- Kleene's generalized first theorem (1943): any correct formal system formalizing a predicate P(a) yields a form (Ex)R(a, x) with R recursive; since (x)T₁(a, a, x) is not of that form, every correct system leaves some of its instances undecided. Kleene's phrase: elementary number theory offers "inexhaustible scope for ingenuity".
| Notion | Proposed by | Idea | Equivalence shown |
|---|---|---|---|
| Primitive recursive | Dedekind, Skolem, Gödel 1931 | Composition + recursion on one variable | Strictly smaller (Ackermann 1928) |
| λ-definable | Church, Kleene 1932 to 1935 | Functions as λ-terms on Church numerals | Kleene 1936 |
| General recursive | Herbrand 1931, Gödel 1934 | Values derivable from functional equations | Kleene 1936 |
| μ-recursive (normal form) | Kleene 1936 | Primitive recursion + unbounded search | Kleene 1936 |
| Turing computable | Turing 1937 (Post 1936) | Abstract human computer with tape | Turing 1937 |
| Entscheidungsdefinit in S | Gödel 1931, 1936a | Numeralwise decidable in a formal system | Absolute (1936a), Gödel 1946 |
The Postscriptum (3 June 1964)
What Turing changed, in Gödel's words
- Formal system = any mechanical procedure for producing formulas; for each there is an equivalent system in the sense of §1 if "finite procedure" means "mechanical procedure", as the concept of formal system requires: "reasoning is completely replaced by mechanical operations on formulas".
- Condition (1) of §6 becomes superfluous: provability is always (Ex) x 𝔅 y with 𝔅 primitive recursive.
- Definitive forms: "There exists no formalized theory that answers all Diophantine questions of the form (P)[F = 0]", and "There is no algorithm for deciding relations in which both + and × occur."
- Footnote 3 answered affirmatively for §9 recursiveness, equivalent to modern general recursiveness (Kleene 1936, 1952).
- Limits of formalism, not of reason: the results "do not establish any bounds for the powers of human reason, but rather for the potentialities of pure formalism in mathematics". Whether there are finite non-mechanical procedures (using abstract terms by their meaning) "has nothing whatsoever to do with" the adequacy of the definitions.
- Sharper Diophantine form (unpublished): prefix of one block of ∀ followed by one block of ∃, polynomial of degree 4.
1931. Simple type theory over Peano; Theorem V only sketched; Richard-style sentence; ω-consistency; "recursive" = primitive recursive; no notion of general computability.
1934. Second-order arithmetic with functions and ε; representation easy via function variables; five abstract conditions; Liar and truth undefinability made explicit; β-function and Diophantine normal form; general recursive functions; 1964 Postscriptum adopts Turing.
From (P)[F = 0] to Hilbert's tenth problem. Gödel's ∀…∀∃…∃ degree-4 form was overtaken by Matiyasevich (1970): every r.e. Set is Diophantine, so there is a specific polynomial whose unsolvability is true but unprovable in any given consistent system, and Hilbert's tenth problem is unsolvable. Bounds have since been pushed to small numbers of variables (Jones 1982: 9 unknowns suffice in principle for universal Diophantine sets). The Church–Turing thesis now has physical and complexity-theoretic variants (the extended thesis and quantum computing), and Kleene's T-predicate survives as the formal core of every modern proof checker: checking a proof is primitive recursive, finding one is not.
Gödel's caution about definitions. He refused to accept a definition of "computable" until it came with a conceptual analysis of what computing is (Turing's human clerk), even though the equivalent definitions already agreed. The lesson for anyone defining a term that regulation will rely on ("explainable", "high-risk", "material model change"): agreement between formalisms is evidence, but adoption should wait for an analysis of the underlying activity that makes the definition evidently adequate.
Reviews of 1934 and 1935: Skolem's Non-Standard Model and the Limits of Formalization
Ten reviews, one of them historic. Skolem (1933a, 1934) built a model of all true arithmetic that is not isomorphic to the natural numbers, using a construction Robert Vaught's note identifies as the ultrapower twenty years early. Gödel described it carefully but credited the consequence to his own incompleteness theorem. Vaught's verdict: the result follows in a few lines from Gödel's own compactness theorem, and "it seems extraordinary that Skolem and especially Gödel himself did not observe" it. The Carnap review ends with a sentence Gödel would build a philosophy on: everything mathematical is formalizable, yet no single formal system captures all of mathematics.
Skolem 1933: Ramsey's theorem and a decision problem (1934a)
- Ramsey's theorem (1929): for any n, μ, ν there is N such that if the ν-element subsets of a set of at least N elements are split into μ classes, some n-element subset has all its ν-subsets in one class. Skolem's proof is simpler and gives smaller N.
- Application (Ramsey's): the decision problem for formulas with no existential quantifiers but possibly identity. Skolem shows: for F with n universal quantifiers there is N such that F is satisfiable in a domain of ≥ N elements iff it is satisfiable on 2n − 1 individuals a₁, …, a₂ₙ₋₁ by a symmetric model, where each relation's value depends only on the order pattern (>, =, <) of the indices.
Quine 1933: a theorem in the calculus of classes (1934b)
The identity ab + ac + bc = (a + b)(a + c)(b + c) generalizes: for finite μ and ν ≤ μ, the sum of all products of ν of μ classes equals the product of all sums of μ − ν + 1 of them. Proved purely formally from Principia theorems; false for ν > μ. Quine's note explains the odd last sentence: Principia's definitions apply outside their intended range, so "meanings thus accrue to the waste cases"; "evidently I cared a little, and Gödel indulged me."
Skolem 1933a and 1934: non-standard arithmetic (1934c, 1935)
Skolem's theorem (Vaught's statement). Let 𝔑 = (N, +, ·, <), or with any further finitary operations. There is a structure 𝔑* not isomorphic to 𝔑 with the same true first-order sentences. Consequence: no axiom system in the language of arithmetic (Skolem: no finite one; Gödel: none at all) characterizes the number sequence up to isomorphism.
The construction (Gödel's summary, nearly identical to Vaught's). Let f₁, f₂, … list the definable functions N → N. Skolem's Theorem 1: there is an infinite G ⊆ N such that for any i, k, either fᵢ(n) < fₖ(n) for almost all n in G, or = for almost all, or > for almost all. Let N* be the definable functions modulo "equal for almost all n in G", with +, ·, < defined pointwise "almost everywhere on G". This 𝔑* satisfies every true sentence and contains the non-standard element given by the identity function.
In modern terms: take a non-principal ultrafilter D on N containing every set that almost includes G, form the ultrapower 𝔑N/D, and keep the elementary substructure of definable functions (equivalently, elements definable from the single parameter [identity]/D).
Gödel's review and what he missed
- Gödel devoted over a third of 1934c to describing 𝔑* and noted Skolem's papers are essentially one. 1935 (on Skolem 1934) adds Skolem's formulation: countably many propositions with only individual variables, true of an ω-sequence, cannot distinguish it from sequences of higher order type; and Skolem's unproved claim that this survives higher-type variables interpreted as in set theory.
- Gödel's claim: the non-characterizability "also follows without difficulty" from 1931. Vaught: true, but it needs completeness too (Kleene 1952): for a recursive set of truths, incompleteness plus completeness give a model where some true sentence fails, which is weaker than Skolem's (1).
The compactness argument nobody made. Add a constant c and the sentences c ≠ 1, c ≠ 1 + 1, … to all truths of 𝔑. Every finite subset has a model (interpret c as a large number), so by compactness (Gödel 1930) the whole set does, and that model is not isomorphic to 𝔑. Vaught: such applications were apparently unknown before 1936, to Gödel, Skolem and even Tarski (who in 1936 proved the class of well-orderings is not first-order axiomatizable by quantifier elimination, though compactness gives it instantly). Maltsev (1936, 1941) first published compactness applications in algebra; others exploited compactness only after World War II.
The afterlife of Skolem's model
| Year | Development | Who |
|---|---|---|
| 1948 | Partial anticipation of ultraproducts | Hewitt |
| 1955 | Ultraproducts and the fundamental theorem | Łoś |
| 1958 to 1959 | Ultraproduct theory takes off | Chang, Frayne, Keisler, Kochen, Morel, Rabin, Scott, Tarski |
| 1961 | Every model of PA has a proper elementary end extension | MacDowell and Specker, using Skolem's definability idea and a formalized Skolem Theorem 1 |
| 1976 | Generalization of the key lemma | Gaifman |
Vaught: Skolem's results "were honored then, but they look still better as time goes on". His style contrasts with Gödel's: Skolem never uses the word "definable", replacing it in each paper by a page-long discussion.
Chen 1933: axioms for real numbers (1934d)
Only an axiom system for <, the order type of the reals, differing from the usual one by dropping the countable dense subset, which loses categoricity. Chen claims it nonetheless; Gödel: "in what sense is not clear".
Church 1933: postulates for logic, second paper (1934e)
Church's 1932 system was contradictory (a modified Russell paradox); the modifications aim to block "empty" implications (antecedent always false). He develops identity, class, and the "completion" of a propositional function (extending it to the widest domain). Gödel notes that the new system is also contradictory, but this does not affect the final definition of natural numbers: n is the operation taking f to its n-th iterate f(…f(x)…), which makes primitive recursive definitions simple: m + n = {n(S)}(m), S the successor. (These are the Church numerals.)
Notcutt 1934: axioms for the theory of deduction (1934f)
Notcutt wants a propositional calculus in which "nothing is left to the intelligence of the reader", making explicit tacit rules (such as reading left to right). For ramified type theory he introduces "inter-typical variables" ranging over all types, which may never be bound if contradiction is to be avoided, and which are meant to make reducibility superfluous.
Huntington 1934: postulates for strict implication (1935a)
Thirteen independent postulates with primitives K (propositions), Q (false propositions), D (impossible propositions), × (conjunction), ′ (negation), =.
- "a ∈ D" is a contentual statement, not an element of K, so impossibility cannot be iterated: the main difference from Lewis.
- Huntington defines a contentual impossibility (what leads to contradiction) for statements built from a ∈ Q, a ∈ D; Lewis's axioms follow from his when first-degree impossibility is his axiomatic D and second-degree is the contentual notion, and conversely.
- Gödel's caveat: this does not show the systems have the same consequences, since there is no translation for impossibility of third and higher degree.
Quine's note: Huntington's system is not a modal logic (predicates, not iterable functors); even with quantifiers it could not quantify into modal contexts, and so avoids the referential opacity that "besets modal logic".
Carnap 1934: the antinomies and the incompleteness of mathematics (1935b)
Carnap's conclusion, which Gödel endorses in summary. The flaw in semantic antinomies (the Epimenides) is not self-reference (Gödel's undecidable sentences are self-referential and harmless) but the notion "true": the assumption that some 𝔚 satisfies 𝔚(A) ≡ A for every sentence A. No consistent language contains such a notion; a language can be extended by a truth predicate for its old sentences but not for all of its own. Every formal system is incomplete twice: (1) undecidable propositions; (2) undefinable notions (𝔚, or number sequences built by diagonalization). "Although everything mathematical is formalizable, it is nonetheless impossible to formalize all of mathematics in a single formal system, a fact that intuitionism has asserted all along."
- Skolem's paradox (countable models of set theory): Carnap refines the resolution: any two sets are equinumerous syntactically, in a suitable metalanguage, but not within the system.
- Gödel adds that Tarski held the same view of truth and the antinomies (1932, 1933a, 1935).
Kalmár 1934: on a theorem of Löwenheim (1935c)
A simpler proof of Löwenheim's theorem: every first-order 𝔄 has a binary 𝔅 (no predicate with more than two places) valid iff 𝔄 is, by replacing each Fλ(x₁, …, xrλ) with a formula in binary relations. Moreover, knowing in which cardinalities 𝔅 is valid settles it for 𝔄, and a proof of 𝔅 converts into a proof of 𝔄. This is the "binary first" step of Gödel's Theorem III (Chapter 18).
Non-standard models now. Models of PA are a field of their own (Kaye, Models of Peano Arithmetic, 1991; Kossak and Schmerl, 2006). Tennenbaum's theorem (1959): no countable non-standard model of PA has recursive + or ·, so the standard model is the only computable one. Robinson's non-standard analysis (1961), built on ultrapowers, has been machine-formalized and is used for infinitesimal proofs in analysis; the ultraproduct method underlies the Ax–Kochen transfer theorems and much of modern model-theoretic algebra.
Specifications cannot pin down their intended model. Skolem's theorem says even all true first-order statements about the integers admit unintended models. Enterprise data models and ontologies face the small-scale version: constraints written in first-order logic admit non-standard instances. Practical mitigations mirror the logic: closed-world assumptions, finite-domain constraints, and validation against concrete instance data, not only against axioms.
Discussion Remark on Economic Equilibrium
Gödel's only published word on economics is two sentences, spoken at the 80th session of Menger's colloquium on 6 November 1934 after Abraham Wald's talk on the equations of production. He pointed out that demand depends on income, and income on the prices of the factors of production, so a realistic equilibrium system must include them, and its solvability should be investigated. John Dawson's note places the remark in the Vienna line of work that led to modern general equilibrium theory.
The remark
"Actually, for each individual entrepreneur the demand also depends on his income, and that in turn depends on the price of the factors of production. One can formulate an appropriate system of equations and investigate whether it is solvable." Gödel, 1936
Context
- Menger's colloquium and economics. Karl Menger's father Carl Menger was a founder of the Austrian school, so mathematical economics was natural there. Gödel reportedly discussed the foundations of economics with Oskar Morgenstern, who in a 1977 interview with Axel Leijonhufvud named Gödel among the colleagues who most influenced his work.
- The chain of models (Weintraub 1983):
| Model | Idea |
|---|---|
| Walras, Cassel | Non-linear equations with demand quantities as functions of prices |
| Schlesinger 1935 (74th session, 19 March 1934) | Inverts it: demand prices as functions of quantities produced; introduces inequalities (free goods) |
| Wald 1935, 1936 | Conditions for unique solutions of Schlesinger's system; the second paper is the talk Gödel answered |
| Gödel's remark | Generalize to systems including income and factor prices |
Not a rebuke, and not straightforward. Dawson reads the remark as suggesting a generalization, not chiding Wald. But Weintraub, quoting Lionel McKenzie, notes that although Walras's own equations included factor prices, there is no obvious way to write a meaningful inverse demand system with factor prices when there is more than one consumer: individual incomes make aggregate inverse demand ill-defined.
Where the question went. The full closure Gödel asked for, with consumers' incomes determined by the values of their endowments and firms' profits, was achieved in the Arrow–Debreu (1954) and McKenzie (1954) existence proofs via fixed-point theorems (Kakutani), building on von Neumann's 1937 growth model, also presented in Menger's colloquium. Morgenstern and von Neumann's Theory of Games (1944) came from the same circle.
Closing the loop in models. Gödel's point is the general modelling rule that feedback variables must be endogenous: demand depends on income, income on prices. Banking stress-test and credit-loss models face the same issue when macro scenarios drive borrower income while lending behaviour drives the macro path; treating either side as exogenous gives a solvable system that answers the wrong question.
On the Length of Proofs; Review of Church 1935
Gödel's last contribution to Menger's colloquium (19 June 1935) states, without proof, the first speed-up theorem: passing from i-th order logic to (i+1)-th order proves new theorems and also shortens infinitely many existing proofs by more than any function computable in the weaker system. A remark added in proof observes that computability in a system is absolute, the same for all the systems Sᵢ and even transfinite ones, unlike provability or definability: an early sighting of the robustness behind Church's thesis. Rohit Parikh's note explains what was later proved and what remains open. The volume ends with Gödel's review of Church's consistent λ-system.
The theorem
Definitions and statement (1936a)
- Length of a proof in S = number of formulas in it.
- φ computable in S: for each numeral m there is a numeral n with φ(m) = n provable in S. All recursively defined functions are already computable in S₁ (classical arithmetic).
- Sᵢ = logic of i-th order over the natural numbers: variables and quantifiers for numbers, classes of numbers, classes of classes, up to type i, none higher.
Theorem. Known: some propositions of Sᵢ are provable in Sᵢ₊₁ but not in Sᵢ. Now take formulas provable in both. For each φ computable in Sᵢ, there are infinitely many formulas f such that, if k = length of a shortest proof of f in Sᵢ and l = length of a shortest proof in Sᵢ₊₁, then k > φ(l).
- Example: with φ(n) = 10⁶·n, infinitely many formulas have shortest Sᵢ-proofs over a million times longer than their shortest Sᵢ₊₁-proofs.
- Gödel's moral: going to the next higher order has the effect "not only of making provable certain propositions that were not provable before, but also of making it possible to shorten, by an extraordinary amount, infinitely many of the proofs already available".
- The sped-up formulas are arithmetical, of the same kind as his undecidable ones: (P)[Q(x₁, …, xₙ) = 0], a quantifier prefix over a Diophantine polynomial. For example, (a)(b)(Ex)(Ey)[Q(a, b, x, y) = 0] says the equation has solutions for all parameter values, each existential depending only on the preceding universals.
The remark added in proof. "A function computable in one of the systems Sᵢ, or even in a system of transfinite order, is computable already in S₁. Thus the notion 'computable' is in a certain sense 'absolute', while almost all metamathematical notions otherwise known (for example, provable, definable, and so on) quite essentially depend upon the system adopted." In 1946 Gödel tied this to Turing computability, calling it the first absolute epistemological notion.
Parikh's commentary: what has been proved
- No proof was given. Mostowski (1952) proved an analogue with length measured by Gödel number (equivalently, number of symbols); also Ehrenfeucht and Mycielski (1971) and Parikh (1971). For n > 1 with symbol length, Solomon (1981) argued via Hartmanis's (1978) complexity results.
- Lines versus symbols. With length = number of lines, the case n > 1 appears open. The difference matters: there are infinitely many proofs with k lines but finitely many with k symbols. Any r.e. Theory has some recursive axiomatization in which every theorem has a proof of at most three lines, so a lines-based result must use that familiar systems are schematic (finitely many axiom and rule schemata).
- Function or predicate symbols? It is unclear whether Gödel's + and × were function or predicate symbols (1931 §2 suggests predicates). It matters: with function symbols t = t is an axiom for any term t; with predicates it must be proved roundabout. Parikh 1973: if PA* uses ternary predicate symbols for + and ×, some sequences of formulas have proofs in S uniformly bounded in length but unbounded in PA*; Gödel's theorem for n = 1 follows, and the speed-up need not even be computable.
- Decidability of short proofs. Parikh's argument needed "does formula A have a PA*-proof of ≤ k lines?" to be decidable; for usual PA the question is open, and Goldfarb (1981) suggests a positive answer is unlikely. Statman (1981): adding an undecidable A to a schematically axiomatized T with T ∪ {¬A} having an infinite model makes even tautologies easier to prove, giving Gödel's n = 1 theorem at once. Statman (1978) studies speed-up in general.
- Name and legacy. "Speed-up" is Blum's (1967) term from complexity theory, where it became a major topic; Parikh notes the P = NP question "can itself be thought of as a speed-up question".
Lines (Gödel's measure). Natural for schematic systems; n = 1 proved (Parikh 1973, Statman 1981); n > 1 open (as of Parikh's note); sensitive to whether + and × are functions or predicates.
Symbols / Gödel numbers. Finitely many proofs of each size; robust across axiomatizations; proved for n = 1 (Mostowski 1952) and n > 1 (via Hartmanis).
Review of Church 1935: a proof of freedom from contradiction (1936b)
Church restricts his earlier (inconsistent) systems to one with three primitives: application of a function to an argument, identity, and λx abstraction.
- Consistent by finitary means, yet rich enough that every recursively defined function of any order is represented: F(n) = m is provable when m = φ(n), with numerals λfx·f(x), λfx·f(f(x)), λfx·f(f(f(x))), … (as in 1934e).
- 1 and 2 double as "false" and "true"; propositional connectives are defined as number-theoretic functions. The formula 2 is the sole axiom; all rules ("conversions") are reversible, and a formula is proved if it converts into 2.
- Universal quantification is not primitive: formulas Π with Π(F, G) provable iff G(x) is derivable from F(x) by rules other than conversions. Because every formal system is incomplete, a transfinite sequence of ever stronger rules and quantifiers can be defined; Church conjectures they match the orders of proof by induction.
Proof length is now a central field. Proof complexity (Cook and Reckhow 1979) asks whether some proof system has polynomial-size proofs of all tautologies, which holds iff NP = coNP. Speed-up results between theories are routine tools: ZFC has exponential or non-elementary speed-up over PA on some arithmetic theorems, and cut elimination can blow up proofs non-elementarily (Statman, Orevkov). In 2020s machine-assisted mathematics, the same phenomenon is practical: stronger libraries and axioms in Lean's Mathlib make many proofs dramatically shorter. Gödel's 1956 letter to von Neumann, published after this volume, asked how fast one can decide whether a formula has a proof of length n, now read as the first statement of the P vs NP question.
Stronger frameworks pay off even when they prove nothing new. Speed-up says a richer theory can make known results astronomically cheaper to establish. Architecture choices behave the same way: a stronger abstraction layer (a shared ontology, a typed data contract, a richer verification library) may not let a team prove anything it could not prove before, but it can collapse the cost of the proofs, tests and checks it already does.
Master Takeaways
Eight years of Gödel's work, read with the commentary of a dozen logicians, reduce to a small set of exact claims about what formal systems can do, plus a method for proving such claims. The method (code syntax as arithmetic, represent the coding inside the system, diagonalize) is as important as the theorems, and it is the method that every later limit result reuses.
Master takeaways
- First-order logic is complete; arithmetic is not. Valid = provable for pure logic (1929), but any consistent, recursively axiomatized system containing elementary arithmetic leaves true arithmetical sentences undecided (1931).
- No sufficiently strong consistent system proves its own consistency. The second theorem moved Hilbert's program from "prove consistency finitarily" to "find stronger but still convincing principles" (Gentzen's ε₀, Gödel's functionals).
- Truth is not definable where provability is. Provability in a system is expressible in its own arithmetic; truth is not (the Liar, Tarski). Soundness then forces a true unprovable sentence: the cleanest one-line reason for incompleteness (1934 §7).
- Arithmetization is the master technique. Gödel numbering, primitive recursive coding and the diagonal lemma turn statements about proofs into statements about numbers, the template for every later undecidability proof in logic and computing.
- Compactness, a by-product, outgrew its parent. Theorem X of 1930 became the foundation of model theory, non-standard arithmetic and analysis, though Gödel himself never used it, even when it would have given Skolem's result in three lines.
- Computability is absolute; provability is not. The functions computable in a system do not change as types are added (1936a), and Gödel accepted a definition of "mechanical procedure" only after Turing's conceptual analysis.
- Consistency is not soundness. A consistent system can prove false Σ⁰₁ sentences (add the negation of a Gödel sentence): Gödel's point at Königsberg and the reason for ω-consistency.
- ω-consistency was a convenience. Rosser (1936) needed only simple consistency; the real requirement is Σ⁰₁-soundness for one half of the theorem.
- The second theorem is intensional. It depends on how consistency is expressed (Gödel's 1966 remark, Feferman 1960); with natural proof predicates, the Löb derivability conditions make it robust.
- Undecidable sentences can be arithmetic and even Diophantine. Gödel reached a quantified polynomial equation (1931, 1934); Matiyasevich (1970) reduced it to the non-existence of solutions of a single polynomial.
- Higher types decide lower Gödel sentences but create new ones. Every rung of the type ladder (or large-cardinal axiom) proves the consistency of the rung below; the ladder never closes (1932b, 1934).
- Higher types also shorten old proofs by more than any computable function: speed-up (1936a), the seed of proof complexity and of the P vs NP question.
- Intuitionistic logic has no finite truth tables, and Gödel's matrices Sₙ generate an infinite chain of intermediate logics (1932), the start of that field.
- Classical arithmetic lives inside intuitionistic arithmetic via the negative translation (1933e): intuitionism is a genuine restriction only where impredicativity enters.
- Intuitionistic logic is a logic of provability, faithfully embedded in S4 (1933f; McKinsey–Tarski 1948), but "provable" there cannot mean provable in a fixed system: that would contradict the second theorem, as Solovay's GL later made exact.
- The decidable/undecidable frontier for prefix classes is sharp: ∃*∀∀∃* decidable with finite models, ∀∀∀∃* a reduction class (1932a, 1933i).
- Even Gödel's claims needed proofs. His unsupported extension of the decidable class to identity was false (Goldfarb 1984); his 1932a proof had a gap he repaired in 1933i.
- General recursive functions came from Herbrand's suggestion plus Gödel's demand that values be formally derivable, turning a semantic definition into a constructive one (1934).
- Finite models are too coarse for some independence proofs (1933a), and lattice axioms are too weak for a complete foundation of projective geometry (Webb on 1933d): Gödel saw incompleteness-like gaps outside arithmetic.
- Gödel misjudged the significance of some results: he credited Skolem's non-standard model to incompleteness rather than compactness, and did not draw propositional compactness from 1932c.
- Realism was Gödel's stated engine. He credited his belief in objective mathematical truth with seeing completeness where Skolem did not and incompleteness where others expected completeness; Feferman accepts the efficacy, Davis questions how early the platonism was fully formed.
- Formal limits are not limits of reason, in Gödel's own words (1964): the theorems bound pure formalism, not human insight; whether minds exceed machines is left as a disjunction, not a conclusion.
Frameworks and mental models
| Name | What it says | Use it when |
|---|---|---|
| Gödel numbering | Map symbols, formulas, proofs injectively to numbers | You need a system to reason about its own syntax |
| Diagonal lemma | For any B(v) there is C with C ↔ B(⌜C⌝) | Building self-referential statements or programs |
| Numeralwise representability | Each instance of R or ¬R is provable | Checking a system is strong enough for incompleteness |
| ω-consistency / 1-consistency | No ∃-statement provable with all instances refuted | Separating consistency from soundness |
| Löb derivability conditions | D1 to D3 on the provability predicate | Proving second-incompleteness style results |
| Compactness | Finitely satisfiable ⇒ satisfiable | Building non-standard or unexpected models |
| Basic alternative (completeness proof) | Some finite expansion is refutable, or a limit model exists | Turning search failure into a model |
| Negative translation | ∨, ∃ replaced via ¬, ∧, ∀ | Moving classical results into constructive systems |
| S4 / GL provability reading | □ as provability by any means vs in PA | Reasoning about verification and self-certification |
| Prefix classification | Quantifier pattern decides decidability | Choosing a decidable fragment for rules |
| Type ladder / reflection | Each stronger system proves consistency of the weaker | Designing layered assurance |
| Speed-up | Stronger systems shorten proofs super-computably | Deciding whether a richer framework is worth adopting |
| Church–Turing thesis | Effective = Turing computable = general recursive | Stating what any algorithm can or cannot do |
Critical lens on the whole volume. (1) Commentary dominates text. Most items are a page or two; the introductory notes carry the interpretation, and they are written by Gödel's admirers and editors, mostly in 1984 to 1986, before the Nachlass was transcribed. Claims about motives (why the dissertation's introduction was cut, whether Hilbert reacted to Gödel, when the platonism formed) rest on thin and late testimony, often Gödel's own letters decades afterwards. (2) Biography is reticent. Feferman's sketch handles Gödel's illness, his apolitical stance in 1938 to 1940 and his last years briefly and gently; Dawson's later biography and the notebooks give a fuller, less tidy picture. (3) Heroic framing. The volume sometimes underweights contemporaries: Skolem's near-completeness, Post's 1921 anticipation of incompleteness, Herbrand's and Church's roles in recursion theory, and Gentzen's and Bernays's independent negative translation are all acknowledged in the notes, but the overall arc reads as Gödel's alone. (4) Gödel's own errors are recorded honestly (the identity claim, the 1932a gap, the Skolem-review misattribution, the "degree" blemish), which is to the editors' credit. (5) Dated in places. Several "open" questions in the notes have since been settled (the lines-versus-symbols speed-up cases remain partly open; the one-variable intuitionistic fragment, Parry's completeness and the Robbins problem are closed), as the SINCE THEN boxes record.
Who's who
| Person | Role in the volume |
|---|---|
| Kurt Gödel (1906 to 1978) | Author; completeness, incompleteness, recursion, intuitionism, decision problem |
| Hans Hahn | Principal teacher; Habilitation referee; subject of the 1933 tribute |
| Karl Menger | Ran the Vienna Mathematical Colloquium; source of most of Gödel's short papers |
| David Hilbert | Program of formalization and finitary consistency; the ω-rule |
| Paul Bernays | Hilbert's collaborator; first full proof of the second theorem (1939) |
| John von Neumann | First to grasp incompleteness; found the second theorem independently |
| Thoralf Skolem | Löwenheim–Skolem, near-completeness, non-standard arithmetic |
| Jacques Herbrand | Proof-theoretic completeness; suggested recursive function definition |
| Alonzo Church | λ-calculus; Church's thesis; unsolvable Entscheidungsproblem |
| Alan Turing | Machine analysis of computation that convinced Gödel |
| Stephen Kleene, J. B. Rosser | Took the 1934 notes; λ-definability; Rosser's sentence |
| Alfred Tarski | Undefinability of truth; visited Vienna 1930 and 1935 |
| Rudolf Carnap | Logicism; diagonal lemma; Logical Syntax; Gödel's long interlocutor |
| Arend Heyting | Formalized intuitionistic logic (H) |
| Abraham Wald | Betweenness axioms; equilibrium equations; Gödel's only co-author |
| Solomon Feferman | Editor-in-chief; life and work; Hilbert-review note |
| John W. Dawson Jr. | Catalogued the Nachlass; chronology; Königsberg and 1936 notes |
| Burton Dreben, Jean van Heijenoort | Note on completeness |
| A. S. Troelstra | Notes on intuitionistic papers |
| Warren Goldfarb | Decision-problem note; refuted the identity claim |
| W. V. Quine, Judson Webb, Robert Vaught, Rohit Parikh | Notes on 1932c and 1933 remarks, geometry, Skolem reviews, length of proofs |
Connect it
- AI assurance cannot be self-contained. The second theorem and Gödel's 1933f remark show that a system rich enough to describe itself cannot certify its own reliability; independent validation layers and human oversight are structural, not optional.
- Rule engines and regulatory logic should live in decidable fragments. The prefix classification and the fate of the identity claim show how small syntactic choices decide whether a compliance checker always terminates.
- Specifications admit unintended models. Compactness and Skolem's construction explain why ontologies and data contracts in banking need instance-level testing as well as axioms.
- Proof assistants and AI provers inherit every limit here. Lean-verified AI results are checked by a primitive recursive proof predicate; finding proofs remains open-ended, and some true statements will always lie beyond any fixed library.
- Choosing stronger frameworks is an economic decision. Speed-up says richer foundations can make known results vastly cheaper to establish, a useful lens on platform and abstraction investments.
About this book
Collected Works I: Publications 1929–1936 by Kurt Gödel, 1986. 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