Mercurial > hg > Members > kono > Proof > ZF-in-agda

comparison src/README.md @ 1097:40345abc0949

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add README
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 24 Dec 2022 11:39:30 +0900
parents
children
comparison
equal deleted inserted replaced
1096:55ab5de1ae02 1097:40345abc0949
1 Constructing ZF Set Theory in Agda
2 ============
3
4 Shinji KONO (kono@ie.u-ryukyu.ac.jp), University of the Ryukyus
5
6 ## ZF in Agda
7
8 ```
9 zf.agda axiom of ZF
10 zfc.agda axiom of choice
11 Ordinals.agda axiom of Ordinals
12 ordinal.agda countable model of Ordinals
13 OD.agda model of ZF based on Ordinal Definable Set with assumptions
14 ODC.agda Law of exclude middle from axiom of choice assumptions
15 LEMC.agda model of choice with assumption of the Law of exclude middle
16 OPair.agda ordered pair on OD
17 zorn.agda Zorn Lemma
18
19 BAlgbra.agda Boolean algebra on OD (not yet done)
20 filter.agda Filter on OD (not yet done)
21 cardinal.agda Caedinal number on OD (not yet done)
22
23 logic.agda some basics on logic
24 nat.agda some basics on Nat
25
26 NSet.agda primitve set thoery examples
27
28 ODUtil.agda
29 OrdUtil.agda
30 PFOD.agda
31 Topology.agda
32 VL.agda
33 generic-filter.agda
34 partfunc.agda
35
36 ```
37
38 ## Ordinal Definable Set
39
40 It is a predicate has an Ordinal argument.
41
42 In Agda, OD is defined as follows.
43
44 ```
45 record OD : Set (suc n ) where
46 field
47 def : (x : Ordinal ) → Set n
48 ```
49
50 This is not a ZF Set, because it can contain entire Ordinals.
51
52 ## HOD : Hereditarily Ordinal Definable
53
54 What we need is a bounded OD, the containment is limited by an ordinal.
55
56 ```
57 record HOD : Set (suc n) where
58 field
59 od : OD
60 odmax : Ordinal
61 <odmax : {y : Ordinal} → def od y → y o< odmax
62 ```
63
64 In classical Set Theory, HOD stands for Hereditarily Ordinal Definable, which means
65
66 ```
67 HOD = { x | TC x ⊆ OD }
68 ```
69
70 TC x is all transitive closure of x, that is elements of x and following all elements of them are all OD. But
71 what is x? In this case, x is an Set which we don't have yet. In our case, HOD is a bounded OD.
72
73 ## 1 to 1 mapping between an HOD and an Ordinal
74
75 HOD is a predicate on Ordinals and the solution is bounded by some ordinal. If we have a mapping
76
77 ```
78 od→ord : HOD → Ordinal
79 ord→od : Ordinal → HOD
80 oiso : {x : HOD } → ord→od ( od→ord x ) ≡ x
81 diso : {x : Ordinal } → od→ord ( ord→od x ) ≡ x
82 ```
83
84 we can check an HOD is an element of the OD using def.
85
86 A ∋ x can be define as follows.
87
88 ```
89 _∋_ : ( A x : HOD ) → Set n
90 _∋_ A x = def (od A) ( od→ord x )
91
92 ```
93 In ψ : Ordinal → Set, if A is a record { def = λ x → ψ x } , then
94
95 A x = def A ( od→ord x ) = ψ (od→ord x)
96
97 They say the existing of the mappings can be proved in Classical Set Theory, but we
98 simply assumes these non constructively.
99
100 ## we need some more axiom to achive ZF Set Theory
101
102 ```
103 record ODAxiom : Set (suc n) where
104 field
105 -- HOD is isomorphic to Ordinal (by means of Goedel number)
106 & : HOD → Ordinal
107 * : Ordinal → HOD
108 c<→o< : {x y : HOD } → def (od y) ( & x ) → & x o< & y
109 ⊆→o≤ : {y z : HOD } → ({x : Ordinal} → def (od y) x → def (od z) x ) → & y o< osuc (& z)
110 *iso : {x : HOD } → * ( & x ) ≡ x
111 &iso : {x : Ordinal } → & ( * x ) ≡ x
112 ==→o≡ : {x y : HOD } → (od x == od y) → x ≡ y
113 sup-o : (A : HOD) → ( ( x : Ordinal ) → def (od A) x → Ordinal ) → Ordinal -- required in Replace
114 sup-o≤ : (A : HOD) → { ψ : ( x : Ordinal ) → def (od A) x → Ordinal } → ∀ {x : Ordinal } → (lt : def (od A) x ) → ψ x lt o≤ sup-o A ψ
115 -- possible order restriction (required in the axiom of infinite )
116 ho< : {x : HOD} → & x o< next (odmax x)
117 ```