Soundness of the Q0 proof system for higher-order logic

Anders Schlichtkrull 🌐

November 20, 2023

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


This entry formalizes the Q0 proof system for higher-order logic (also known as simple type theory) from the book "An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof" by Peter B. Andrews together with the system's soundness. Most of the used theorems and lemmas are also from his book. The soundness proof is with respect to general models and as a consequence also holds for standard models. Higher-order logic is given a semantics by porting to Isabelle/HOL the specification of set theory by Kumar et al. from the CakeML project. The independently developed AFP entry "Metatheory of Q0" by Javier Díaz also formalizes Q0 in Isabelle/HOL. I highly recommend the reader to also take a look at his formalization!


BSD License


Related publications

Session Q0_Soundness