Mathematical Logic and Foundations

Canonical T1 reference for the logical and foundational substrate of mathematics. Touches propositional + first-order logic, set theory, incompleteness, computability, model theory, proof theory, type theory and the constructive tradition, and a pointer at category theory.

Related notes:

• philosophy-of-mind-and-language — logic as language theory.
• epistemology — what counts as proof, intuition, and certainty.
• number-theory, algebraic-geometry-foundations, group-theory-and-representation — domains that use the foundations.
• coq, lean, agda, idris — practical proof assistants and dependently typed languages.

1. At a glance

Mathematical logic is the formal study of valid reasoning, formal languages, models, proofs, and the limits of computation. Foundations is the meta-mathematical project of identifying a base layer of axioms and rules from which the rest of mathematics can be derived.

The 1879-1936 founding period (Frege, Russell, Hilbert, Gödel, Tarski, Turing) produced several seismic results:

• A rigorous syntactic notion of proof, separable from semantic truth (Frege 1879, Russell 1910).
• An axiomatic foundation for all of working mathematics (ZFC set theory; Zermelo 1908, Fraenkel + Skolem 1920s).
• A proof that arithmetic is incomplete — there are true statements that cannot be proved (Gödel 1931).
• A mechanical model of computation (Turing 1936) and the undecidability of the halting problem.
• The completeness theorem connecting syntactic provability to semantic truth in first-order logic (Gödel 1929).

This note surveys the resulting landscape: classical logic (propositional and first-order), set theory and the universe, computability, model and proof theory, the constructive / type-theoretic alternative tradition, and a brief pointer at category theory as a foundational alternative.

Why a working mathematician or AI agent should care

• Programming languages and verification — type systems (Hindley-Milner, dependent types) and proof assistants (Coq, Lean, Agda, Isabelle) are direct descendants of formal logic. The Curry-Howard correspondence makes proofs and programs the same thing.
• AI and reasoning — SAT solvers, SMT solvers, theorem provers, planning, formal methods. Every soundness/completeness question in an LLM-reasoning system has its analogue here.
• Database theory — relational algebra is a fragment of first-order logic; Datalog is a fragment of Horn-clause logic.
• Complexity theory — Cook (1971) showed propositional SAT is NP-complete; the entire P-vs-NP question is logic-theoretic at heart.
• Philosophy of mathematics — the foundational debates (logicism, formalism, intuitionism, structuralism) live and die on the technical theorems below.

2. Propositional logic

The simplest formal system. Atomic propositions $p,q,r,\dots$ are combined via connectives:

Symbol	Name	Truth condition
$\neg$	negation	$\neg p$ true iff $p$ false
$\wedge$	conjunction	both true
$\vee$	disjunction	at least one true
$\to$	implication	false only when $p$ true, $q$ false
$\leftrightarrow$	biconditional	both same value
$\oplus$	XOR	exactly one true

Syntax — well-formed formulas (WFFs) built inductively from atoms via connectives.

Semantics — a truth assignment $v:\mathrm{Atoms}\to \{T,F\}$ extends compositionally to all WFFs. $\phi$ is valid (a tautology) iff true under every assignment; satisfiable iff true under some assignment; contradictory if true under none.

Equivalences and normal forms

Equivalence	Form
Double negation	$\neg \neg p\equiv p$
De Morgan	$\neg (p\wedge q)\equiv \neg p\vee \neg q$
Distribution	$p\wedge (q\vee r)\equiv (p\wedge q)\vee (p\wedge r)$
Material implication	$p\to q\equiv \neg p\vee q$
Contrapositive	$p\to q\equiv \neg q\to \neg p$
Excluded middle	$p\vee \neg p$ (classical only)
Peirce’s law	$((p\to q)\to p)\to p$ (classical only)

Normal forms.

• Disjunctive normal form (DNF) — disjunction of conjunctions of literals.
• Conjunctive normal form (CNF) — conjunction of disjunctions of literals; the input form for SAT solvers.
• Negation normal form (NNF) — negations applied only to atoms.
• Horn clauses — at most one positive literal per clause; underlies Prolog and Datalog.

Every WFF has a (non-unique) equivalent in each normal form. Conversion can blow up exponentially.

Proof systems

Three styles, all equivalent in deductive power for classical propositional logic:

1. Hilbert-style (axiomatic) — a few axiom schemata plus modus ponens. Compact to state, painful to use.
2. Natural deduction (Gentzen 1934) — introduction and elimination rules per connective. Closest to informal mathematical reasoning.
3. Sequent calculus (Gentzen 1934) — manipulates sequents $\Gamma ⊢\Delta$ via left/right rules; the central object of proof theory (Section 11).

Soundness. If $\Gamma ⊢\phi$ in the proof system then $\Gamma \models \phi$ semantically.

Completeness (propositional, Post 1921). If $\Gamma \models \phi$ then $\Gamma ⊢\phi$. Together with soundness, syntactic provability matches semantic validity.

Compactness. A set $\Gamma$ is satisfiable iff every finite subset is. Follows from completeness; key tool in model theory.

SAT and complexity

The Boolean satisfiability problem (SAT) asks: given $\phi$ in CNF, does some assignment satisfy it? Cook (1971) (independently Levin 1973) showed SAT is NP-complete — the foundational result of complexity theory. Every problem in NP reduces to SAT in polynomial time.

Modern SAT solvers — CDCL (Conflict-Driven Clause Learning), originating with GRASP (Marques-Silva + Sakallah 1996) and Chaff (Moskewicz et al. 2001), routinely handle industrial instances with millions of variables despite the worst-case exponential hardness. The gap between worst-case and typical-case is one of the deep mysteries of computer science.

SMT (Satisfiability Modulo Theories) generalises SAT by allowing background theories (linear arithmetic, arrays, bit-vectors, uninterpreted functions). Solvers like Z3, CVC5 power program verification, model checking, and security analysis.

3. First-order logic

Propositional logic cannot say “all”, “some”, or “equals”. First-order logic (FOL) extends it with quantifiers $\forall ,\exists$ over a domain of individuals, variables, function symbols, relation symbols, and equality.

Signature — a tuple $\Sigma =(\text{constants},\text{functions},\text{relations})$ with arities.

Terms — built from variables, constants, and function applications.

Formulas — atomic ($R(t_1,\dots ,t_n)$, $t_1=t_2$) combined via Boolean connectives and quantifiers.

Example (arithmetic). Signature $\{0,S,+,\cdot ,<\}$. Formula $\forall x\forall y(x<y\to \exists z(x+z=y))$.

Tarski semantics (1933)

A structure $\mathcal{M}$ for signature $\Sigma$ is a pair $(M,{\cdot }^{\mathcal{M}})$: a non-empty domain $M$ and interpretations of each constant, function, relation. An assignment $\sigma$ maps variables to elements of $M$. Tarski’s recursive truth definition specifies when $\mathcal{M}\models \phi [\sigma ]$:

• $\mathcal{M}\models R(t_1,\dots ,t_n)[\sigma ]$ iff $(t_1^{\mathcal{M},\sigma },\dots ,t_n^{\mathcal{M},\sigma })\in R^{\mathcal{M}}$.
• Boolean cases by usual recursion.
• $\mathcal{M}\models \forall x\phi [\sigma ]$ iff $\mathcal{M}\models \phi [\sigma [x\mapsto a]]$ for every $a\in M$.
• $\mathcal{M}\models \exists x\phi [\sigma ]$ iff $\mathcal{M}\models \phi [\sigma [x\mapsto a]]$ for some $a\in M$.

A sentence $\phi$ (no free variables) is true in $\mathcal{M}$ iff $\mathcal{M}\models \phi$. A theory $T$ is a set of sentences; $\mathcal{M}$ models $T$ iff it satisfies every sentence in $T$.

Gödel’s completeness theorem (1929)

Theorem. For a first-order theory $T$ and sentence $\phi$: $T⊢\phi$ iff $T\models \phi$.

That is, syntactic provability and semantic entailment coincide in FOL. The proof (Henkin-style; Henkin 1949 simplification) constructs a model of any consistent theory from witnessing constants.

Two important corollaries:

Compactness. $T$ has a model iff every finite subset does. Used to build non-standard models (of arithmetic, analysis, etc.).

Löwenheim-Skolem theorem (Löwenheim 1915, Skolem 1920). Any consistent FOL theory with at least one infinite model has models of every infinite cardinality $\ge |\Sigma |$. So no first-order theory can pin down a unique infinite structure up to isomorphism. Hence the Skolem paradox: ZFC has a countable model even though ZFC proves uncountable sets exist (the model’s notion of “uncountable” is internal).

Beyond first-order

Higher-order logic (HOL) allows quantification over predicates (Frege 1879, Russell 1910). Strictly more expressive, but loses completeness (Henkin semantics restores it by restricting to “general” models).

