Metatheory of Q0

Javier Díaz 📧

November 4, 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 is a formalization of the metatheory of \(\mathcal{Q}_0\) in Isabelle/HOL. \(\mathcal{Q}_0\) is a classical higher-order logic equivalent to Church's Simple Theory of Types. In this entry we formalize Chapter 5 of "An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof" (Andrews, 2002), up to and including the proofs of soundness and consistency of \(\mathcal{Q}_0\). These proof are, to the best of our knowledge, the first to be formalized in a proof assistant.


BSD License


Session Q0_Metatheory