# HG changeset patch # User Shinji KONO # Date 1594103531 -32400 # Node ID de2c472bcbcd857655ab9015f4e6f5d636faf9b0 # Parent 231deb255e74be53e62098494612d0dd78425ce1 ... diff -r 231deb255e74 -r de2c472bcbcd README.md --- 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 +