Infinitary logics $L_{\kappa \lambda }$ allow infinite conjunctions / quantifiers. Useful for descriptive set theory and admissibility theory.

Modal logics (Kripke 1959, 1963) add operators $\square$ (necessity), $◊$ (possibility). Underlie temporal logic, epistemic logic, dynamic logic, and program verification. Soundness + completeness for various axiom systems (K, T, S4, S5) match different classes of Kripke frames.

Intuitionistic logic — drops excluded middle; semantics via Kripke models or Heyting algebras (Section 12).

4. Set theory and the axiomatic universe

Naïve set theory. Cantor (1874-1897) introduced sets, cardinality, the diagonal argument, the hierarchy of infinities ${\aleph }_0<{\aleph }_1<{\aleph }_2<\cdots$. Russell’s paradox (1901) — the “set of all sets that do not contain themselves” — showed naïve comprehension is inconsistent. The response: axiomatic set theory.

ZFC — Zermelo-Fraenkel set theory with Choice

The canonical foundation of modern mathematics. Axioms (Zermelo 1908, Fraenkel + Skolem 1920s; choice typically labelled separately):

1. Extensionality — sets with the same members are equal.
2. Pairing — for any $a,b$, the set $\{a,b\}$ exists.
3. Union — for any $A$, $\bigcup A$ exists.
4. Power set — for any $A$, $\mathcal{P}(A)$ exists.
5. Separation (schema) — for any property $\phi$, $\{x\in A:\phi (x)\}$ exists.
6. Replacement (schema) — for a definable function $F$ and set $A$, the image $F[A]$ is a set. (Fraenkel + Skolem, 1922.)
7. Infinity — an infinite set exists (e.g. ℕ).
8. Foundation / Regularity — every non-empty set has an $\in$-minimal element. Excludes pathological self-membership.
9. Choice (AC) — every collection of non-empty sets has a choice function.

Together: ZF (without choice) or ZFC.

Ordinals and cardinals

Ordinals — well-ordered sets up to isomorphism; canonically $0=\varnothing$, $1=\{0\}$, $2=\{0,1\}$, …, $\omega =\{0,1,2,\dots \}$, $\omega +1,\omega \cdot 2,{\omega }^2,{\omega }^{\omega },{\epsilon }_0,\dots$. Ordinals are linearly well-ordered by $\in$.

Cardinals — equivalence classes of sets under bijection. $|A|=|B|$ iff there is a bijection. ${\aleph }_0=|\mathbb{N}|$; ${\aleph }_1$ = least uncountable cardinal; etc.

Cantor’s theorem. $|A|<|\mathcal{P}(A)|$ — no surjection from $A$ to $\mathcal{P}(A)$. So the cardinal hierarchy is unbounded.

Continuum hypothesis (CH). $2^{{\aleph }_0}={\aleph }_1$. Gödel (1940) showed CH is consistent with ZFC (via the constructible universe $L$); Cohen (1963) showed its negation is also consistent (via forcing). Hence CH is independent of ZFC — neither provable nor refutable. Cohen won the 1966 Fields Medal for forcing.

The axiom of choice and its equivalents

Choice is non-constructive and has paradoxical consequences (Banach-Tarski paradox 1924), but is needed for:

• Every vector space has a basis.
• Every product of compact spaces is compact (Tychonoff).
• Every ideal is contained in a maximal ideal.
• The Hahn-Banach theorem in functional analysis.

Equivalents to AC (under ZF).

• Zorn’s Lemma — every non-empty partially ordered set in which every chain has an upper bound has a maximal element.
• Well-ordering theorem (Zermelo 1904) — every set can be well-ordered.
• Hausdorff maximal principle — every chain in a poset extends to a maximal chain.
• Tukey’s lemma — every collection of finite character has a maximal element.

Weaker fragments — countable choice (DC), axiom of dependent choice — suffice for most of analysis without the worst pathologies.

Alternative foundations

ZFC is dominant but not unique. Alternatives:

• NBG (von Neumann-Bernays-Gödel) — adds proper classes; conservative over ZFC.
• MK (Morse-Kelley) — strictly stronger than NBG.
• Type theory — Section 12.
• Category theory / ETCS (Lawvere 1964) — Elementary Theory of the Category of Sets.
• Homotopy type theory (HoTT) (Voevodsky et al. 2006-2013) — Section 12.

5. Gödel’s incompleteness theorems (1931)

