Mathematical Logic
The mathematics of proof, types, and computation
About this series
Mathematical logic is the field that rigorously treats mathematical "reasoning" and "proof" themselves as objects of mathematics. It answers questions such as "what is a proof?", "what do we take as the foundation of trust?", and "which logical basis do we choose?" with the theory of formal systems.
This series begins at the entrance of distinguishing syntax and semantics of formal systems, then proceeds through natural deduction, soundness and completeness, the λ-calculus and type theory, the Curry–Howard correspondence, dependent type theory, Gödel's incompleteness theorems, and on to the de Bruijn criterion, the trusted computing base (TCB), and the design of proof assistants. Ultimately it aims to trace, step by step, the path from the entrance to the current state of modern theorem provers — up to the design of a proof-checking kernel built on constructive reals.
This series is adjacent to the existing Proof series (which teaches how to write proofs), Set Theory, and Theory of Computation. Whereas the Proof series covers "how to write a proof," this series covers "what a proof is and how a machine checks it."
Learning by level
The learning flow
Main topics
Syntax and semantics
The distinction between manipulating symbols (syntax) and what they mean (semantics). The starting point for understanding a formal system.
Proof = program
The Curry–Howard correspondence. Propositions are types, proofs are terms, reduction is computation. The backbone of type-theory-based proof systems.
Soundness and completeness
When "provable" coincides with "valid under a given semantics". The two bridges connecting syntax and semantics. Gödel's completeness theorem, about first-order logic itself, is a different statement from the incompleteness theorems, which are about particular formal systems.
Limits of systems
Gödel's incompleteness theorems. A consistent formal system that can express enough arithmetic cannot, under suitable conditions, prove its own consistency inside that system.
Trusted computing base (TCB)
The de Bruijn criterion, a small checking kernel, and "generator → checker." What must you trust to trust a proof?
Three major foundational frameworks
ZFC (set theory), HOL (higher-order logic), and type theory: the main options for building mathematics and how they differ (category-theoretic foundations and HoTT/UF are further alternatives).
Why study mathematical logic
There are several reasons to study mathematical logic:
- The nature of proof: understand "what a proof is" formally, not just intuitively
- The foundation of trust: learn which axioms and rules suffice to build mathematics
- Correspondence with computation: through Curry–Howard, see the deep correspondence between logical proofs and typed computation
- Proof assistants: understand the theoretical basis of Coq, Lean, Isabelle, and HOL Light
- Formal verification: learn the principles behind large-scale verifications such as seL4, CompCert, and Flyspeck
Related and applied fields
- Proof assistants: Coq, Lean, Agda, Isabelle, HOL Light
- Formal verification: OS kernels (seL4), compilers (CompCert), mathematical theorems (Flyspeck)
- Programming language theory: type systems, type safety, dependent types
- Foundations of mathematics: connections with set theory, model theory, and recursion theory
- Mathematics by computer: constructive mathematics, the design of proof-checking kernels
Frequently Asked Questions
What is mathematical logic
Mathematical logic rigorously studies mathematical reasoning, proof, and computation themselves as objects of mathematics. It treats the syntax and semantics of formal systems, the structure of proofs (proof theory), the correspondence between logic and types/programs (type theory and the Curry–Howard correspondence), and the limits of systems (the incompleteness theorems), providing the theoretical foundation for proof assistants and formal verification.
What does it mean that a proof and a program are the same thing
The Curry–Howard correspondence is the discovery that propositions correspond to types, proofs to programs (terms) of those types, and proof reduction to computation. A proof of 'A implies B' corresponds to 'a function that takes an input of type A and produces an output of type B.' This correspondence is the backbone of type-theory-based proof assistants such as Coq, Lean, and Agda.
What is the difference between soundness and completeness
Soundness means 'what is provable is true' (the proof system derives no falsehoods); completeness means 'what is true is provable' (no truth is missed). Here 'true' means valid under a given semantics. When both hold, 'provable' and 'valid' coincide, and syntax (proof) and semantics (truth) agree. First-order logic, for instance, has Gödel's soundness and completeness theorems for its standard semantics.
Why do proof assistants base their trust on a small kernel
This is the idea of the LCF architecture: trust only a small core (the trusted computing base, TCB) that checks every proof, and do not trust the tactics that generate proofs. Even if a tactic has a bug, the generated proof is always re-checked by the kernel, so no unsound conclusion gets through (fail-closed). Minimizing the code that must be trusted concentrates the reliability of the whole system in one place.
Do the completeness and incompleteness theorems contradict each other
They do not, because they are about different things. Gödel's completeness theorem is about first-order logic itself: every formula valid under the standard semantics is derivable in the proof system. The incompleteness theorems are about particular formal systems such as arithmetic: inside such a system there are sentences that can be neither proved nor refuted. The first concerns logical validity, the second the limits of what one theory can prove.