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
setoidinstance. - 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 aspSetquotiented bypSet.equiv, the extensional equivalence.Class: Class. Defined asset Set.Set.choice: Axiom of choice. Proved from Lean's axiom of choice.
Other definitions #
arity α n:n-ary functionα → α → ... → α. Defined inductively.arity.const a n:n-ary constant function equal toa.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.pSet.omega,Set.omega: The von Neumann ordinalωas apSet, as aSet.pSet.arity.equiv: Extensional equivalence ofn-arypSet-valued functions. Extension ofpSet.equiv.pSet.resp: Collection ofn-arypSet-valued functions that respect extensional equivalence.pSet.eval: Turns apSet-valued function that respect extensional equivalence into aSet-valued function.classical.all_definable: All functions are classically definable.Set.is_func: Predicate that a ZFC set is a subset ofx × ythat can be considered as a ZFC functionx → y. That is, each member ofxis related by the ZFC set to exactly one member ofy.Set.funs: ZFC set of ZFC functionsx → y.Class.iota: Definite description operator.
Notes #
To avoid confusion between the Lean set and the ZFC Set, docstrings in this file refer to them
respectively as "set" and "ZFC set".
TODO #
Prove Set.map_definable_aux computably.
Informal translation
The arity of a type $α$ with $0$ arguments is $α$.
Informal translation
The arity of a function of arity $n+1$ is the arity of a function of arity $n$.
Constant n-ary function with value a.
Equations
- arity.const a (n + 1) = λ (_x : α), arity.const a n
- arity.const a 0 = a
Informal translation
The constant function $f(x_1,\ldots,x_n)=a$ is equal to $a$ when $n=0$.
Informal translation
Let $a$ be an element of a type $α$ and let $n$ be a natural number. Then the function $f:\alpha\to\alpha$ defined by $f(x)=a$ for all $x\in\alpha$ is equal to the function $g:\alpha\to\alpha$ defined by $g(x)=a$ for all $x\in\alpha$.
Informal translation
Let $a$ be an element of a type $α$ and let $n$ be a natural number. Then $arity.const a (n+1) x = arity.const a n$.
Equations
The type of pre-sets in universe u. A pre-set
is a family of pre-sets indexed by a type in Type u.
The ZFC universe is defined as a quotient of this
to ensure extensionality.
Instances for pSet
The underlying type of a pre-set
Instances for pSet.type
Informal translation
The type of the pSet $pSet.mk α A$ is $α$.
Informal translation
The function of the power set of a set $A$ is $A$.
Informal translation
The map $\eta: \mathrm{pSet}\to \mathrm{pSet}$ is the identity map.
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.
Informal translation
Let $x$ and $y$ be pointed sets. If $x$ and $y$ are equivalent, then for each $i\in x$ there is a $j\in y$ such that $x(i)$ and $y(j)$ are equivalent.
Informal translation
Let $x$ and $y$ be pointed sets. If $x$ and $y$ are equivalent, then there is a pointed set $z$ such that $x$ and $z$ are equivalent and $y$ and $z$ are equivalent.
Informal translation
The identity function is an equivalence of $x$ with itself.
Informal translation
The identity function is an equivalence of $x$ with itself.
Informal translation
If $x$ is equivalent to $y$ and $y$ is equivalent to $z$, then $x$ is equivalent to $z$.
Informal translation
If $x$ and $y$ are equivalent posets, then $y$ and $x$ are equivalent posets.
Informal translation
If $x$ is equinumerous to $y$ and $y$ is equinumerous to $z$, then $x$ is equinumerous to $z$.
Equations
- pSet.setoid = {r := pSet.equiv, iseqv := pSet.setoid._proof_1}
Equations
Informal translation
Two sets $x$ and $y$ are equivalent if and only if $x\subset y$ and $y\subset x$.
Informal translation
Let $x,y,z$ be pSets. If $x$ and $y$ are equivalent, then $x\subset z$ if and only if $y\subset z$.
Informal translation
Let $x,y,z$ be pointed sets. If $x$ and $y$ are equivalent, then $z\subset x$ if and only if $z\subset y$.
Equations
- pSet.has_mem = {mem := pSet.mem}
Informal translation
Let $A$ be a function from a set $X$ to the power set of $X$. Then $A(x)\in\mathcal{P}(X)$ for all $x\in X$.
Informal translation
Two sets $x$ and $y$ are equal if and only if they have the same elements.
Informal translation
If $x$ and $y$ are equivalent sets, then $w\in x$ if and only if $w\in y$.
Informal translation
Two sets $x$ and $y$ are equivalent if and only if $w\in x$ if and only if $w\in y$.
Informal translation
If $x$ and $y$ are equivalent sets, then $x\in w$ if and only if $y\in w$.
Informal translation
The membership relation on the set of all sets is well-founded.
Equations
Informal translation
If $x$ is a member of $y$, then $y$ is not a member of $x$.
Informal translation
The partial set $x$ is not a member of itself.
Two pre-sets are equivalent iff they have the same members.
Informal translation
Two pSets $x$ and $y$ are equivalent if and only if their underlying sets are equal.
Equations
The empty pre-set
Equations
Equations
Equations
- pSet.inhabited = {default := ∅}
Informal translation
No element of a pSet is in the empty set.
Informal translation
The empty set is a subset of any set.
Equations
Equations
- pSet.has_singleton = {singleton := λ (s : pSet), {s}}
Equations
The n-th von Neumann ordinal
Equations
- pSet.of_nat (n + 1) = has_insert.insert (pSet.of_nat n) (pSet.of_nat n)
- pSet.of_nat 0 = ∅
The von Neumann ordinal ω
Equations
- pSet.omega = pSet.mk (ulift ℕ) (λ (n : ulift ℕ), pSet.of_nat n.down)
Equations
- pSet.has_sep = {sep := pSet.sep}
Informal translation
Let $x$ and $y$ be sets. Then $y\in x^*$ if and only if $y\subset x$.
Informal translation
Let $x$ and $y$ be pSets. Then $y\in\bigcup x$ if and only if there is a pSet $z$ such that $z\in x$ and $y\in z$.
Informal translation
Let $f:X\to Y$ be a function between two sets $X$ and $Y$. Then $y\in f(X)$ if and only if there is an $x\in X$ such that $y=f(x)$.
Informal translation
The lift of a pSet is in the embedding of pSet.
Function equivalence is defined so that f ~ g iff ∀ x y, x ~ y → f x ~ g y. This extends to
equivalence of n-ary functions.
Equations
- pSet.arity.equiv a b = ∀ (x y : pSet), x.equiv y → pSet.arity.equiv (a x) (b y)
- pSet.arity.equiv a b = pSet.equiv a b
Informal translation
The arity of a constant function is constant.
resp n is the collection of n-ary functions on pSet that respect
equivalence, i.e. when the inputs are equivalent the output is as well.
Equations
- pSet.resp n = {x // pSet.arity.equiv x x}
Instances for pSet.resp
Equations
Function equivalence for functions respecting equivalence. See pSet.arity.equiv.
Equations
- a.equiv b = pSet.arity.equiv a.val b.val
Informal translation
The relation of being equivalent is reflexive on the set of partitions of $n$.
Informal translation
Let $a,b,c$ be partitions of a set of size $n$. If $a$ and $b$ are equivalent and $b$ and $c$ are equivalent, then $a$ and $c$ are equivalent.
Informal translation
Let $a$ and $b$ be partitions of a set of size $n$. Then $a$ is equivalent to $b$ if and only if $b$ is equivalent to $a$.
Informal translation
Let $n$ be a natural number and let $x, y, z$ be $n$-element sets. If $x$ is equivalent to $y$ and $y$ is equivalent to $z$, then $x$ is equivalent to $z$.
Equations
- pSet.resp.setoid = {r := pSet.resp.equiv n, iseqv := _}
The ZFC universe of sets consists of the type of pre-sets, quotiented by extensional equivalence.
Equations
Helper function for pSet.eval.
An equivalence-respecting function yields an n-ary ZFC set function.
Equations
Instances for pSet.resp.eval
Informal translation
Let $f$ be a function from $n+1$-types to sets. Then $f(x)$ is a function from $n$-types to sets.
- mk : Π {n : ℕ} (f : pSet.resp n), pSet.definable n (pSet.resp.eval n f)
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 this typeclass
Instances of other typeclasses for pSet.definable
- pSet.definable.has_sizeof_inst
The evaluation of a function respecting equivalence is definable, by that same function.
Equations
Turns a definable function into a function that respects equivalence.
Equations
- pSet.definable.resp (pSet.resp.eval n f) = f
Informal translation
The definable set $s$ is equal to the set $pSet.resp.eval n (pSet.definable.resp s)$.
All functions are classically definable.
Equations
- classical.all_definable F = pSet.definable.eq_mk ⟨λ (x : pSet), (pSet.definable.resp (F ⟦x⟧)).val, _⟩ _
- classical.all_definable F = let p : ∃ (a : pSet), ⟦a⟧ = F := _ in pSet.definable.eq_mk ⟨classical.some p, _⟩ _
Informal translation
The set of equivalence classes of $x$ is $x$.
Informal translation
Two sets $x$ and $y$ are equal if and only if they are equivalent.
Informal translation
If $x$ and $y$ are equivalent sets, then $x=y$.
Informal translation
If two sets $x$ and $y$ have the same underlying type, then they are equal.
Informal translation
Let $n$ be a natural number and let $f$ be a function from $n+1$-element sets to sets. Let $x$ be a set. Then $f(x\cup\{x\})=f(x)$.
Equations
- Set.has_mem = {mem := Set.mem}
Equations
Informal translation
$x\subseteq y$ if and only if $z\in x$ implies $z\in y$.
Informal translation
Let $x$ and $y$ be sets. Then $x\subset y$ if and only if $Set.mk x\subset Set.mk y$.
Informal translation
Two sets $x$ and $y$ are equal if and only if they contain the same elements.
Informal translation
Two sets $x$ and $y$ are equal if and only if they contain the same elements.
Equations
Equations
- Set.inhabited = {default := ∅}
Informal translation
$x$ is not an element of the empty set.
Informal translation
The empty set is a subset of any set.
Informal translation
A set $x$ is empty if and only if for all sets $y$, $y$ is not an element of $x$.
insert x y is the set {x} ∪ y
Equations
- Set.insert = pSet.resp.eval 2 ⟨pSet.insert, Set.insert._proof_1⟩
Equations
Equations
- Set.has_singleton = {singleton := λ (x : Set), {x}}
Informal translation
$x$ is an element of the set $y\cup z$ if and only if $x=y$ or $x$ is an element of $z$.
Informal translation
$x\in\{y\}$ if and only if $x=y$.
Informal translation
$x$ is an element of $\{y,z\}$ if and only if $x=y$ or $x=z$.
Informal translation
The empty set is a countable set.
Informal translation
If $n$ is a set, then $n\cup\{n\}$ is a set.
Equations
- Set.has_sep = {sep := Set.sep}
Informal translation
$y\in\{y\in x\mid p(y)\}$ if and only if $y\in x$ and $p(y)$.
The powerset operation, the collection of subsets of a ZFC set
Equations
- Set.powerset = pSet.resp.eval 1 ⟨pSet.powerset, Set.powerset._proof_1⟩
Informal translation
$y$ is a subset of $x$ if and only if $y$ is an element of the powerset of $x$.
Informal translation
Let $A$ and $B$ be families of sets indexed by $α$ and $β$, respectively. Suppose that for each $a\in\bigcup_{α}A$ there is a $b\in\bigcup_{β}B$ such that $A(a)$ is equinumerous to $B(b)$. Then there is a $b\in\bigcup_{β}B$ such that $A(a)$ is equinumerous to $B(b)$.
The union operator, the collection of elements of elements of a ZFC set
Equations
- Set.sUnion = pSet.resp.eval 1 ⟨pSet.sUnion, Set.sUnion._proof_1⟩
Informal translation
$y$ is an element of the union of the sets $x$ if and only if there is a set $z$ in $x$ such that $y$ is an element of $z$.
Informal translation
The union of a singleton set is the set itself.
Informal translation
If $x$ and $y$ are sets and $\{x\}=\{y\}$, then $x=y$.
Equations
Equations
Equations
- Set.has_sdiff = {sdiff := Set.diff}
Informal translation
An element $z$ is in the union of $x$ and $y$ if and only if $z$ is in $x$ or $z$ is in $y$.
Informal translation
$z\in x\cap y$ if and only if $z\in x$ and $z\in y$.
Informal translation
$z\in x\setminus y$ if and only if $z\in x$ and $z\notin y$.
Induction on the ∈ relation.
Informal translation
Let $p$ be a property of sets. Then $p$ holds for all sets.
Informal translation
The relation $x\in y$ is well-founded.
Equations
Informal translation
If $x$ is a member of $y$, then $y$ is not a member of $x$.
Informal translation
The set $x$ does not contain itself.
Informal translation
Let $x$ be a set. If $x$ is nonempty, then there is a set $y$ such that $y\in x$ and $x\cap y=\emptyset$.
The image of a (definable) ZFC set function
Equations
- Set.image f = let r : pSet.resp 1 := pSet.definable.resp f in pSet.resp.eval 1 ⟨pSet.image r.val, _⟩
Informal translation
Let $f:X\to Y$ be a definable function. Then $f(y)\in f(X)$ for all $y\in X$.
Informal translation
Let $f:X\to Y$ be a definable function. Then $y\in f(X)$ if and only if there is $x\in X$ such that $f(x)=y$.
Informal translation
$z\in\{(a,b)\mid a\in x, b\in y, p(a,b)\}$ if and only if there are $a\in x$ and $b\in y$ such that $z=(a,b)$ and $p(a,b)$.
Informal translation
If $x\times y=x'\times y'$, then $x=x'$ and $y=y'$.
Informal translation
$z$ is in the product of $x$ and $y$ if and only if there are $a\in x$ and $b\in y$ such that $z=(a,b)$.
Informal translation
$(a,b)\in X\times Y$ if and only if $a\in X$ and $b\in Y$.
is_func x y f is the assertion that f is a subset of x × y which relates to each element
of x a unique element of y, so that we can consider fas a ZFC function x → y.
Informal translation
$f$ is a function from $x$ to $y$ if and only if $f$ is an element of $x.funs y$.
Equations
- Set.map_definable_aux f = classical.all_definable (λ (y : Set), y.pair (f y))
Informal translation
Let $f:X\to Y$ be a definable function. Then $y\in f(x)$ if and only if there is $z\in X$ such that $f(z)=y$.
Informal translation
Let $f:X\to Y$ be a definable function. Then for each $x\in X$ there is a unique $y\in Y$ such that $f(x)=y$.
Informal translation
Let $f:Set\to Set$ be a definable function. Then $x$ is a function from $y$ to $f(x)$ if and only if $f(z)\in y$ for all $z\in x$.
The collection of all classes. A class is defined as a set of ZFC sets.
Coerce a ZFC set into a class
Equations
- Class.of_Set x = {y : Set | y ∈ x}
Equations
Assert that A is a ZFC set satisfying p
Equations
- Class.has_mem = {mem := Class.mem}
Informal translation
A class $A$ is in the universe if and only if there is a set $x$ such that $A=x$.
Convert a conglomerate (a collection of classes) into a class
Equations
- Class.Cong_to_Class x = {y : Set | ↑y ∈ x}
Convert a class into a conglomerate (a collection of classes)
Equations
- x.Class_to_Cong = {y : Class | y ∈ x}
The power class of a class is the class of all subclasses that are ZFC sets
Equations
- x.powerset = Class.Cong_to_Class (𝒫x)
The union of a class is the class of all members of ZFC sets in the class
Equations
- ⋃₀ x = ⋃₀ x.Class_to_Cong
Informal translation
The map $x\mapsto \{x\}$ is injective.
Informal translation
Let $p$ be a property of sets. Then $p(x)$ holds if and only if $p(\{x\})$ holds.
Informal translation
$x\in A$ if and only if $A(x)$.
Informal translation
$x\in y$ if and only if $y$ is a member of the class of all sets containing $x$.
Informal translation
The class of $x$ is a subset of the class of $y$ if and only if $x$ is a subset of $y$.
Informal translation
The class of all $y\in x$ such that $p(y)$ is equal to the class of all $y\in x$ such that $p(y)$.
Informal translation
The class of the empty set is the empty set.
Informal translation
The class of a set $x$ with an element $y$ added is the class of the set $x$ with the element $y$ added.
Informal translation
The union of two classes is the class of the union of the two sets.
Informal translation
The intersection of two classes is the class of the intersection of the sets.
Informal translation
The difference of two sets is the set of elements that are in the first set but not in the second.
Informal translation
The powerset of a set $x$ is a set.
Informal translation
The set of all classes of elements of a set $X$ is equal to the class of the set of all elements of $X$.
Informal translation
Let $p$ be a property of sets and let $x$ be a set such that $p(y)$ if and only if $y=x$. Then the class of all sets $y$ such that $p(y)$ is equal to the set $x$.
Unlike the other set constructors, the iota definite descriptor
is a set for any set input, but not constructively so, so there is no
associated (Set → Prop) → Set function.
Informal translation
The class $\iota p$ is a member of the class $\mathcal{U}$.
Function value
Equations
- F′A = Class.iota (λ (y : Set), Class.to_Set (λ (x : Set), F (x.pair y)) A)
Informal translation
The class $F′A$ is a member of the class $Class.univ$.
Informal translation
Let $f:Set\to Set$ be a definable function. Then for all $x,y\in Set$, $y\in x$ implies that $f(x)′y=f(y)$.
Informal translation
Let $x$ be a set such that $\emptyset\notin x$. Let $y$ be a set such that $y\in x$. Then there is a set $z$ such that $z\in y$.
Informal translation
Let $x$ be a set. Then the choice function $x\to \bigcup x$ is a function.
Informal translation
Let $x$ be a set. If $x$ is nonempty, then there is a function $f:x\to x$ such that $f(y)\in y$ for all $y\in x$.