Mathematical Logic.

What logic is.

The mathematical study of mathematical reasoning.

Logic, before 1850, was philosophy — Aristotle's Organon, the Scholastic syllogistic tradition, Leibniz's dream of a universal calculus. Logic, after 1879, is mathematics. The change came when George Boole and Gottlob Frege showed that inference itself could be made the object of formal calculation.

The four classical pillars of mathematical logic are set theory, model theory, proof theory, and recursion theory (computability). Each studies a different aspect of formal mathematics; the four interlock through Gödel's theorems, the Church-Turing thesis, and the Cohen forcing technique.

This deck moves through the founders, the great results, and the working subfields. It tries to say accurately what Gödel proved — and to clear the air of the things he is often falsely said to have proved.

Aristotle's syllogisms.

The founding text is Aristotle's Prior Analytics (c. 350 BCE). The atomic unit is the syllogism: two premises and a conclusion, related by quantified subject-predicate forms (All A are B, Some A is B, No A is B, Some A is not B).

Aristotle classified the valid moods — there are 24, though the medievals named only 19 — and gave the first deductive system in the West. Stoic logic, especially Chrysippus (c. 280–207 BCE), independently developed propositional logic with conditionals.

The system was sufficient for two thousand years and conspicuously insufficient for mathematics. Every line through a point parallel to a given line is unique involves a multiply-quantified statement that no Aristotelian syllogism can express. The mismatch was felt for centuries before it was repaired.

The algebra of logic.

George Boole's An Investigation of the Laws of Thought (1854) was the first treatment of logic as algebra. Boole let propositions be variables taking values 0 or 1, with multiplication for AND, addition (with x + x = x) for OR, and 1 − x for NOT. Logical inference became algebraic manipulation.

The system was incomplete by modern standards — it handled propositional logic but not quantification — and it had idiosyncrasies. But it founded a tradition. De Morgan's laws were stated in this period (1847). C. S. Peirce and Ernst Schröder extended Boole's algebra through the late 19th century.

Boolean algebra was unlikely to change mathematics on its own. It changed engineering. Claude Shannon's 1937 master's thesis showed that switching circuits realise Boolean expressions, and the digital computer became a possibility.

Begriffsschrift.

The single most important book in the history of logic. Gottlob Frege's Begriffsschrift (1879) — "concept-script" — was the first system in which mathematical reasoning could be carried out in completely formal symbolic terms.

Frege introduced quantifiers (∀, ∃) and variable binding, formalising "for all x" and "there exists x" with a precision Aristotle could not. He gave the first complete system of predicate logic, including a deduction calculus. He distinguished function from argument in a way that prefigures lambda calculus.

The book was nearly unreadable. Its two-dimensional notation was abandoned within a generation. But its mathematical content — that a logical system can be made a formal object of study — opened every gate that followed. Russell, Whitehead, Hilbert, Gödel, Tarski, Church, Turing all walked through it.

Russell's paradox.

Frege had nearly completed the second volume of his Grundgesetze der Arithmetik when, in June 1902, he received a letter from Bertrand Russell describing a contradiction in his system. Frege replied: "Arithmetic totters."

The set of all sets that do not contain themselves contains itself if and only if it does not. The paradox shows that unrestricted comprehension — forming a set from any predicate — is logically inconsistent.

Frege's project was holed below the waterline. The set-theoretic foundation of mathematics needed reconstruction. Two responses dominated the next thirty years: Russell's theory of types, and Zermelo's axiomatic set theory.

Principia Mathematica.

Three volumes, by Alfred North Whitehead and Bertrand Russell, attempting to derive all of mathematics from logical axioms. Volume I (1910), Volume II (1912), Volume III (1913). A fourth on geometry was announced and never completed.

The system used a ramified theory of types to evade the paradoxes. Each variable was tagged with a type level; sets could only contain entities of lower type, blocking self-membership. The technical price was high — the famously laborious proof, on page 86 of Volume II, that 1 + 1 = 2 "is occasionally useful."

Principia was the most influential and least-read book in 20th-century logic. It demonstrated that the foundational programme was technically feasible. It also demonstrated that the foundational programme was excruciating. Within twenty years, simpler axiomatisations had displaced it for working mathematicians, while logicians began to ask whether the programme could ever be completed at all.

A finitary foundation.

David Hilbert's response to the foundational crisis was a programme: prove the consistency of all mathematics by purely finitary reasoning — methods involving only finite, surveyable, combinatorial objects. If finitary methods could prove that no contradiction can be derived from the axioms of arithmetic, the rest of mathematics would be safe.

