Metatheory of Q0

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.