Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I.

Leipzig: Akademische Verlagsgesellschaft, 1931.

First edition, author’s presentation offprint, and an association copy of the first order — Paul Bernays’s own working text, annotated in pencil throughout in the years he was preparing the second volume of Grundlagen der Mathematik (1939). Gödel’s paper contains the two results that ended Hilbert’s programme to prove mathematics consistent by finitary means: first, that any sufficiently rich consistent formal system contains a true sentence the system cannot prove; second, that no such system can prove its own consistency from within. Together they are the most consequential single contribution to twentieth-century mathematical logic. Bernays, Hilbert’s chief collaborator in Göttingen and the technical executor of the formalist programme, worked through this offprint as he prepared the canonical formalised treatment of Gödel’s result, including the first complete proof of the second incompleteness theorem and the explicit statement of what are now called the derivability conditions. The marginalia run the full length of the paper — terminological glosses, reformulations of Gödel’s compressed notation, and dense pages of working derivations — and at one point, beside Gödel’s introduction of the diagonal argument on which the entire proof turns, Bernays has pencilled a cross-reference to the page of his own forthcoming volume where he performs the same diagonal step in formalised guise. Two further annotations are explicitly dated 1938, the year before the volume went to press.

Bernays (1888–1977) — Hilbert’s assistant from 1917 and, in the verdict of Wilfried Sieg and the editors of the Bernays Project at Carnegie Mellon, arguably the greatest philosopher of mathematics of the twentieth century — was among the very first readers of Gödel’s result, having received the page proofs from the author in the winter of 1930–31, months before publication. Forced from his Göttingen Privatdozentur in 1933 as a non-Aryan under the Gesetz zur Wiederherstellung des Berufsbeamtentums — the first of the Nazi racial laws — he settled at the Eidgenössische Technische Hochschule in Zürich on a precarious annual teaching contract that was renewed for over a decade and only converted to a regular Extraordinariat in 1945. Through the second half of the 1930s, at the ETH, he wrote the second volume of Grundlagen der Mathematik — the great two-volume treatise of modern proof theory, nominally jointly authored with Hilbert but, as Solomon Feferman put it in his 2012 inaugural Bernays Lectures at the ETH, due ‘entirely to Bernays’. Signed at Zürich in March 1939, Band II is the book in which Gödel’s second incompleteness theorem — sketched without full proof in the closing pages of the present paper, with a sequel promised in print that Gödel never wrote — received its first complete published proof; it also formalises Tarski’s truth-undefinability theorem and presents Rosser’s sharpening of Gödel’s first theorem. The book has never been translated into English (Russian, Moscow 1979/82; French, Paris 2001/03; bilingual German–English of Vol. I only, London 2011/13). The present offprint is the working text Bernays read while writing it.

The result had been announced to the world in compressed form not in print but in a discussion period, on the closing day of the Zweite Tagung für Erkenntnislehre der exakten Wissenschaften at Königsberg, on Sunday 7 September 1930 — a meeting at which Carnap had spoken for logicism, Heyting for intuitionism, and von Neumann for Hilbert’s formalism. Gödel, then twenty-four and only seven months past his Vienna doctorate under Hans Hahn, used the open floor to deliver in a sentence the result that ended the formalist programme. Von Neumann took him aside afterwards. Within ten weeks, working from a single suggestion he had offered Gödel in that conversation — the transformation of undecidability into a statement about integers — von Neumann had independently rederived the second incompleteness theorem and announced it in a letter to Gödel of 20 November 1930; Gödel’s letter declaring his own prior discovery crossed it in the post, and von Neumann thereafter substantially abandoned foundational research. Carnap, who had first heard the result from Gödel in the Café Reichsrat on 26 August 1930, would within four years deploy the arithmetisation technique of §2 in his Logische Syntax der Sprache (1934), the first application of Gödel-numbering outside logic proper. Jacques Herbrand, the third figure of that immediate reception, was in Berlin attending von Neumann’s proof-theory course and, over Easter 1931, studied the page proofs of Gödel’s paper that Bernays had lent him; he wrote to Gödel from Berlin on 7 April 1931 working through the implications for his own consistency proofs. Herbrand fell to his death in the Massif des Écrins on 27 July 1931, aged twenty-three, two days after Gödel’s reply; his final paper was received by Journal für die reine und angewandte Mathematik on the same day. Gödel later credited Herbrand’s April letter with suggesting a crucial part of the definition of a general recursive function that he would set out in his 1934 IAS lectures — the foundation of computability theory.

The exchange belongs to an eight-year working relationship between Bernays and Gödel preserved in their correspondence (Collected Works, vol. IV; Feferman, Dawson, Goldfarb, Parsons, and Sieg, eds., Clarendon, 2003). On 2 April 1931 Gödel wrote to Bernays from Vienna with the dispatch of two offprints — one for Hilbert, one for Bernays himself — and a long letter sketching the truth-definition diagonal in detail, introducing in a footnote the compound-formula shorthand ‘Statt Sb(x¹⁷/Z(y)) schreibe ich kurz: [x; y]’ and remarking that the truth-definition idea had been developed independently and in parallel by Alfred Tarski. Bernays replied from Göttingen on 20 April — ‘Vielen Dank für die Übersendung der beiden Exemplare Ihrer Arbeit (für Herrn Professor Hilbert und für mich)’ — immediately adopting Gödel’s bracket convention and extending it with his own single-letter shorthands for compound recursive predicates; in the same letter he set out the first written derivation of the Tarski-style truth-undefinability contradiction in the formalism F, the diagonal step he would canonise eight years later on page 272 of Grundlagen II. The single-letter shorthand convention recurs at the formula site on page 189 of the present copy, where Bernays names Gödel’s compound provability expression with a single pencilled letter — the same notational move he had made in his 1931 letter.

The marginalia in this offprint run to substantive working notes on at least sixteen pages of the text block. The keystone is a single pencilled cross-reference. At the head of page 175, beside Gödel’s introduction of the diagonal construction, Bernays has written ‘S. 272’ — a reference to the page of Grundlagen II that houses the second incompleteness theorem, the derivability conditions, and his own formal version of Tarski’s truth-undefinability theorem (the close cousin of Gödel’s first theorem, proved by the same diagonal construction applied to truth rather than provability). The cited page is precisely where Bernays himself performs the diagonal step in the proof of Tarski’s theorem. He is reading Gödel’s setup and pointing across a decade to his own analogous one, in formal apparatus he was still composing.

The other marginalia work at three registers.

Terminological: Bernays maps Gödel’s vocabulary onto the canonical Hilbert–Bernays nomenclature, labelling Gödel’s sections II and III Satzkalkül and Funktionenkalkül (propositional and predicate calculus), abbreviating Ausdruck to ‘Ausdr.’, and underlining the word Peano in identification of the source of the Principia notation Gödel inherits.

Cross-referential: where Gödel defines the proof predicate, Bernays glosses the Principia origins (‘in PM’, ‘im PM’) and cross-references his own English-language Princeton mimeograph Logical Calculus, prepared with F. A. Ficken at the Institute for Advanced Study in 1935–36 and reviewed by Curry in the Journal of Symbolic Logic in December 1938; page 16 of that mimeograph sets out the propositional truth-functional completeness on which Gödel’s recursive class-symbol formalism rests.

Substantive: on the paper’s final page Bernays pointedly underlines Gödel’s promise of a demnächst erscheinende Fortsetzung, the never-written Part II in which the proof of the second theorem was to appear; and in the bottom margin of page 193, in a dense five-line pencil block also dated 1938, he sketches the case-by-case proof he would publish in Band II — enumerated cases marked ‘1.)’ and ‘2.)’ matching the structure of the Rosser-form sharpening that occupies pages 284–288, an ‘F C’ cluster (Formel ℭ, his own Fraktur shorthand for the Rosser-form Gödel sentence on page 284), and a closing function-application parenthetical matching the terminal disjunct of his central disjunction.

The 1938 dates are precisely locatable. In December of that year Bernays was at Zürich finalising the Grundlagen II manuscript and lecturing at the Entretiens de Zürich, organised by Ferdinand Gonseth, on Sur les questions méthodologiques actuelles de la théorie Hilbertienne de la démonstration — a paper Gödel would later cite in correspondence (CW IV, Letter 12, January 1942). The annotations in this copy are contemporaneous with that lecture and with the closing months of Band II composition.

The hand is authenticated against the principal surviving Bernays specimens at the ETH-Bibliothek Hochschularchiv, Zürich. The largest accessible corpus is Hs 973:41, a 34-page typescript prepared in 1952 by Gisbert Hasenjäger toward a never-completed second edition of Grundlagen der Mathematik and corrected throughout by Bernays in pencil and ink; a chronologically closer comparator is Hs 91:11, Bernays’s autograph letter to Hermann Weyl of 16 February 1935 (reproduced on the ETH Library’s institutional short-portrait page for Bernays) — three years short of the dated annotations here. The match obtains at script family (Latin academic cursive, distinct from the older German Kurrent that Hilbert continued to use to the end of his life), slant, compound-word ligature, parenthesis style, and Hilbert-school working vocabulary.

The book that resulted is the locus classicus of the second incompleteness theorem. The derivability conditions Bernays sets out in its § 5 — that any provability predicate PrT(x) satisfy the closure rules now called D1, D2, and D3 — are the apparatus by which the theorem has been stated and applied ever since. Martin Löb’s 1955 theorem (Journal of Symbolic Logic 20, 115–118) is built directly on Bernays’s D2 and D3; the resulting Hilbert–Bernays–Löb conditions underpin the whole modal logic of provability that Solovay, Boolos, and others developed across the second half of the twentieth century. Gerhard Gentzen — Bernays’s most distinguished Göttingen doctoral student — closed Band II’s open question whether the second theorem could be evaded by stepping outside the system, with his two 1936/1938 consistency proofs of arithmetic by transfinite induction up to ε₀; postwar proof theory through Schütte and Tait runs from there. Grundlagen II remains in active citation in current research in reverse mathematics and ordinal analysis.

Gödel’s twenty-six pages set the foundations not only of modern proof theory but of theoretical computer science. The arithmetisation technique of § 2 — the encoding of every formula and every proof as a unique natural number — is the formal ancestor of source-code-as-data, of Turing’s description numbers and his universal machine, and of the von Neumann architecture itself. The recursive functions of § 2 became, through Gödel’s own IAS lectures of February–May 1934 (taken down in mimeograph by Stephen Kleene and J. Barkley Rosser), the substrate of Alonzo Church’s λ-calculus and of his and Turing’s independent 1936 solutions to Hilbert’s Entscheidungsproblem. Rosser’s 1936 sharpening — replacing Gödel’s hypothesis of ω-consistency with simple consistency — is the result whose Bernays formulation occupies the page-193 marginal block of the present copy. Turing’s ‘On Computable Numbers, with an Application to the Entscheidungsproblem’ (Proc. London Math. Soc. 1936–37), motivated equally by Gödel 1931 and the Entscheidungsproblem, contained errors in its proof of the unsolvability of the latter; the single mathematician who identified them and prompted Turing’s published correction (Proc. London Math. Soc. 43, 1938) was Bernays, reading at Zürich. Turing’s correction-notice closes: ‘The author is indebted to P. Bernays for pointing out these errors’. The Swiss correspondent who caught Turing was the same logician who, in the same years, was writing the present marginalia.

The front wrapper carries, at upper left, the surname GÖDEL in deliberate dark-ink Roman block capitals with a thick red-crayon underline beneath, and matching red-crayon underlines on the printed words Mathematica in the title and Wien in the author line. The unified pattern identifies this inscription as a third-party cataloguing convention applied at some point in the offprint’s twentieth-century transit — a bookseller’s stock label or institutional shelf-marker — not a personal inscription, and not in Gödel’s own hand: his documented inscription practice on presentation offprints, attested by the five Morgenstern presentations dispersed at Bonhams in 2017 and by his autograph letter to Skolem of 1 November 1931 (Christie’s), is cursive Latin with German-language dedications, with no surviving instance of him writing his own surname in block capitals.

Among recorded surviving copies of the 1931 offprint, no other carries substantive working annotation by a major figure in the development of mathematical logic. Gödel’s own retained galley and offprint are at the Institute for Advanced Study, Princeton (finding aid C0282). Two are at the Bertrand Russell Archives at McMaster — one inscribed by Amethe, Countess von Zeppelin; the other unmarked, found in Dora Russell’s house after her death. Carnap’s copy is at the Carnap Papers, University of Pittsburgh. The two named-private copies that have appeared at auction — the Eino Kaila–Georg Henrik von Wright–Jan von Plato copy (Sotheby’s New York, 2017) and the Theodore Hailperin–John W. Dawson Jr. copy (Christie’s London, 2014) — carry presentation inscriptions but no substantive working notes. None of these copies sits at the same triangulation. No other surviving offprint can be traced, through its single annotator, to all three vectors of the result’s immediate reception: to the page proofs Bernays lent Herbrand at Easter 1931, to the corrections Bernays sent Turing on his 1936 paper, and to the canonical exposition of the second theorem that Bernays would publish in Grundlagen II. The present copy stands alone: the working witness to the transmission from Gödel’s compressed twenty-six pages of 1931 to the canonical architecture of 1939, in the hand of the mathematician who performed that transmission. A detailed report documenting the marginalia leaf by leaf, the documentary chain from the 1931 paper to Bernays’s 1939 canonical exposition, the paleographic comparison against the Hs 973:41 specimens at the ETH Hochschularchiv, and the full census of recorded 1931 offprints, is available on request.