Setting. Let $T$ be a consistent, recursively axiomatised theory strong enough to encode arithmetic (e.g. Peano arithmetic PA or any extension; ZFC qualifies).

First incompleteness theorem. There exists a sentence $G_T$ in the language of $T$ that is true in the standard model of arithmetic but neither provable nor refutable in $T$.

Construction: encode the syntax of $T$ via Gödel numbering (each formula and proof gets a natural-number code). Build a formula ${\mathrm{Prov}}_T(x)$ saying ”$x$ is the code of a provable sentence”. Use diagonalisation (Cantor’s trick once removed) to construct $G_T$ asserting “I am not provable in $T$“. If $T$ proved $G_T$, $T$ would prove a false statement; if $T$ proved $\neg G_T$, $T$ would be inconsistent (by reflecting that fact).

Second incompleteness theorem. $T$ cannot prove its own consistency $\mathrm{Con}(T)$ (assuming $T$ is consistent). So we cannot bootstrap confidence in $T$‘s consistency from within $T$.

Consequences.

• Hilbert’s programme of finitistic foundations for all of mathematics is impossible as originally stated.
• ZFC cannot prove its own consistency (assuming it is consistent); we trust it on extrinsic grounds (no contradiction found, models in stronger systems).
• “Truth” and “provability” diverge: $G_T$ is true but unprovable.
• Refinements: Rosser (1936) removed Gödel’s $\omega$-consistency assumption; Löb’s theorem (1955) gave a powerful formal-provability principle; Paris-Harrington (1977) found “natural” arithmetic statements independent of PA.

The incompleteness theorems do not say mathematics is futile; they say no single formal system captures all mathematical truth. Mathematics expands by adopting new axioms (large cardinal axioms, determinacy axioms) that decide previously-independent questions.

6. Computability theory

A computational model suffices for arithmetic if it can compute exactly the computable functions on ℕ. Several formalisms turned out to be equivalent — the Church-Turing thesis: any “effectively calculable” function is computable in any of these.

Computational models

• Turing machine (Turing 1936) — finite control + infinite tape + read/write head.
• λ-calculus (Church 1932-1936) — function abstraction and application; Church-Rosser confluence theorem.
• Recursive functions (Gödel + Herbrand 1934, Kleene 1936) — primitive recursive base + minimisation.
• Register machines (Shepherdson + Sturgis 1963), counter machines, cellular automata, real-world programming languages.

All are equivalent in computational power and define the same class of partial recursive functions.

Halting problem and undecidability

Halting problem. Given a program $P$ and input $x$, does $P$ halt on $x$? Turing (1936) proved this is undecidable: no algorithm decides halting for arbitrary $(P,x)$. Proof: assume a halting-decider $H$; build $D(P)=$ “loop forever if $H(P,P)$ says halt; halt otherwise” and derive a contradiction at $D(D)$.

Rice’s theorem (1951). Any non-trivial semantic property of partial functions is undecidable. So “does $P$ compute the constant function 0?”, “does $P$ run in polynomial time?”, “is $P$ equivalent to $Q$?” are all undecidable.

Reductions and degrees. Problem $A$ many-one reduces to $B$ ($A{\le }_{m}B$) if there is a computable $f$ with $x\in A⟺f(x)\in B$. Turing reduces allows oracle access. Turing degrees classify problems by their relative difficulty; the halting problem is the canonical example at degree $0^{\prime }$. There are infinitely many strictly-increasing degrees (Friedberg-Muchnik 1956).

Complexity classes

P — decidable in deterministic polynomial time. NP — decidable in nondeterministic polynomial time; equivalently, “guess then verify in polynomial time”. NP-complete — NP problems to which every NP problem polynomial-time reduces (Cook 1971, Karp 1972). PSPACE, EXPTIME, EXPSPACE, BPP, BQP, … — many other classes; see complexity theory texts.

The P versus NP problem asks whether P = NP. Almost universally believed to be P ≠ NP; one of the Clay Millennium problems. A proof either way would reshape mathematics, cryptography, and AI.

Decidable vs undecidable theories

Theory	Decidable?	Why
Propositional logic	Decidable (NP-complete validity)	Truth tables / SAT
Presburger arithmetic ($\mathbb{N},+$)	Decidable (Presburger 1929)	Quantifier elimination
Real closed fields ($\mathbb{R},+,\cdot$)	Decidable (Tarski 1948)	CAD; exponential complexity
Algebraically closed fields	Decidable	Quantifier elimination
Theory of ℕ with $+,\cdot$ (PA)	Undecidable (Church 1936)	Encodes the halting problem
ZFC	Undecidable	Encodes arithmetic
Word problem in groups	Undecidable (Novikov 1955, Boone 1959)	---
Hilbert’s 10th problem (Diophantine)	Undecidable (Matijasevich 1970)	MRDP theorem

