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. Higher-order logic (HOL), whose term language is the simply typed λ-calculus, 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: when and why reduction terminates, and how that termination underpins the decidability of type checking. Finally, with the LCF architecture (a small trusted kernel plus untrusted tactics) as the axis, we survey how the foundations of HOL Light / Isabelle/HOL / 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

A central theorem of Gentzen-style proof theory.

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

Strong Normalization & Termination

When and why reduction 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.