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

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)

### License

BSD License

### Topics

- Logic/Set theory

### Session ZFC_in_HOL

- ZFC_Library
- ZFC_in_HOL
- ZFC_Cardinals
- Kirby
- Ordinal_Exp
- Cantor_NF
- ZFC_Typeclasses
- General_Cardinals

### Used by

- Soundness of the Q0 proof system for higher-order logic
- Metatheory of Q0
- Wetzel’s Problem and the Continuum Hypothesis
- Category Theory for ZFC in HOL I: Foundations: Design Patterns, Set Theory, Digraphs, Semicategories
- Ordinal Partitions
- Category Theory with Adjunctions and Limits

## Cite

×

ZFC_in_HOL-AFP

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

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 20, 2020 : Isabelle2020
- Nov 4, 2019 : Isabelle2019