Mercurial > hg > Members > kono > Proof > ZF-in-agda
diff zf-in-agda.ind @ 279:197e0b3d39dc
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 09 May 2020 16:41:40 +0900 |
| parents | 9ccf8514c323 |
| children | 231deb255e74 |
line wrap: on
line diff
--- a/zf-in-agda.ind Sat May 09 09:40:18 2020 +0900 +++ b/zf-in-agda.ind Sat May 09 16:41:40 2020 +0900 @@ -2,6 +2,24 @@ --author: Shinji KONO +--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 + --Programming Mathematics Programming is processing data structure with λ terms. @@ -620,7 +638,7 @@ --Pure logical axioms - empty, pair, select, ε-inductioninfinity + empty, pair, select, ε-induction??infinity These are logical relations among OD.