A model of ZFC #
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.
ZFSet: ZFC set. Defined as
PSet.Equiv, the extensional equivalence.
Class: Class. Defined as
ZFSet.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.
ZFSet.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.allDefinable: All functions are classically definable.
ZFSet.IsFunc: 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
ZFSet.funs: ZFC set of ZFC functions
x → y.
ZFSet.Hereditarily p x: Predicate that every set in the transitive closure of
Class.iota: Definite description operator.
To avoid confusion between the Lean
set and the ZFC
Set, docstrings in this file refer to them
respectively as "
set" and "ZFC set".
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.
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.
The collection of all classes.
Set ZFSet, as this allows us to get many instances automatically. However, in
practice, we treat it as (the definitionally equal)
ZFSet → Prop. This means, the preferred way to
x : ZFSet belongs to
A : Class is to write