Book1958
Gödel's Proof
Ernest Nagel & James R. Newman
Walks a general reader through Gödel's argument that any consistent system strong enough for arithmetic contains truths it cannot prove.
link checked 17 Sept 2026FreeEntry
Foundations & Logic
What mathematics rests on, and the limits of what it can prove about itself.
13 topics · 27 curated works
Topics
Reading in Foundations & Logic
27A way in
Start here
No prior grounding assumed.
Gödel's Proof
Ernest Nagel & James R. Newman · 1958
Walks a general reader through Gödel's argument that any consistent system strong enough for arithmetic contains truths it cannot prove.
+3 more at this level
Then
Assumes you know the vocabulary.
The Mathematical Analysis of Logic
George Boole · 1847
Recasts logical reasoning as an algebra of classes obeying arithmetic-like laws, treating deductive inference as a calculation to be checked rather…
+8 more at this level
Go deeper
Primary sources and full treatments.
On Computable Numbers, with an Application to the Entscheidungsproblem
Alan Turing · 1936
Defines the universal machine and proves the halting problem undecidable — the founding document of computer science.
+13 more at this level
12 of 27 works
Essay1998
Constructive Mathematics
Douglas Bridges
Argues mathematics should only assert existence where an object can in principle be exhibited or computed, and shows how much of analysis survives when that constraint replaces the law of excluded middle.
link checked 17 Sept 2026FreeEntry
Book2005
forall x: An Introduction to Formal Logic
P.D. Magnus
Builds formal validity from explicit translation into symbolic logic and truth tables rather than rules to memorise, so an argument's validity becomes something the reader can check for themselves.
link checked 17 Sept 2026FreeEntry
Video2021
Math's Fundamental Flaw
Derek Muller (Veritasium)
Traces the route from Cantor's diagonal argument through Godel's incompleteness theorems to Turing's halting problem, arguing they are three faces of one limit on formal systems.
link checked 17 Sept 2026FreeEntry
Book1847
The Mathematical Analysis of Logic
George Boole
Recasts logical reasoning as an algebra of classes obeying arithmetic-like laws, treating deductive inference as a calculation to be checked rather than an art to be judged.
link checked 17 Sept 2026FreeIntermediate
Book1976
Elementary Calculus: An Infinitesimal Approach
H. Jerome Keisler
Rebuilds single-variable calculus on Abraham Robinson's infinitesimals rather than epsilon-delta limits, arguing Leibniz's intuitive infinitesimal reasoning can be made fully rigorous.
link checked 17 Sept 2026FreeIntermediate
Essay2001
Model Theory (Stanford Encyclopedia of Philosophy)
Wilfrid Hodges
Introduces model theory as the study of the relationship between formal languages and the structures that satisfy them, organised around the compactness and Loewenheim-Skolem theorems.
link checked 17 Sept 2026FreeIntermediate
Essay2004
Computability and Complexity (Stanford Encyclopedia of Philosophy)
Neil Immerman
Surveys computability theory and computational complexity as one continuum, from what a Turing machine cannot decide at all to what it can decide only given resources that grow faster than any polynomial.
link checked 17 Sept 2026FreeIntermediate
Essay2006
Type Theory (Stanford Encyclopedia of Philosophy)
Thierry Coquand
Traces type theory from Russell's device for blocking his own paradox through Martin-Loef's constructive type theory, arguing that treating proofs and programs as the same kind of object is the theory's real payoff.
link checked 17 Sept 2026FreeIntermediate
Essay2008
The Axiom of Choice
John L. Bell
Lays out the equivalents of the axiom of choice, including Zorn's Lemma and the well-ordering theorem, and the paradoxical consequences, such as Banach-Tarski, that made it controversial even after its independence from the other axioms was proved.
link checked 17 Sept 2026FreeIntermediate
Essay2008
The Development of Proof Theory
Jan von Plato
Recounts proof theory from Hilbert's program for proving consistency by finitary means through Gentzen's natural deduction and sequent calculus, treating the field's central results as an answer to a foundational crisis rather than a purely technical exercise.
link checked 17 Sept 2026FreeIntermediate
Book2013
Category Theory for Scientists
David I. Spivak
Recasts category theory as a general-purpose modelling language for the sciences, using databases and hierarchies as running examples rather than starting from pure mathematics.
link checked 17 Sept 2026FreeIntermediate
In order written
1847 – 2021- 1847The Mathematical Analysis of LogicGeorge Boole
- 1904Beweis, dass jede Menge wohlgeordnet werden kannErnst Zermelo
- 1910Principia MathematicaAlfred North Whitehead & Bertrand Russell
- 1936An Unsolvable Problem of Elementary Number TheoryAlonzo Church
- 1945General Theory of Natural EquivalencesSamuel Eilenberg & Saunders Mac Lane
- 1958Gödel's ProofErnest Nagel & James R. Newman
- 1961Non-standard AnalysisAbraham Robinson
- 1963The Independence of the Continuum HypothesisPaul J. Cohen
- 1967Foundations of Constructive AnalysisErrett Bishop
- 1976Elementary Calculus: An Infinitesimal ApproachH. Jerome Keisler
- 1998Constructive MathematicsDouglas Bridges
- 1998An Introduction to Proof TheorySamuel R. Buss
- 1999Subsystems of Second Order ArithmeticStephen G. Simpson
- 2001Model Theory (Stanford Encyclopedia of Philosophy)Wilfrid Hodges
- 2004Computability and Complexity (Stanford Encyclopedia of Philosophy)Neil Immerman
- 2005forall x: An Introduction to Formal LogicP.D. Magnus
- 2006Type Theory (Stanford Encyclopedia of Philosophy)Thierry Coquand
- 2008The Axiom of ChoiceJohn L. Bell
- 2008The Development of Proof TheoryJan von Plato
- 2013Category Theory for ScientistsDavid I. Spivak
- 2013Homotopy Type Theory: Univalent Foundations of MathematicsThe Univalent Foundations Program
- 2014Set TheoryJoan Bagaria
- 2016Category Theory in ContextEmily Riehl
- 2016Model TheoryLou van den Dries and C. Ward Henson
- 2021Math's Fundamental FlawDerek Muller (Veritasium)