diff --git a/metadata/entries/Q0_Metatheory.toml b/metadata/entries/Q0_Metatheory.toml new file mode 100644 --- /dev/null +++ b/metadata/entries/Q0_Metatheory.toml @@ -0,0 +1,26 @@ +title = "Metatheory of Q0" +date = 2023-11-04 +topics = [ + "Logic/General logic", +] +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" +note = "" + +[authors] + +[authors.diaz] +email = "diaz_email" + +[contributors] + +[notify] +diaz = "diaz_email" + +[history] + +[extra] + +[related] +dois = [] +pubs = [] diff --git a/web/authors/diaz/index.html b/web/authors/diaz/index.html --- a/web/authors/diaz/index.html +++ b/web/authors/diaz/index.html @@ -1,148 +1,161 @@
Asta Halkjær From 🌐 with contributions from Alexander Birch Jensen 🌐, Anders Schlichtkrull 🌐 and Jørgen Villadsen 🌐
July 18, 2019
October 12, 2020
Chelsea Edmonds 📧 and Lawrence C. Paulson 📧
September 23, 2023
+ Javier Díaz 📧 + +
+November 4, 2023
+October 24, 2019
This entry is a new formalisation of ZFC set theory in Isabelle/HOL. It is logically equivalent to Obua's HOLZF; the point is to have the closest possible integration with the rest of Isabelle/HOL, minimising the amount of new notations and exploiting type classes.
There is a type V of sets and a function elts :: V => V set mapping a set to its elements. Classes simply have type V set, and a predicate identifies the small classes: those that correspond to actual sets. Type classes connected with orders and lattices are used to minimise the amount of new notation for concepts such as the subset relation, union and intersection. Basic concepts — Cartesian products, disjoint sums, natural numbers, functions, etc. — are formalised.
More advanced set-theoretic concepts, such as transfinite induction, ordinals, cardinals and the transitive closure of a set, are also provided. The definition of addition and multiplication for general sets (not just ordinals) follows Kirby.
The theory provides two type classes with the aim of facilitating developments that combine V with other Isabelle/HOL types: embeddable, the class of types that can be injected into V (including V itself as well as V*V, etc.), and small, the class of types that correspond to some ZF set.
extra-history = Change history: [2020-01-28]: Generalisation of the "small" predicate and order types to arbitrary sets; ordinal exponentiation; introduction of the coercion ord_of_nat :: "nat => V"; numerous new lemmas. (revision 6081d5be8d08)December 27, 2019
This article provides a formalisation of Beukers's straightforward analytic proof that ζ(3) is irrational. This was first proven by Apéry (which is why this result is also often called ‘Apéry's Theorem’) using a more algebraic approach. This formalisation follows Filaseta's presentation of Beukers's proof.
The Archive of Formal Proofs is a collection of proof libraries, examples, and larger scientific developments, mechanically checked in the theorem prover Isabelle. It is organized in the way of a scientific journal, is indexed by dblp and has an ISSN: 2150-914x. Submissions are refereed and we encourage companion AFP submissions to conference and journal publications. To cite an entry, please use the preferred citation style.
A development version of the archive is available as well.
777 | +778 | Entries |
467 | Authors | |
- ~248,200 + ~248,700 | Lemmas | |
- ~4,021,300 + ~4,033,700 | Lines of Code |
Name | Used by ? entries | |
---|---|---|
1. | List-Index | 23 |
2. | Collections | 18 |
3. | Show | 16 |
4. | Jordan_Normal_Form | 15 |
5. | Coinductive | 13 |
6. | Deriving | 13 |
7. | Polynomial_Factorization | 12 |
8. | Regular-Sets | 12 |
9. | Landau_Symbols | 11 |
10. | Abstract-Rewriting | 10 |
11. | Automatic_Refinement | 10 |
12. | Native_Word | 10 |
AMS: Mathematical logic and foundations / General logic