7. Model theory

Studies structures and their first-order theories.

Theory of a structure. $\mathrm{Th}(\mathcal{M})=\{\phi :\mathcal{M}\models \phi \}$ — all first-order sentences true in $\mathcal{M}$.

Elementary equivalence. $\mathcal{M}\equiv \mathcal{N}$ iff $\mathrm{Th}(\mathcal{M})=\mathrm{Th}(\mathcal{N})$. Weaker than isomorphism in general; by Löwenheim-Skolem, $\mathcal{M}\equiv$ many non-isomorphic $\mathcal{N}$.

Elementary substructure. $\mathcal{M}⪯\mathcal{N}$ if $\mathcal{M}\subseteq \mathcal{N}$ and every $\phi (\bar{a})$ with parameters from $M$ has the same truth value in both.

Types. A type over a parameter set $A$ is a maximal consistent set of formulas with parameters from $A$. Types capture “what can be said about” an element. Saturated models realise all types.

Categoricity. $T$ is $\kappa$-categorical if all its models of cardinality $\kappa$ are isomorphic. Morley’s categoricity theorem (1965): a countable complete theory categorical in some uncountable cardinal is categorical in every uncountable cardinal — a stunning result that launched modern stability theory and Shelah’s classification programme.

Examples.

• Theory of $(\mathbb{Q},<)$ — dense linear orders without endpoints; ${\aleph }_0$-categorical (Cantor’s back-and-forth).
• Theory of algebraically closed fields of characteristic $p$ — categorical in uncountable cardinals; foundational for algebraic geometry.
• Theory of vector spaces over a fixed field — categorical in every cardinality $>$ field size.

Quantifier elimination. Some theories admit it: every formula is equivalent to a quantifier-free formula. Decidability and good geometric properties usually follow. Examples: algebraically closed fields, real closed fields, presburger arithmetic.

Compactness and ultraproducts (Łoś 1955). Compactness theorem proved via ultraproducts; the ultraproduct construction yields non-standard models — non-standard analysis (Robinson 1960) uses ultraproducts of $\mathbb{R}$ to give a rigorous treatment of infinitesimals.

8. Proof theory

Studies proofs as combinatorial objects. Originated with Hilbert (1900s) and matured under Gentzen (1930s).

Sequent calculus (Gentzen 1934)

A sequent $\Gamma ⊢\Delta$ asserts “from the assumptions $\Gamma$, at least one of $\Delta$ follows”. Inference rules act on sequents; the system LK (for classical logic) has structural rules (weakening, contraction, exchange), logical rules (left and right introductions for each connective), and one cut rule:

$$\frac{\Gamma ⊢\Delta ,\phi \phi ,\Sigma ⊢\Pi }{\Gamma ,\Sigma ⊢\Delta ,\Pi }.$$

Cut corresponds to using a lemma: proved $\phi$, now use it.

Cut elimination (Hauptsatz, Gentzen 1934)

Theorem. Every LK proof can be transformed into a cut-free proof of the same conclusion. (Same theorem for intuitionistic LJ.)

Consequences:

• Subformula property — cut-free proofs only mention subformulas of the conclusion. Powerful for proof search.
• Consistency of PA via ordinal induction up to ${\epsilon }_0$ (Gentzen 1936). This proof was historically important — PA’s consistency is not provable in PA (Gödel II), but is provable in PA + transfinite induction.
• Interpolation theorem (Craig 1957) and Beth’s definability theorem follow.

Proof complexity

How long are proofs? Resolution is a proof system for refuting CNF formulas; lower bounds on resolution proof length (Haken 1985 for the pigeonhole principle, exponential lower bound) parallel computational complexity bounds. The Frege, extended Frege, bounded-arithmetic hierarchies of proof systems are the proof-theoretic analogue of complexity classes.

Reverse mathematics (Friedman + Simpson, 1970s-)

Identify the minimal axiom system needed to prove given mathematical theorems. The “big five” subsystems of second-order arithmetic:

