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' can be identified with '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). When both hold, 'provable' and 'true' coincide, and syntax (proof) and semantics (truth) agree.

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.

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 (proof theory), 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

Introduction

The gateway to the concepts

The syntax/semantics distinction
Propositional and predicate logic
What a proof is (formally)
A gentle introduction to Curry–Howard

Basic

Systems of proof

Natural deduction (introduction/elimination rules)
Soundness and completeness
Introduction to the λ-calculus
Intuitionistic vs. classical logic

Intermediate

Type theory and proof theory

Simple type theory = HOL
Sequent calculus and cut elimination
Strong normalization and termination
Proof assistants overview and LCF

Advanced

Comparing foundations and their limits

Dependent type theory (MLTT / CIC)
Gödel's incompleteness theorems
The de Bruijn criterion and TCB
ZFC vs. HOL vs. type theory

Readings & Cases

Concrete examples and the current state

Two proofs of the addition formula
Examples of formal verification
What makes verification trustworthy
The design of a proof-checking kernel

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" and "true" coincide. The two bridges connecting syntax and semantics.

Limits of systems

Gödel's incompleteness theorems. A sufficiently strong system cannot prove its own consistency.

Trusted computing base (TCB)

The de Bruijn criterion, a small checking kernel, and "generator → checker." What must you trust to trust a proof?

The three foundations

ZFC (set theory), HOL (higher-order logic), and type theory. The options for building mathematics and how they differ.

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
Unity with computation: through Curry–Howard, see that logic and computation are the same thing
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

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