Metatheory of Q0 (Q7361320)
From MaRDI portal
!
This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use the normal view instead:
AFP entry Q0_Metatheory
| Language | Label | Description | Also known as |
|---|---|---|---|
| default for all languages | No label defined |
||
| English | Metatheory of Q0 |
AFP entry Q0_Metatheory |
Statements
4 November 2023
0 references
Javier Díaz
0 references
Metatheory of Q0 (English)
0 references
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.
0 references
