Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison 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 |
comparison
equal
deleted
inserted
replaced
278:bfb5e807718b | 279:197e0b3d39dc |
---|---|
1 -title: Constructing ZF Set Theory in Agda | 1 -title: Constructing ZF Set Theory in Agda |
2 | 2 |
3 --author: Shinji KONO | 3 --author: Shinji KONO |
4 | |
5 --ZF in Agda | |
6 | |
7 zf.agda axiom of ZF | |
8 zfc.agda axiom of choice | |
9 Ordinals.agda axiom of Ordinals | |
10 ordinal.agda countable model of Ordinals | |
11 OD.agda model of ZF based on Ordinal Definable Set with assumptions | |
12 ODC.agda Law of exclude middle from axiom of choice assumptions | |
13 LEMC.agda model of choice with assumption of the Law of exclude middle | |
14 OPair.agda ordered pair on OD | |
15 | |
16 BAlgbra.agda Boolean algebra on OD (not yet done) | |
17 filter.agda Filter on OD (not yet done) | |
18 cardinal.agda Caedinal number on OD (not yet done) | |
19 | |
20 logic.agda some basics on logic | |
21 nat.agda some basics on Nat | |
4 | 22 |
5 --Programming Mathematics | 23 --Programming Mathematics |
6 | 24 |
7 Programming is processing data structure with λ terms. | 25 Programming is processing data structure with λ terms. |
8 | 26 |
618 ZFのrecord | 636 ZFのrecord |
619 </a> | 637 </a> |
620 | 638 |
621 --Pure logical axioms | 639 --Pure logical axioms |
622 | 640 |
623 empty, pair, select, ε-inductioninfinity | 641 empty, pair, select, ε-induction??infinity |
624 | 642 |
625 These are logical relations among OD. | 643 These are logical relations among OD. |
626 | 644 |
627 empty : ∀( x : ZFSet ) → ¬ ( ∅ ∋ x ) | 645 empty : ∀( x : ZFSet ) → ¬ ( ∅ ∋ x ) |
628 pair→ : ( x y t : ZFSet ) → (x , y) ∋ t → ( t ≈ x ) ∨ ( t ≈ y ) | 646 pair→ : ( x y t : ZFSet ) → (x , y) ∋ t → ( t ≈ x ) ∨ ( t ≈ y ) |