1. RCA₀ — recursive comprehension; basic computable analysis.
2. WKL₀ — weak König’s lemma; many classical theorems (Heine-Borel, separating hyperplane).
3. ACA₀ — arithmetical comprehension; classical analysis + algebra at countable level.
4. ATR₀ — arithmetical transfinite recursion.
5. Π¹₁-CA₀ — Π¹₁-comprehension; strong descriptive set theory.

Most ordinary mathematics lives at WKL₀ or ACA₀, well below the strength of ZFC.

9. Constructive mathematics and intuitionism

Brouwer (1908 onward) rejected classical excluded middle on philosophical grounds: a proof of $\phi \vee \neg \phi$ should produce either a proof of $\phi$ or a proof of $\neg \phi$, but for many statements we have neither.

Intuitionistic logic drops excluded middle ($p\vee \neg p$), double-negation elimination ($\neg \neg p\to p$), and Peirce’s law. Proofs are constructive — to prove $\exists x\phi$ one must exhibit a witness; to prove $\phi \vee \psi$ one must produce a proof of at least one.

Heyting algebra semantics: instead of $\{T,F\}$, truth values lie in a Heyting algebra (a lattice with a relative pseudo-complement). Kripke semantics alternative: a tree of possible worlds with monotone valuations.

Brouwer-Heyting-Kolmogorov (BHK) interpretation. Reads each connective as a constructive operation:

• A proof of $\phi \wedge \psi$ is a pair (proof of $\phi$, proof of $\psi$).
• A proof of $\phi \to \psi$ is a function turning proofs of $\phi$ into proofs of $\psi$.
• A proof of $\exists x\phi$ is a pair (witness $a$, proof of $\phi [a/x]$).
• A proof of $\forall x\phi$ is a function $a\mapsto$ proof of $\phi [a/x]$.

This points directly at type theory.

Constructive mathematics in practice

Bishop (1967, Foundations of Constructive Analysis) showed that essentially all of analysis can be done constructively, just with more careful statements. Modern constructive frameworks:

• Errett Bishop’s constructive analysis — neutral toward classical mathematics.
• Martin-Löf type theory (1972, 1984) — formal foundation for constructive maths; basis of Agda, Coq’s CIC, Lean.
• CZF / IZF — constructive set theories.

10. Curry-Howard correspondence

Curry (1934), Howard (1969, published 1980) observed a deep equivalence:

Logic	Type theory
Proposition $\phi$	Type $A$
Proof of $\phi$	Inhabitant / term $t:A$
$\phi \to \psi$	Function type $A\to B$
$\phi \wedge \psi$	Product type $A\times B$
$\phi \vee \psi$	Sum type $A+B$
$\forall x:T,\phi (x)$	Dependent function $\Pi x:T.A(x)$
$\exists x:T,\phi (x)$	Dependent pair $\Sigma x:T.A(x)$
Cut elimination	Beta reduction

Propositions = types, proofs = programs, theorem proving = programming. This insight powers modern proof assistants:

• Coq — based on the Calculus of Inductive Constructions (Coquand + Huet 1988); used for the Four-Colour Theorem (Gonthier 2005), Feit-Thompson Odd Order Theorem (Gonthier et al. 2012), CompCert verified C compiler (Leroy 2009).
• Agda — dependently typed; emphasises programming as the same activity as proving.
• Lean — Microsoft Research / Leonardo de Moura (2013); growing community formalisation effort (Mathlib has over a million lines).
• Isabelle/HOL — higher-order classical logic; long industrial track record.
• Idris — practical dependently-typed programming language.

See coq, lean, agda, idris for the language notes.

Dependent type theory

Martin-Löf type theory (MLTT) is the dominant constructive foundation. Types may depend on values: $\mathrm{Vec}(A,n)$ is the type of length-$n$ lists of $A$‘s; $n$ varies. Identity types ${\mathrm{Id}}_A(a,b)$ encode equality.

Homotopy type theory (HoTT)

Voevodsky (2006-2014) and collaborators discovered that identity types in MLTT carry the structure of homotopy: types are spaces, terms are points, identifications are paths, higher identifications are higher homotopies. The univalence axiom (Voevodsky) asserts that equivalent types are equal — a constructive rendition of the practising mathematician’s “up to isomorphism” reasoning.

HoTT is both a new foundation (potentially replacing ZFC) and a programming language for higher mathematics. The HoTT Book (2013) is the founding text. Active research includes cubical type theory (Cohen, Coquand, Huber, Mörtberg 2015) — a computable interpretation of univalence.

11. Category theory primer

