|
1097
|
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 ```
|
