### 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

BSD License

### Topics

- Logic/General logic

### 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. Lecture Notes in Computer Science, 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.

### Session Q0_Soundness

- Set_Theory
- HOLZF_Set_Theory
- ZFC_in_HOL_Set_Theory
- Q0

### Depends on

- Zermelo Fraenkel Set Theory in Higher-Order Logic

### Auto-related entries

- Metatheory of Q0
- MLSS Decision Procedure
- Category Theory for ZFC in HOL II: Elementary Theory of 1-Categories
- Recursion Theorem in ZF
- Auto2 Prover

## Cite

×

Q0_Soundness-AFP

    @article{Q0_Soundness-AFP,
      author  = {Anders Schlichtkrull},
      title   = {Soundness of the Q0 proof system for higher-order logic},
      journal = {Archive of Formal Proofs},
      month   = {November},
      year    = {2023},
      note    = {\url{https://isa-afp.org/entries/Q0_Soundness.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest