1904 - "Proof that any set can be well-ordered" - Ernst Zermelo (well-ordering theorem). 1908 - "Investigations into the foundations of set theory I" - Zermelo (first axioms for Z-set theory). 1909 - "On the theory of transfinite numbers" - Paul Mahlo (introduces Mahlo cardinals). 1914 - Felix Hausdorff's opus "Principles of set theory appears" appears. World War I begins (28 July 1914). 1915 - Leopold Löwenheim proves his eponymous theorem in "On possibilities in the calculus of relatives." 1918 - Armistice signed; World War I ends (11 Nov 1918). 1922 - Thoralf Skolem's "Einige Bemerkungen …" and Abraham Fraenkel's "Zur Mengenlehre" extend Zermelo → ZF set theory. 1925 - John von Neumann, "An axiomatization of set theory", laying the groundwork for NBG set-class theory. 1929-30 - Kurt Gödel, doctoral thesis and "On the completeness of the logical calculus" (completeness theorem). 1930 - Haskell Curry, "Foundations of Combinatorial Logic" (first full system of combinatory logic). 1931 - Gödel publishes "On Formally Undecidable Propositions of Principia Mathematica and Related Systems" (first incompleteness theorem). 1932 - Alonzo Church, "A Set of Postulates for the Foundation of Logic." 1935 - S.C. Kleene & J.B. Rosser show the untyped λ-calculus is inconsistent in "The Inconsistency of Certain Formal Logics"; Gerhard Gentzen introduces the sequent calculus in "Untersuchungen über das logische Schließen." 1936 - Church, "An Unsolvable Problem of Elementary Number Theory" (Entscheidungsproblem). 1936 - Alan Turing, "On Computable Numbers …" (Turing machines; Church–Turing thesis). 1936 - Gentzen, "Die Widerspruchsfreiheit der reinen Zahlentheorie" (ε₀ consistency of PA). 1938 - Gödel proves AC + GCH are consistent with ZF via the constructible universe L. 1939 - World War II begins (1 Sep 1939). 1940 - Mid-year: Turing's Bombe enables regular decryption of Luftwaffe Enigma traffic, marking the first sustained Enigma break-through. 1945 - World War II ends (2 Sep 1945). 1945 - John Von Neumann gathers a group of engineers at the Institute for advanced study at Princeton to begin building digital computer with 5kb storage. 1950 - Turing proposes the "Turing Test" in "Computing Machinery and Intelligence." 1952 - Turing is arrested and convicted for homosexuality (31 Mar 1952). 1963 - Paul J. Cohen, "The Independence of the Continuum Hypothesis." 1964 - Cohen, "The Independence of the Axiom of Choice from ZF." 1967 - Harvey Friedman gets his PhD from MIT at the age of 19. 1969 - William A. Howard circulates "The formulae-as-types notion of construction," founding the Curry–Howard correspondence. 1971 - Kenneth Kunen's "Elementary Embeddings and Infinitary Combinatorics" proves the Kunen inconsistency (no non-trivial j : V → V in ZFC). 1974 - William N. Reinhardt posits Reinhardt cardinals (elementary embeddings V ↷ V) - consistent with ZF but not with AC. 1975 - Harvey Friedman uses Kruskal's Tree Theorem to obtain the first natural independence results for subsystems of second-order arithmetic, birthing Reverse Mathematics. 1978 - Kurt Gödel dies in Princeton (14 Jan 1978). 1985 - Stephen G. Simpson's lecture notes Subsystems of Second Order Arithmetic circulate, canonising Reverse Mathematics. 1988 - Thierry Coquand & Gérard Huet publish "The Calculus of Constructions," a keystone of modern type theory and Coq. 1996 - Harvey Friedman publishes a short paper called "Extremely Large Cardinals in the Rationals." 1999 - Stephen Simpson's book Subsystems of Second Order Arithmetic published.