### Abstract

This entry is a formalization of the metatheory of \(\mathcal{Q}_0\) in Isabelle/HOL. \(\mathcal{Q}_0\) is a classical higher-order logic equivalent to Church's Simple Theory of Types. In this entry we formalize Chapter 5 of "An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof" (Andrews, 2002), up to and including the proofs of soundness and consistency of \(\mathcal{Q}_0\). These proof are, to the best of our knowledge, the first to be formalized in a proof assistant.

### License

BSD License

### Topics

- Logic/General logic

### Session Q0_Metatheory

- Utilities
- Syntax
- Boolean_Algebra
- Propositional_Wff
- Proof_System
- Elementary_Logic
- Semantics
- Soundness
- Consistency

### Depends on

- Finite Map Extras
- Zermelo Fraenkel Set Theory in Higher-Order Logic

### Auto-related entries

- Hello World
- The Irrationality of ζ(3)
- Soundness of the Q0 proof system for higher-order logic
- Real Exponents as the Limits of Sequences of Rational Exponents
- A Sequent Calculus for First-Order Logic

## Cite

×

Q0_Metatheory-AFP

    @article{Q0_Metatheory-AFP,
      author  = {Javier Díaz},
      title   = {Metatheory of Q0},
      journal = {Archive of Formal Proofs},
      month   = {November},
      year    = {2023},
      note    = {\url{https://isa-afp.org/entries/Q0_Metatheory.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest