Abstract
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!
License
Topics
Related publications
- Kumar, R., Arthan, R., Myreen, M. O., & Owens, S. (2016). Self-Formalisation of Higher-Order Logic. Journal of Automated Reasoning, 56(3), 221–259. https://doi.org/10.1007/s10817-015-9357-x
- Kumar, R., Arthan, R., Myreen, M. O., & Owens, S. (2014). HOL with Definitions: Semantics, Soundness, and a Verified Implementation. Interactive Theorem Proving, 308–324. https://doi.org/10.1007/978-3-319-08970-6_20
- Andrews, P. B. (1986). An introduction to mathematical logic and type theory: to truth through proof, ISBN 978-0-12-058535-9.
- Díaz, J. (2023). Metatheory of Q0, AFP entry.