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.
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.
Class.iota: Definite description operator.
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
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.
All functions are classically definable.