A categorical lens on foundations. Originates with Eilenberg-Mac Lane (1945) for algebraic topology; matured under Mac Lane, Grothendieck, Lawvere, and others.

A category $\mathcal{C}$ consists of:

• A collection of objects.
• For each pair $X,Y$, a set ${\mathrm{Hom}}_{\mathcal{C}}(X,Y)$ of morphisms.
• A composition operation $\mathrm{Hom}(Y,Z)\times \mathrm{Hom}(X,Y)\to \mathrm{Hom}(X,Z)$.
• Identity morphisms ${\mathrm{id}}_X$ for each object.

Subject to associativity and identity laws.

Examples.

• Set — sets and functions.
• Grp, Ab, Ring, Top — groups, abelian groups, rings, topological spaces and their structure-preserving maps.
• Vect_k — vector spaces over $k$ and linear maps.
• Cat — categories and functors.

Functor — a map between categories preserving composition and identity. Functors come in covariant and contravariant flavours.

Natural transformation — a “morphism between functors”. $\eta :F\Rightarrow G$ assigns to each object $X$ a morphism ${\eta }_X:F(X)\to G(X)$ commuting with $F$ and $G$ on morphisms.

Yoneda lemma. $\mathrm{Nat}(\mathrm{Hom}(X,-),F)\cong F(X)$. An object is determined (up to isomorphism) by its hom-functor — “you are what you map to”. Foundational.

Adjoint functors. $F⊣G$ ($F$ left adjoint to $G$) iff there is a natural isomorphism $\mathrm{Hom}(F(X),Y)\cong \mathrm{Hom}(X,G(Y))$. Free / forgetful constructions, currying, tensor / hom, are all adjunctions.

Monads. Endofunctor $T$ with $\mathrm{unit}:\mathrm{Id}\to T$ and $\mathrm{mult}:T\circ T\to T$ satisfying coherence. Came from algebraic topology; reborn in programming languages (Moggi 1989; Wadler 1992) as a way to structure side effects in pure functional languages.

Foundational alternatives.

• ETCS (Lawvere 1964) — axiomatises the category of sets rather than membership directly.
• Topos theory — generalises set theory; a topos is a “category that behaves like Sets”. Subobject classifier, Yoneda, geometric morphisms.
• (∞, 1)-categories and higher topos theory — Lurie’s modern synthesis. Underlies derived algebraic geometry.

This is a one-paragraph pointer; for the working mathematician’s introduction, see Mac Lane, Categories for the Working Mathematician (2nd ed., 1998), or Riehl, Category Theory in Context (2016). Within this Compendium, see algebraic-geometry-foundations for category theory applied to schemes and sheaves.

12. Philosophical foundations debate

The early 20th century saw three competing visions of what mathematics is:

School	Key figures	Claim
Logicism	Frege, Russell, Whitehead	Mathematics reduces to logic
Formalism	Hilbert	Mathematics is formal manipulation of symbols; meaning is irrelevant; consistency is everything
Intuitionism	Brouwer, Heyting	Mathematics is mental construction; classical logic over-reaches

Gödel’s theorems sank strong formalism and pure logicism: arithmetic cannot be reduced to bare logic (Russell’s type theory needed an axiom of infinity, hence not “pure logic”) and no formal system captures all arithmetic truth. Set theory (ZFC) became the practical foundation by default.

Contemporary positions are often more nuanced — structuralism (Benacerraf 1965, Shapiro 1997) asks “what is the number 2?” and answers “the position labelled ‘2’ in any progression structure”; naturalism treats mathematics empirically. See epistemology and philosophy-of-mind-and-language for the philosophical literature.

13. Foundational results timeline

