Mathematical Logic: Intermediate

Type theory and proof theory

About this level

At the Intermediate level we step into the theory that underpins modern proof assistants. Simple type theory = higher-order logic (HOL) is the basis of HOL Light and Isabelle/HOL, while the sequent calculus and cut elimination and strong normalization / termination give the heart of proof theory: why type checking always terminates and why proofs can be mechanically normalized. Finally, with the LCF architecture (a small trusted kernel plus untrusted tactics) as the axis, we survey how the foundations of HOL Light / Isabelle / Coq / Lean differ.

Prerequisites

Contents

Simple Type Theory = HOL

The basis of higher-order logic.

  • Simple types and Church's types
  • Higher-order quantification
  • The basis of HOL Light / Isabelle

Sequent Calculus & Cut Elimination

The main theorem of proof theory.

  • The sequent $\Gamma \vdash \Delta$
  • The cut rule and its elimination
  • The subformula property

Strong Normalization & Termination

Computation always terminates.

  • Normal forms and reduction
  • The strong normalization theorem
  • Decidability of type checking

Computability & Decidability

What a machine can decide.

  • Decidable and semi-decidable
  • The halting problem
  • Type checking vs. proof checking

Proof Assistants & LCF

Trust only a small kernel.

  • The LCF architecture
  • HOL Light / Isabelle / Coq / Lean
  • Tactics are not trusted

Next step

Once you have grasped HOL, cut elimination, and the LCF architecture, move on to the Advanced level to study dependent type theory (MLTT / CIC), Gödel's incompleteness theorems, the de Bruijn criterion and the TCB, and a comparison of ZFC, HOL, and type theory. For a worked proof-assistant example, see also Proving with Lean.