Hilbert posed three questions about any sufficiently rich formal system:

1. Consistency. Can a contradiction be derived?
2. Completeness. Is every true statement provable?
3. Decidability (the Entscheidungsproblem). Is there an algorithm that, given any statement, decides whether it is provable?

Hilbert expected the answers to be no, yes, yes. The answers turned out to be more complicated. The 1930s would settle them in one of the most concentrated bursts of foundational mathematics ever recorded.

Incompleteness.

A 25-year-old Kurt Gödel proved, in his 1931 paper "Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I," that Hilbert's expectation was wrong.

The technique: arithmetisation of syntax. Gödel showed how to encode formulas and proofs as natural numbers — what is now called Gödel numbering. Statements about provability become arithmetic statements. The system can talk about itself.

From this self-reference, Gödel constructed a sentence G that, decoded, says This sentence has no proof in the system. If the system is consistent, G is true but unprovable. If the system proves G, the system is inconsistent.

The result was decisive. No formal system rich enough to express arithmetic can be both consistent and complete. Hilbert's second question is answered: no.

The first incompleteness theorem.

Stated cleanly: any consistent formal system in which a sufficient amount of elementary arithmetic can be carried out is incomplete. There exist statements in the language of the system that the system can neither prove nor disprove.

Three subtleties matter.

One. "Sufficient amount of arithmetic" means roughly Robinson arithmetic — a very weak fragment. The result applies to PA, ZFC, and any extension. It does not apply to systems too weak to encode their own syntax.

Two. Truth and provability are different. The Gödel sentence G is true (it correctly asserts that it has no proof) but unprovable. Tarski's 1933 theorem on the undefinability of arithmetical truth is the deeper companion result.

Three. The statement is conditional. If the system is consistent, then it is incomplete. The first incompleteness theorem does not establish consistency.

The second incompleteness theorem.

The deeper result, also in Gödel's 1931 paper. Any sufficiently rich consistent formal system cannot prove its own consistency.

The proof passes through the first theorem. The statement I am consistent can be encoded as an arithmetical formula. If the system could prove this formula, it could also prove the Gödel sentence — but if it proved the Gödel sentence, it would be inconsistent.

Hilbert's programme, in its strict form, dies here. The hope was to prove the consistency of mathematics by finitary methods. Finitary methods are a fragment of arithmetic. So no finitary argument can establish the consistency of arithmetic. Any consistency proof must use methods beyond what it certifies.

Gentzen (1936) proved the consistency of arithmetic using transfinite induction up to the ordinal ε₀ — a strictly stronger principle than arithmetic itself. The trade is real, the result is interesting, and Hilbert's original ambition is foreclosed.

What Gödel did not prove.

The two incompleteness theorems are among the most over-cited results in mathematics. The most common popular misreadings:

"Gödel proved mathematics is inconsistent." No. He proved that consistent systems strong enough to encode arithmetic cannot prove their own consistency. Mathematics is presumed consistent; we just cannot certify it from inside.

"Gödel proved there are truths that can never be known." No. The Gödel sentence of one system is provable in a stronger system. Nothing in Gödel's work places a permanent limit on human knowledge. It places a limit on what any single formal system can certify about itself.

"Gödel refuted artificial intelligence." No. The Penrose-Lucas argument — that Gödel's theorems show human minds transcend any algorithm — has been criticised on technical grounds for sixty years. The minimum charge: the argument requires the assumption that human mathematical reasoning is consistent, which is itself uncertifiable.

Read Torkel Franzén's Gödel's Theorem: An Incomplete Guide to Its Use and Abuse (2005) before invoking the results in any non-mathematical setting.

Tarski and truth.

Alfred Tarski's "The Concept of Truth in Formalised Languages" (1933, Polish; 1956, English) gave the first satisfactory definition of truth for a formal language.

The schema: a sentence S is true if and only if [what S says is the case]. The sentence "Snow is white" is true iff snow is white. The schema is trivial; the work is in giving it precise content for an arbitrary formal language.

Tarski's main results: (1) truth for a formal language can be defined within a stronger metalanguage by structural recursion on formulas; (2) truth for arithmetic cannot be defined within arithmetic itself. The second result — Tarski's undefinability theorem — explains why Gödel's incompleteness theorems must speak of provability rather than truth.

Tarski founded model theory in the same period: the systematic study of structures that satisfy formal sentences.

The Turing machine.

Hilbert's third question — the Entscheidungsproblem — was resolved in 1936 by two independent answers.

Alan Turing's "On Computable Numbers, with an Application to the Entscheidungsproblem" defined a precise model of mechanical computation: an automaton with an infinite tape, a finite state machine, and a head that reads, writes, and moves. A function is computable if some Turing machine eventually halts and outputs its value.

Turing showed that the question Does this Turing machine halt? is not itself computable — the halting problem. From this it follows that the Entscheidungsproblem is undecidable: no algorithm can determine whether an arbitrary statement of first-order logic is provable. Hilbert's third question is answered: no.

The same paper accidentally invented the universal computer, by exhibiting a Turing machine that simulates any other when fed its description as input.

The halting problem.

Suppose, for contradiction, that a program H exists which, given any program P and input I, returns 1 if P halts on I and 0 otherwise.

D's behaviour on itself contradicts H's verdict either way. So H cannot exist.

The halting problem is the prototype of an undecidable problem. Many natural questions reduce to it — the word problem for groups (Novikov 1955), Hilbert's tenth problem on Diophantine equations (Matiyasevich 1970), and questions about formal grammars and tilings. Where there is undecidability in mathematics, the halting problem is usually nearby.

Church's lambda calculus.

The other answer to the Entscheidungsproblem, also 1936, was Alonzo Church's. The lambda calculus is a formalism in which every expression is either a variable, a function abstraction λx.M, or an application M N. Computation is repeated substitution.

The system is small — three syntactic forms, one rewriting rule (β-reduction) — and Turing-complete. Church proved the same negative result as Turing about the Entscheidungsproblem using lambda calculus.

The lambda calculus turned out to be the founding formal language of computer science. Lisp (McCarthy, 1958) is a thinly-veiled lambda calculus; Haskell, OCaml, and the functional core of every modern language descend from it. The Curry-Howard correspondence (1969) revealed that lambda terms are proofs in intuitionistic logic — programs and proofs are the same thing.

The Church-Turing thesis.

Turing machines and lambda calculus, defined in 1936 in different countries with different motivations, compute exactly the same class of functions. Adding any reasonable mechanical model — Post systems, register machines, partial recursive functions — yields the same class.

The Church-Turing thesis is the empirical claim that this class is precisely the class of effectively calculable functions — the functions a human or machine can compute by mechanical procedure.

The thesis is not a theorem. It cannot be, since "effectively calculable" is an informal notion. But every model of computation proposed in the ninety years since 1936 — including quantum computers, in the relevant sense — has been Turing-equivalent. No counter-example exists. Most working logicians and computer scientists treat the thesis as established.

Recursion theory.

The branch of logic concerned with the structure of computability. Founded by Kleene and Post in the 1940s; matured under Sacks, Soare, and Shore from the 1960s.

The main hierarchy is the arithmetical hierarchy, classifying sets of natural numbers by the number of quantifier alternations needed to define them. Σ⁰₁ sets are computably enumerable; Π⁰₁ are co-c.e.; Δ⁰₁ are computable; the higher levels — Σ⁰_n, Π⁰_n — strictly increase in complexity.

Beyond arithmetic lies the analytical hierarchy (quantifying over functions) and degrees of unsolvability — Turing degrees — measuring relative computability. The structure of the Turing degrees is one of the richest objects in foundational mathematics.

Set theory and the ZFC axioms.

Ernst Zermelo's 1908 axiomatisation of set theory, refined by Fraenkel in 1922 and supplemented by the axiom of choice, became the standard foundation of modern mathematics. ZFC has nine axioms (counting Replacement as a schema).

Extensionality. Empty Set. Pairing. Union. Power Set. Infinity. Replacement. Foundation. Choice.

The system is rich enough to formalise essentially all of mathematics — analysis, algebra, topology, even most of category theory if one is careful about size. It is also strong enough to fall under Gödel's incompleteness theorems: there are statements of ZFC that ZFC can neither prove nor disprove (assuming ZFC is consistent).

The most famous such statement is the continuum hypothesis. The next.

The continuum hypothesis.

Cantor's 1878 conjecture: there is no set whose cardinality lies strictly between that of the integers and that of the real numbers. Equivalently, 2^ℵ₀ = ℵ₁.

Hilbert listed it as the first of his 23 problems in 1900. Gödel proved in 1940 that CH is consistent with ZFC by constructing the constructible universe L — every set that can be built by transfinite iteration of definable operations from the empty set. CH holds in L.

Paul Cohen proved in 1963 that the negation of CH is also consistent with ZFC. He invented the technique of forcing — adding "generic" sets to a model of ZFC in a controlled way — and used it to construct a model where 2^ℵ₀ exceeds ℵ₁ by any prescribed amount.

CH is therefore independent of ZFC. Cohen received the Fields Medal in 1966 — the only one ever awarded for work in pure logic.

The technique of forcing.

Cohen's method has become the dominant tool of modern set theory. The intuition: start with a countable model M of ZFC. To add a new set G with controlled properties, work with a partial order P inside M whose elements are "approximations" to G. A generic filter on P picks G from outside M; the resulting larger model M[G] still satisfies ZFC, but G can be made to satisfy or violate any desired statement consistent with the constraints encoded in P.

Forcing has produced hundreds of independence results. Most natural set-theoretic statements about cardinals between ℵ₀ and 2^ℵ₀ are independent of ZFC. The Suslin hypothesis, the Kurepa tree, the existence of P-points in the Stone-Čech compactification — all settled by forcing.

The technique is technically demanding but conceptually clean: forcing makes the universe of sets feel less like a fixed structure and more like a malleable object that can be expanded in many compatible directions.

Large cardinal axioms.

To settle the questions ZFC leaves open, set theorists have proposed large cardinal axioms — assertions of the existence of cardinals so large that their existence cannot be proved in ZFC.

The hierarchy: inaccessible, Mahlo, weakly compact, measurable, Woodin, supercompact, huge, ascending towards a (consistent) point and finally to Reinhardt and Berkeley cardinals (whose ZFC-consistency is unknown or, in Reinhardt's case, refuted).

The hierarchy has the remarkable property of being linearly ordered by consistency strength: stronger axioms imply the consistency of weaker ones, and most natural large cardinal axioms fit on a single tower. This provides a measuring stick for mathematical statements: determinacy of analytic sets, for example, has the same consistency strength as the existence of a measurable cardinal (Martin, 1970).

Whether the universe of sets actually contains large cardinals is a question the axioms cannot decide. The bet, among most contemporary set theorists, is that they do.

Model theory.

Model theory studies structures that satisfy formal sentences — what kinds of mathematical objects can be characterised by what kinds of axioms.

The two foundational results are the Löwenheim-Skolem theorem (every consistent first-order theory with an infinite model has models of every infinite cardinality) and the compactness theorem (a set of first-order sentences has a model iff every finite subset does).

Modern model theory, after Morley (1965), classifies theories by stability and uses the resulting structure to attack problems in algebra and geometry. The discipline has produced remarkable applications: Hrushovski's 1996 model-theoretic proof of the geometric Mordell-Lang conjecture in characteristic p; the use of o-minimality in the Pila-Wilkie theorem and Tate's conjecture for products of elliptic curves.

Model theory has become one of the most successful exporters of logical methods to mainstream mathematics.

Proof theory.

The branch concerned with formal proofs as combinatorial objects. Founded by Hilbert in the 1920s and matured by Gentzen, who introduced natural deduction and sequent calculus in 1934.

The central technical result is cut elimination (Gentzen's Hauptsatz): every proof in sequent calculus can be transformed into a cut-free proof. Cut-free proofs have the subformula property — every formula appearing in the proof is a subformula of some formula in the conclusion. The result trivialises decision procedures for many propositional logics.

Proof theory underlies modern programming-language theory through the Curry-Howard correspondence: types are propositions, programs are proofs, evaluation is cut elimination. Linear logic (Girard, 1987) and homotopy type theory (Voevodsky and others, 2010s) are recent flowerings of the same root.

Type theory and constructive logic.

Russell's theory of types (1908) was the first; Per Martin-Löf's intuitionistic type theory (1972) is the modern descendant. In Martin-Löf type theory, every term has a type, propositions are types, and the rules of inference correspond to typing rules.

The system is constructive: a proof of an existence statement must exhibit a witness; a proof of a disjunction must say which disjunct holds. There is no law of excluded middle and no proof by contradiction in the classical form. The price is power; the reward is computational content — every proof is automatically a program.

Modern proof assistants — Coq, Agda, Lean — are based on dependent type theories descended from Martin-Löf. They have been used to formalise the four-color theorem (Gonthier 2005), the Feit-Thompson theorem (Gonthier 2012), and the Kepler conjecture (Hales 2017).

Modal logic.

Logic with operators □ ("necessarily") and ◇ ("possibly"). Origins in Aristotle and the medievals; modern formalisation by C. I. Lewis (1918). Saul Kripke's 1959 semantics — a frame of "possible worlds" with an accessibility relation — gave modal logic the technical machinery that made it useful.

Modal logic has many applications. Provability logic: read □ as "is provable in PA," and Gödel's theorems give axioms; Solovay (1976) proved that the modal logic GL captures the propositional content of provability exactly. Epistemic logic: read □ as "it is known that"; temporal logic: read □ as "it will always be the case that." Both are used heavily in computer science for verification and AI.

Branches of modal logic are now native to philosophy (counterfactuals), linguistics (modality and tense), and economics (game-theoretic reasoning about beliefs about beliefs).

Coq, Lean, and machine-checked mathematics.

The proof assistants are no longer toys. Coq (INRIA, 1989–) was used by Georges Gonthier to formally verify the four-color theorem (2005) and the odd-order theorem (2012). Lean (Microsoft Research, 2013–; now under the Lean FRO) is the rising star.

The Liquid Tensor Experiment (Scholze, 2020) asked the Lean community to verify a key theorem in condensed mathematics. The community succeeded in 2022. Terence Tao has formalised the Polynomial Freiman-Ruzsa conjecture (his joint work with Green and others) in Lean. Kevin Buzzard's ongoing project aims to formalise the proof of Fermat's Last Theorem.

The premise — that the foundations of mathematics will, by 2050, be checked by software — was fringe in 2010 and is now mainstream. The acceleration is due as much to the maturity of dependent type theory as to the willingness of working mathematicians to engage.

Logic in computer science.

Logic is to computer science what calculus is to physics. Three places it appears:

Verification. Hardware and safety-critical software are verified using model checking (Clarke, Emerson, Sifakis — Turing Award 2007), satisfiability solvers (SAT/SMT), and theorem provers. Intel's hardware verification programme exists because of a 1994 floating-point bug; SAT solvers underpin much of modern systems verification.

Programming language theory. Type systems, semantics of programming languages, and compiler correctness are applied logic. Hindley-Milner type inference, Hoare logic, separation logic, and dependent types all live here.

Databases and knowledge representation. First-order logic is the theoretical core of relational databases. Description logics underlie RDF, OWL, and the Semantic Web. Datalog is enjoying a renaissance in program analysis and machine learning.

Reading list.

• 1854The Laws of ThoughtGeorge Boole
• 1879BegriffsschriftGottlob Frege
• 1910Principia MathematicaWhitehead & Russell
• 1934Investigations into Logical DeductionGerhard Gentzen
• 1949Mathematical LogicWillard Van Orman Quine
• 1952Introduction to MetamathematicsStephen Kleene
• 1972A Mathematical Introduction to LogicHerbert Enderton
• 1979Gödel, Escher, BachDouglas Hofstadter
• 1990Computability and LogicBoolos & Jeffrey
• 1997Set Theory — the standard graduate textThomas Jech
• 2002Model Theory: An IntroductionDavid Marker
• 2005Gödel's Theorem: An Incomplete GuideTorkel Franzén
• 2012Set Theory: An Introduction to Independence ProofsKenneth Kunen
• 2013Homotopy Type TheoryUnivalent Foundations Program
• 2021Theorem Proving in Lean 4Avigad & de Moura

Watch & read.

↑ Marcus du Sautoy on Gödel's incompleteness theorem

More on YouTube

Watch · Computerphile on Turing and the halting problem
Watch · Russell's paradox explained

And read

Franzén's Gödel's Theorem is the only popular book on the incompleteness theorems that gets them right. Boolos & Jeffrey's Computability and Logic is the cleanest one-volume introduction to the technical material. For set theory, Jech (graduate) or Hrbacek-Jech (undergraduate). Hofstadter's Gödel, Escher, Bach remains the best entry point for non-specialists who care about the music of the subject more than the formalism.

The constants.

What mathematical logic has taught:

1. Reasoning is a formal object. Frege's lesson. The same techniques used to study numbers can be turned on the proofs that talk about them.

2. Self-reference is a recurring source of paradox and of theorem. The Liar, Russell, Gödel, the halting problem, and the Y combinator are all variants of one trick.

3. Some mathematical questions are not answerable from any plausible foundation. CH, Suslin, and many natural questions in set theory are independent of ZFC. The universe of sets is plural in a way that cannot be reduced.

4. Computation and proof are the same thing. Curry-Howard. Programs are proofs, types are propositions, evaluation is normalisation. The deepest result of the subject and still under-appreciated outside specialists.

5. Logic is becoming the meta-language of mathematics. The Lean libraries are not toy projects. The proofs of 2050 will be machine-checked.