Email Gateway (Nov 26 2023 at 10:32): Email Gateway (Nov 26 2023 at 10:32):From: Dmitriy Traytel <traytel@di.ku.dk>
Anders Schlichtkrull has formalized the soundness of Q0 (for meta-assumption-less theorems):
Soundness of the Q0 proof system for higher-order logic
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!
https://www.isa-afp.org/entries/Q0_Soundness.html
An independent formalization of the same result and more by Javier Díaz (https://www.isa-afp.org/entries/Q0_Metatheory.html) has appeared in the AFP recently. Anders’ formalization was part of IsaFoL (https://github.com/IsaFoL/IsaFoL) for more than a year. One interesting aspect is that Anders uses a formalization of set theory inspired by CakeML, and shows that it is consistent with the two existing axiomatizations (HOLZF and ZFC_in_HOL).
Enjoy!
Last updated: Apr 29 2024 at 01:08 UTC