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
setoid
instance. - 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 asPSet
quotiented byPSet.Equiv
, the extensional equivalence.Class
: Class. Defined asSet ZFSet
.ZFSet.choice
: Axiom of choice. Proved from Lean's axiom of choice.
Other definitions #
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
,ZFSet.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 aZFSet
-valued function.Classical.allDefinable
: All functions are classically definable.ZFSet.IsFunc
: Predicate that a ZFC set is a subset ofx × y
that can be considered as a ZFC functionx → y
. That is, each member ofx
is related by the ZFC set to exactly one member ofy
.ZFSet.funs
: ZFC set of ZFC functionsx → y
.ZFSet.Hereditarily p x
: Predicate that every set in the transitive closure ofx
has propertyp
.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 ZFSet.mapDefinableAux
computably.
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.
Equations
Instances For
Equations
- PSet.setoid = { r := PSet.Equiv, iseqv := PSet.setoid.proof_1 }
Equations
- PSet.instHasSubset = { Subset := PSet.Subset }
Equations
Equations
Equations
- PSet.instMembership = { mem := PSet.Mem }
Equations
- PSet.instWellFoundedRelation = { rel := fun (x1 x2 : PSet) => x1 ∈ x2, wf := PSet.mem_wf }
Equations
Equations
A nonempty set is one that contains some element.
Equations
- u.Nonempty = u.toSet.Nonempty
Instances For
Equations
- PSet.instEmptyCollection = { emptyCollection := PSet.empty }
Equations
Insert an element into a pre-set
Equations
- x.insert y = PSet.mk (Option y.Type) fun (o : Option y.Type) => Option.casesOn o x y.Func
Instances For
Equations
- PSet.instInsert = { insert := PSet.insert }
Equations
- PSet.instSingleton = { singleton := fun (s : PSet) => insert s ∅ }
Equations
Equations
- x.instInhabitedTypeInsert y = inferInstanceAs (Inhabited (Option y.Type))
The n-th von Neumann ordinal
Equations
- PSet.ofNat 0 = ∅
- PSet.ofNat n.succ = insert (PSet.ofNat n) (PSet.ofNat n)
Instances For
The von Neumann ordinal ω
Equations
- PSet.omega = PSet.mk (ULift.{?u.4, 0} ℕ) fun (n : ULift.{?u.4, 0} ℕ) => PSet.ofNat n.down
Instances For
The pre-set union operator
Equations
- PSet.«term⋃₀_» = Lean.ParserDescr.node `PSet.term⋃₀_ 110 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "⋃₀ ") (Lean.ParserDescr.cat `term 110))
Instances For
The image of a function from pre-sets to pre-sets.
Equations
- PSet.image f x = PSet.mk x.Type (f ∘ x.Func)
Instances For
Universe lift operation
Equations
- (PSet.mk α A).Lift = PSet.mk (ULift.{?u.121, ?u.122} α) fun (x : ULift.{?u.121, ?u.122} α) => match x with | { down := x } => (A x).Lift
Instances For
Embedding of one universe in another
Equations
- PSet.embed = PSet.mk (ULift.{?u.6, ?u.7 + 1} PSet) fun (x : ULift.{?u.6, ?u.7 + 1} PSet) => match x with | { down := x } => x.Lift
Instances For
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 = PSet.Equiv a b
- PSet.Arity.Equiv a b = ∀ (x y : PSet), x.Equiv y → PSet.Arity.Equiv (a x) (b y)
Instances For
Equations
- PSet.Resp.inhabited = { default := ⟨Function.OfArity.const PSet default n, ⋯⟩ }
Function equivalence for functions respecting equivalence. See PSet.Arity.Equiv
.
Equations
- a.Equiv b = PSet.Arity.Equiv ↑a ↑b
Instances For
Helper function for PSet.eval
.
Equations
- PSet.Resp.evalAux = ⟨fun (a : PSet.Resp 0) => ⟦↑a⟧, PSet.Resp.evalAux.proof_4⟩
- PSet.Resp.evalAux = ⟨fun (a : PSet.Resp (n + 1)) => Quotient.lift (fun (x : PSet) => ↑PSet.Resp.evalAux (a.f x)) ⋯, ⋯⟩
Instances For
An equivalence-respecting function yields an n-ary ZFC set function.
Equations
- PSet.Resp.eval n = ↑PSet.Resp.evalAux
Instances 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.
- mk: {n : ℕ} → (f : PSet.Resp n) → PSet.Definable n (PSet.Resp.eval n f)
Instances
The evaluation of a function respecting equivalence is definable, by that same function.
Equations
Instances For
Turns a definable function into a function that respects equivalence.
Equations
- PSet.Definable.Resp (PSet.Resp.eval n f) = f
Instances For
All functions are classically definable.
Equations
- Classical.allDefinable F = PSet.Definable.EqMk ⟨Classical.choose ⋯, ⋯⟩ ⋯
- Classical.allDefinable F = PSet.Definable.EqMk ⟨fun (x : PSet) => ↑(PSet.Definable.Resp (F ⟦x⟧)), ⋯⟩ ⋯
Instances For
Equations
- ZFSet.instMembership = { mem := fun (t s : ZFSet) => s.Mem t }
A nonempty set is one that contains some element.
Equations
- u.Nonempty = u.toSet.Nonempty
Instances For
Equations
- ZFSet.hasSubset = { Subset := ZFSet.Subset }
Equations
Equations
Equations
Equations
- ZFSet.instEmptyCollection = { emptyCollection := ZFSet.empty }
Equations
- ZFSet.instInsert = { insert := ZFSet.Insert }
Equations
- ZFSet.instSingleton = { singleton := fun (x : ZFSet) => insert x ∅ }
Equations
The powerset operation, the collection of subsets of a ZFC set
Equations
Instances For
The union operator, the collection of elements of elements of a ZFC set
Equations
Instances For
The union operator, the collection of elements of elements of a ZFC set
Equations
- ZFSet.«term⋃₀_» = Lean.ParserDescr.node `ZFSet.term⋃₀_ 110 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "⋃₀ ") (Lean.ParserDescr.cat `term 110))
Instances For
The intersection operator, the collection of elements in all of the elements of a ZFC set. We
define ⋂₀ ∅ = ∅
.
Equations
- ZFSet.«term⋂₀_» = Lean.ParserDescr.node `ZFSet.term⋂₀_ 110 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "⋂₀ ") (Lean.ParserDescr.cat `term 110))
Instances For
Equations
- ZFSet.instWellFoundedRelation = { rel := fun (x1 x2 : ZFSet) => x1 ∈ x2, wf := ZFSet.mem_wf }
Equations
Equations
The image of a (definable) ZFC set function
Equations
- ZFSet.image f = match (motive := PSet.Resp 1 → ZFSet → ZFSet) PSet.Definable.Resp f with | ⟨r, hr⟩ => PSet.Resp.eval 1 ⟨PSet.image r, ⋯⟩
Instances For
The range of an indexed family of sets. The universes allow for a more general index type
without manual use of ULift
.
Equations
- ZFSet.range f = ⟦PSet.mk (ULift.{?u.19, ?u.20} α) (Quotient.out ∘ f ∘ ULift.down)⟧
Instances For
The cartesian product, {(a, b) | a ∈ x, b ∈ y}
Equations
- ZFSet.prod = ZFSet.pairSep fun (x x : ZFSet) => True
Instances For
Equations
- ZFSet.mapDefinableAux f = Classical.allDefinable fun (y : ZFSet) => y.pair (f y)
Given a predicate p
on ZFC sets. Hereditarily p x
means that x
has property p
and the
members of x
are all Hereditarily p
.
Equations
- ZFSet.Hereditarily p x = (p x ∧ ∀ y ∈ x, ZFSet.Hereditarily p y)
Instances For
Alias of the forward direction of ZFSet.hereditarily_iff
.
Equations
- instInsertZFSetClass = { insert := Set.insert }
Equations
- Class.instCoeZFSet = { coe := Class.ofSet }
Equations
- Class.instMembership = { mem := Class.Mem }
Equations
- Class.instWellFoundedRelation = { rel := fun (x1 x2 : Class) => x1 ∈ x2, wf := Class.mem_wf }
Equations
Equations
Convert a conglomerate (a collection of classes) into a class
Equations
- Class.congToClass x = {y : ZFSet | ↑y ∈ x}
Instances For
The power class of a class is the class of all subclasses that are ZFC sets
Equations
- x.powerset = Class.congToClass (𝒫 x)
Instances For
The union of a class is the class of all members of ZFC sets in the class
Equations
- Class.«term⋃₀_» = Lean.ParserDescr.node `Class.term⋃₀_ 110 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "⋃₀ ") (Lean.ParserDescr.cat `term 110))
Instances For
The intersection of a class is the class of all members of ZFC sets in the class
Equations
- Class.«term⋂₀_» = Lean.ParserDescr.node `Class.term⋂₀_ 110 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "⋂₀ ") (Lean.ParserDescr.cat `term 110))
Instances For
An induction principle for sets. If every subset of a class is a member, then the class is universal.
Function value
Equations
- F ′ A = Class.iota fun (y : ZFSet) => Class.ToSet (fun (x : ZFSet) => F (x.pair y)) A
Instances For
Function value
Equations
- Class.«term_′_» = Lean.ParserDescr.trailingNode `Class.term_′_ 100 100 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ′ ") (Lean.ParserDescr.cat `term 101))
Instances For
A choice function on the class of nonempty ZFC sets.
Instances For
ZFSet.toSet
as an equivalence.
Equations
- One or more equations did not get rendered due to their size.