Dawson, Logical Dilemmas: The Life and Work of Kurt Gödel (A. K. Peters, 1997), Ch. IV — Feferman et al. (eds.), Kurt Gödel: Collected Works, vol. IV: Correspondence A–G (Clarendon, 2003), particularly Letters 1–10 of the Bernays–Gödel exchange and Sieg’s editorial introduction — Collected Works, vol. V: Correspondence H–Z (Clarendon, 2003), Herbrand–Gödel correspondence — Hilbert and Bernays, Grundlagen der Mathematik, Band II, 2., neubearbeitete Aufl. (Berlin: Springer, 1970), § 5, pp. 263–387 — Sieg and Ravaglia, ‘Hilbert and Bernays’ Grundlagen der Mathematik’, in Grattan-Guinness (ed.), Landmark Writings in Western Mathematics 1640–1940 (Elsevier, 2005), pp. 981–1000 — Zach, ‘Kurt Gödel, paper on the incompleteness theorems (1931)’, ibid., pp. 917–925 — Zach, ‘Completeness Before Post: Bernays, Hilbert, and the Development of Propositional Logic’, Bulletin of Symbolic Logic 5:3 (1999), pp. 331–366 — Sieg, ‘Only Two Letters: The Correspondence between Herbrand and Gödel’, Bulletin of Symbolic Logic 11 (2005), pp. 172–184 — Bernays, Logical Calculus. Notes on Lectures at the Institute for Advanced Study 1935–36, prepared with the assistance of F. A. Ficken (mimeographed, IAS Princeton, 1936), reviewed by H. B. Curry, Journal of Symbolic Logic 3:4 (1938), pp. 162–163 — Turing, ‘On Computable Numbers, with an Application to the Entscheidungsproblem. A Correction’, Proceedings of the London Mathematical Society 2nd ser. 43 (1938), pp. 544–546 — Hodges, Alan Turing: The Enigma (Burnett, 1983) — von Neumann, ‘Tribute to Dr. Gödel’, in Bulloff, Holyoke and Hahn (eds.), Foundations of Mathematics: Symposium Papers Commemorating the Sixtieth Birthday of Kurt Gödel (Springer, 1969), pp. ix–x — Wang, A Logical Journey: From Gödel to Philosophy (MIT, 1996) — Linsky, ‘Russell and Gödel’, Bulletin of Symbolic Logic 19 (2013) — von Plato, Portrait of Young Gödel (Springer / Vienna Circle Institute Library 9, 2024) — Helsinki Gödel Enigma project (Lethen, Kanckos, Hämeen-Anttila, von Plato; ERC project 787758) — Mancosu and Zach, ‘Heinrich Behmann’s 1921 lecture on the decision problem’, Bulletin of Symbolic Logic 21 (2015) — Wirth, ‘A Most Interesting, but Revoked Draft for Hilbert and Bernays’ Grundlagen der Mathematik’, arXiv:1803.01386 (2018) — Bernays, ‘Sur les questions méthodologiques actuelles de la théorie Hilbertienne de la démonstration’, in Gonseth (ed.), Les Entretiens de Zürich (Zürich: Leemann, 1941), pp. 144–152 — DSB (Gödel) — Wang, Reflections on Kurt Gödel (MIT, 1987) — Sigmund, Exact Thinking in Demented Times (Basic, 2017) — Goldstein, Incompleteness: The Proof and Paradox of Kurt Gödel (Norton, 2005).



8vo (236 × 153 mm), pp. 173–198, drawn from Monatshefte für Mathematik und Physik, volume 38 (Leipzig: Akademische Verlagsgesellschaft, 1931); approximately one hundred copies struck for the author’s personal distribution from Vienna in late March 1931 (Dawson, Logical Dilemmas, 1997, Ch. IV). Original printed tan card wrappers, sewn, with the printed legend Überreicht vom Verfasser at the head of the front wrapper; back wrapper carries a publisher’s advertisement for L. Schiller (ed.), Hydro- und Aerodynamik I. Teil (Handbuch der Experimentalphysik IV/1), Leipzig 1931. Front wrapper carries two manuscript marks: at upper left, the surname GÖDEL in dark-ink Roman block capitals with a thick red-crayon underline beneath, matching red-crayon underlines marking the printed words Mathematica in the title and Wien in the author line (a unified third-party cataloguing or library-shelf convention, not in Gödel’s hand); at upper right, faint pencil cursive of uncertain content. Substantial pencil-cursive marginalia by Bernays on at least sixteen pages of the text block (pp. 173, 175, 176, 177, 178, 179, 180, 183, 184, 185, 186, 187, 189, 190, 193, 194, 195), including two explicit date markers ‘1938:’ on pp. 179 and 193; the cross-reference ‘S. 272’ on p. 175; Hilbert-school terminological glosses (Satzkalkül, Funktionenkalkül, ‘Ausdr.’) on p. 178; the Peano identification on p. 177; cross-references to Principia Mathematica on p. 186 (‘in PM’, ‘im PM’) together with the bilingual ‘s. Lect. Notes p. 16’; a function-iteration notation on p. 183; a single-letter shorthand for Gödel’s compound provability formula on p. 189; and a dense five-line bottom-margin block of mathematical working on p. 193; pointed underlining on p. 198 of Gödel’s promise of a never-realised Fortsetzung. Some light handling wear and edge-toning to wrappers; spine reinforced with a brown cloth strip; wrappers and text block both sound, holding together without lifted leaves; light foxing scattered.

.

Item #6710

Price: $225,000.00