Zermelo Fraenkel Set Theory in Higher-Order Logic

 

Title: Zermelo Fraenkel Set Theory in Higher-Order Logic
Author: Lawrence C. Paulson
Submission date: 2019-10-24
Abstract:

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.

BibTeX:
@article{ZFC_in_HOL-AFP,
  author  = {Lawrence C. Paulson},
  title   = {Zermelo Fraenkel Set Theory in Higher-Order Logic},
  journal = {Archive of Formal Proofs},
  month   = oct,
  year    = 2019,
  note    = {\url{http://isa-afp.org/entries/ZFC_in_HOL.html},
            Formal proof development},
  ISSN    = {2150-914x},
}
License: BSD License