Logic and foundations §
Logic and foundations studies the rules of reasoning, the axiomatic structure of mathematics, and the limits of formal systems. It is relevant whenever a problem needs rigorous proof, formal specification, decidability analysis, or a clear understanding of what can and cannot be established within a given framework. It underlies all of mathematics, computer science, and formal verification.
Brief history §
- Antiquity: Aristotle’s syllogistic and Euclid’s axiomatic method.
- 19th century: Boolean algebra, set theory (Cantor), and the formalization of logic (Frege, Peano).
- Early 20th century: Hilbert’s program, Gödel’s incompleteness theorems, and the foundations of computability (Turing, Church).
- 1930s–1960s: the Curry–Howard correspondence (“proofs are programs”) links logic to computation; lambda calculus becomes the bridge between the two.
- Mid-20th century onward: model theory, proof theory, category theory, and type theory expand the landscape.
Logic and foundations is deeply intertwined with Computer Science: type theory underpins programming-language semantics, and computability underpins the theory of algorithms (see Theory of Computation).
Classes §
| Page | Key question | Core objects | How it relates |
|---|---|---|---|
| Mathematical logic | What counts as a valid inference, and what can a formal system prove? | propositional and predicate logic, formal systems, model theory, proof theory, Gödel incompleteness theorems | the meta-discipline that studies formal systems themselves; its incompleteness theorems bound what any foundation (set-theoretic or type-theoretic) can prove |
| Computability and decidability | What can be mechanically decided? | Turing machines, halting problem, arithmetical hierarchy, recursive functions | bounds what proofs and algorithms can achieve; the Computer-Science-side treatment of the same questions lives in Theory of Computation |
| Set theory | What is the universe of mathematical objects? | sets, cardinality, ordinals, axioms (ZFC), large cardinals | the standard foundational language for mathematics; provides the universe in which other structures live; underpins measure theory and hence Probability and statistics |
| Category theory | What is structure, and when do two structures behave the same? | categories, functors, natural transformations, limits, adjunctions | abstracts structure and morphism across all of mathematics; a rival foundation to set theory (topos theory) and the native language of modern algebra |
| Type theory | How do propositions and programs correspond? | type systems, lambda calculus, Curry–Howard correspondence, dependent types, homotopy type theory | an alternative foundational framework at the intersection of logic and computability; underpins programming-language semantics and proof assistants (Coq, Agda, Lean) |
Details
How to use the table as a map. Mathematical logic and Computability and decidability are meta-disciplines: they study formal systems and mechanical procedures from the outside. Set theory, Category theory, and Type theory are foundational languages: each is a language in which mathematics itself can be written, and to a large extent they are rivals — a theorem of one can often be translated into another, but each makes different statements feel natural to express.
Connections to the rest of Mathematics. Set theory underpins measure theory, which in turn underpins Probability and statistics. Category theory supplies the language of algebraic structure used throughout Algebraic and discrete mathematics. On the Computer Science side, type theory underpins programming-language semantics (see Language Theory), and computability underpins the theory of algorithms (see Theory of Computation).
A note on breadth. Mathematical logic and Computability and decidability are each broad enough to become topic pages with their own sub-categorizations; they are listed here as classes until those pages exist. Set theory, Category theory, and Type theory are likewise broad enough to be topic pages of their own.