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

Research output: Contribution to journalJournal articleResearchpeer-review

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

Fingerprint

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

Cite this