Year	Result	Originator
1854	Algebra of logic	Boole
1879	Predicate calculus	Frege (Begriffsschrift)
1889	Peano axioms for ℕ	Peano
1895-7	Set theory + cardinal arithmetic	Cantor
1901	Russell’s paradox	Russell
1908	First ZFC axiomatisation	Zermelo
1910-13	Principia Mathematica	Russell + Whitehead
1915-22	Löwenheim-Skolem; Replacement	Löwenheim, Skolem, Fraenkel
1920s	Hilbert’s programme	Hilbert
1929	Completeness of FOL	Gödel
1931	Incompleteness theorems	Gödel
1933	Tarski’s truth definition	Tarski
1934	Sequent calculus; cut elimination	Gentzen
1934-6	Recursive functions; Church-Turing	Church, Turing, Kleene
1936	Halting problem undecidable	Turing
1940	Consistency of CH with ZFC	Gödel
1948	Decidability of real closed fields	Tarski
1955	Word problem in groups undecidable	Novikov
1963	Cohen forcing; independence of CH	Cohen
1965	Categoricity theorem	Morley
1969-70	Curry-Howard correspondence	Howard
1970	Hilbert’s 10th undecidable	Matijasevich
1971	NP-completeness	Cook
1972	Martin-Löf type theory	Martin-Löf
1977	Paris-Harrington	Paris + Harrington
1985	Resolution lower bounds	Haken
1995	Ten Thousand Year Clock… I mean Lean 0.1 ;)	(placeholder skip)
2006-13	Univalent foundations / HoTT	Voevodsky et al.
2012	Feit-Thompson formalised in Coq	Gonthier et al.
2017	Liquid tensor experiment in Lean (begun)	Scholze, Commelin, et al.

14. Pitfalls and folklore

• Gödel’s theorems do not say “mathematics is uncertain” — they say no single formal system captures all truth. Mathematics keeps working.
• “True but unprovable” depends on a notion of truth (typically: in the standard model of arithmetic). It does not say a statement is “true in some absolute sense beyond formalisation”.
• The continuum hypothesis being independent does not make it meaningless — it can be settled by adopting new axioms (e.g. forcing axioms, large cardinals).
• Axiom of choice is not pathological — it is needed for most working analysis. The Banach-Tarski paradox uses non-measurable sets, which never arise in concrete analysis.
• Higher-order logic is not “stronger first-order logic” — it’s a different beast, with its own completeness story (Henkin semantics restores completeness; full semantics does not have it).
• Naïve set theory still works for pedagogy at low foundational stakes — Russell’s paradox needs unrestricted comprehension over impredicative properties.
• Constructive mathematics is not “weak classical mathematics” — every classical theorem has a constructive version, but the statement may be subtler.
• Proof assistants do not eliminate human judgement — they verify the steps, not the axioms, definitions, or conjectures.
• Decidability is a property of a theory, not of a problem in the abstract — “is 17 prime?” is trivially decidable; “is this Diophantine equation solvable?” is undecidable.
• Computability and complexity are distinct — undecidable problems are “uncomputable in finite time”; NP-hard problems are “computable but probably slowly”.

15. Further reading

• Enderton, A Mathematical Introduction to Logic (2nd ed., 2001) — standard undergraduate text covering propositional + first-order logic, model theory, computability.
• Mendelson, Introduction to Mathematical Logic (6th ed., 2015) — alternative classical introduction.
• Shoenfield, Mathematical Logic (1967, reprint 2001) — denser graduate text.
• Kunen, Set Theory (2nd ed., 2011) — modern set-theory textbook, forcing included.
• Jech, Set Theory: The Third Millennium Edition (2002) — encyclopaedic reference.
• Sipser, Introduction to the Theory of Computation (3rd ed., 2012) — definitive computability + complexity textbook.
• Soare, Recursively Enumerable Sets and Degrees (1987) — classical computability theory.
• Marker, Model Theory: An Introduction (2002) — modern model theory.
• Troelstra + Schwichtenberg, Basic Proof Theory (2nd ed., 2000) — proof theory reference.
• Awodey, Category Theory (2nd ed., 2010) — accessible introduction.
• Mac Lane, Categories for the Working Mathematician (2nd ed., 1998) — classic.
• HoTT Book — Homotopy Type Theory: Univalent Foundations of Mathematics (open access, 2013).
• Sørensen + Urzyczyn, Lectures on the Curry-Howard Isomorphism (2006) — the proofs-as-programs story.
• Smullyan, Gödel’s Incompleteness Theorems (1992) — accessible mid-level treatment.

16. Companion notes in this library

• number-theory — concrete arithmetic that Gödel encodes.
• algebraic-geometry-foundations — sheaves, schemes, categorical foundations.
• group-theory-and-representation — algebraic structures whose theories live inside FOL.
• measure-theory-and-integration — analysis foundations; uses choice / DC.
• functional-analysis — Hahn-Banach, Tychonoff, equivalent to AC.
• coq, lean, agda, idris — proof assistant / dependently-typed language notes.
• haskell — Curry-Howard intuitions live in the type system.
• epistemology — what counts as knowing a proof.
• philosophy-of-mind-and-language — logic as analysis of language and thought.
• philosophy-of-science — Hempel, Carnap, Quine, the role of formal logic in scientific method.