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 )