Soundness of the Q0 proof system for higher-order logic.

Research output: Contribution to journalJournal articleResearchpeer-review


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!
Original languageEnglish
JournalArchive of Formal Proofs
Publication statusPublished - 2023


Dive into the research topics of 'Soundness of the Q0 proof system for higher-order logic.'. Together they form a unique fingerprint.

Cite this