A model of ZFC #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
In this file, we model Zermelo-Fraenkel set theory (+ Choice) using Lean's underlying type theory. We do this in four main steps:
- Define pre-sets inductively.
- Define extensional equivalence on pre-sets and give it a
- Define ZFC sets by quotienting pre-sets by extensional equivalence.
- Define classes as sets of ZFC sets. Then the rest is usual set theory.
The model #
pSet: Pre-set. A pre-set is inductively defined by its indexing type and its members, which are themselves pre-sets.
Set: ZFC set. Defined as
pSet.equiv, the extensional equivalence.
Class: Class. Defined as
Set.choice: Axiom of choice. Proved from Lean's axiom of choice.
Other definitions #
arity α n:
α → α → ... → α. Defined inductively.
arity.const a n:
n-ary constant function equal to
pSet.type: Underlying type of a pre-set.
pSet.func: Underlying family of pre-sets of a pre-set.
pSet.equiv: Extensional equivalence of pre-sets. Defined inductively.
Set.omega: The von Neumann ordinal
pSet, as a
pSet.arity.equiv: Extensional equivalence of
pSet-valued functions. Extension of
pSet.resp: Collection of
pSet-valued functions that respect extensional equivalence.
pSet.eval: Turns a
pSet-valued function that respect extensional equivalence into a
classical.all_definable: All functions are classically definable.
Set.is_func: Predicate that a ZFC set is a subset of
x × ythat can be considered as a ZFC function
x → y. That is, each member of
xis related by the ZFC set to exactly one member of
Set.funs: ZFC set of ZFC functions
x → y.
Set.hereditarily p x: Predicate that every set in the transitive closure of
Class.iota: Definite description operator.
The type of pre-sets in universe
u. A pre-set
is a family of pre-sets indexed by a type in
The ZFC universe is defined as a quotient of this
to ensure extensionality.
Two pre-sets are extensionally equivalent if every element of the first family is extensionally equivalent to some element of the second family and vice-versa.
Function equivalence is defined so that
f ~ g iff
∀ x y, x ~ y → f x ~ g y. This extends to
The ZFC universe of sets consists of the type of pre-sets, quotiented by extensional equivalence.
Helper function for
A set function is "definable" if it is the image of some n-ary pre-set function. This isn't exactly definability, but is useful as a sufficient condition for functions that have a computable image.
Instances of other typeclasses for
All functions are classically definable.
The collection of all classes.
set Set, as this allows us to get many instances automatically. However, in
practice, we treat it as (the definitionally equal)
Set → Prop. This means, the preferred way to
x : Set belongs to
A : Class is to write