Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 337:de2c472bcbcd
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Tue, 07 Jul 2020 15:32:11 +0900 |
parents | 231deb255e74 |
children | bca043423554 |
files | README.md |
diffstat | 1 files changed, 111 insertions(+), 1 deletions(-) [+] |
line wrap: on
line diff
--- a/README.md Mon Jul 06 17:14:46 2020 +0900 +++ b/README.md Tue Jul 07 15:32:11 2020 +0900 @@ -1,1 +1,111 @@ -zf-in-agda.ind \ No newline at end of file +Constructing ZF Set Theory in Agda +============ + +Shinji KONO (kono@ie.u-ryukyu.ac.jp), University of the Ryukyus + +## ZF in Agda + +``` + zf.agda axiom of ZF + zfc.agda axiom of choice + Ordinals.agda axiom of Ordinals + ordinal.agda countable model of Ordinals + OD.agda model of ZF based on Ordinal Definable Set with assumptions + ODC.agda Law of exclude middle from axiom of choice assumptions + LEMC.agda model of choice with assumption of the Law of exclude middle + OPair.agda ordered pair on OD + + BAlgbra.agda Boolean algebra on OD (not yet done) + filter.agda Filter on OD (not yet done) + cardinal.agda Caedinal number on OD (not yet done) + + logic.agda some basics on logic + nat.agda some basics on Nat +``` + +## Ordinal Definable Set + +It is a predicate has an Ordinal argument. + +In Agda, OD is defined as follows. + +``` + record OD : Set (suc n ) where + field + def : (x : Ordinal ) → Set n +``` + +This is not a ZF Set, because it can contain entire Ordinals. + +-- HOD : Hereditarily Ordinal Definable + +What we need is a bounded OD, the containment is limited by an ordinal. + +``` + record HOD : Set (suc n) where + field + od : OD + odmax : Ordinal + <odmax : {y : Ordinal} → def od y → y o< odmax +``` + +In classical Set Theory, HOD stands for Hereditarily Ordinal Definable, which means + +``` + HOD = { x | TC x ⊆ OD } +``` + +TC x is all transitive closure of x, that is elements of x and following all elements of them are all OD. But +what is x? In this case, x is an Set which we don't have yet. In our case, HOD is a bounded OD. + +## 1 to 1 mapping between an HOD and an Ordinal + +HOD is a predicate on Ordinals and the solution is bounded by some ordinal. If we have a mapping + +``` + od→ord : HOD → Ordinal + ord→od : Ordinal → HOD + oiso : {x : HOD } → ord→od ( od→ord x ) ≡ x + diso : {x : Ordinal } → od→ord ( ord→od x ) ≡ x +``` + +we can check an HOD is an element of the OD using def. + +A ∋ x can be define as follows. + +``` + _∋_ : ( A x : HOD ) → Set n + _∋_ A x = def (od A) ( od→ord x ) + +``` +In ψ : Ordinal → Set, if A is a record { def = λ x → ψ x } , then + + A x = def A ( od→ord x ) = ψ (od→ord x) + +They say the existing of the mappings can be proved in Classical Set Theory, but we +simply assumes these non constructively. + +## What have we done + +``` + Axioms of Ordinals + An implementation of countable Ordinal + ZF Axioms + Model of ZF based on OD/HOD + LEM axiom of choice from LEM + ODC LEM from axiom of choice + OPair classical ordered pair example + filter definition of filter and ideal + cardinal unfinished Cardinal number + BAlgebra boolean algebra of OD + +``` + + + + + + + + +