|
431
|
1 {-# OPTIONS --allow-unsolved-metas #-}
|
|
|
2 open import Level
|
|
|
3 open import Ordinals
|
|
|
4 module ODC {n : Level } (O : Ordinals {n} ) where
|
|
|
5
|
|
|
6 open import zf
|
|
|
7 open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ; _⊔_ to _n⊔_ )
|
|
|
8 open import Relation.Binary.PropositionalEquality
|
|
|
9 open import Data.Nat.Properties
|
|
|
10 open import Data.Empty
|
|
|
11 open import Relation.Nullary
|
|
|
12 open import Relation.Binary
|
|
|
13 open import Relation.Binary.Core
|
|
|
14
|
|
|
15 import OrdUtil
|
|
|
16 open import logic
|
|
|
17 open import nat
|
|
|
18 import OD
|
|
|
19 import ODUtil
|
|
|
20
|
|
|
21 open inOrdinal O
|
|
|
22 open OD O
|
|
|
23 open OD.OD
|
|
|
24 open OD._==_
|
|
|
25 open ODAxiom odAxiom
|
|
|
26 open ODUtil O
|
|
|
27
|
|
|
28 open Ordinals.Ordinals O
|
|
|
29 open Ordinals.IsOrdinals isOrdinal
|
|
|
30 open Ordinals.IsNext isNext
|
|
|
31 open OrdUtil O
|
|
|
32
|
|
|
33
|
|
|
34 open HOD
|
|
|
35
|
|
|
36 open _∧_
|
|
|
37
|
|
|
38 postulate
|
|
|
39 -- mimimul and x∋minimal is an Axiom of choice
|
|
|
40 minimal : (x : HOD ) → ¬ (x =h= od∅ )→ HOD
|
|
|
41 -- this should be ¬ (x =h= od∅ )→ ∃ ox → x ∋ Ord ox ( minimum of x )
|
|
|
42 x∋minimal : (x : HOD ) → ( ne : ¬ (x =h= od∅ ) ) → odef x ( & ( minimal x ne ) )
|
|
467
|
43 -- minimality (proved by ε-induction with LEM)
|
|
431
|
44 minimal-1 : (x : HOD ) → ( ne : ¬ (x =h= od∅ ) ) → (y : HOD ) → ¬ ( odef (minimal x ne) (& y)) ∧ (odef x (& y) )
|
|
|
45
|
|
|
46
|
|
|
47 --
|
|
|
48 -- Axiom of choice in intutionistic logic implies the exclude middle
|
|
|
49 -- https://plato.stanford.edu/entries/axiom-choice/#AxiChoLog
|
|
|
50 --
|
|
|
51
|
|
|
52 pred-od : ( p : Set n ) → HOD
|
|
|
53 pred-od p = record { od = record { def = λ x → (x ≡ o∅) ∧ p } ;
|
|
|
54 odmax = osuc o∅; <odmax = λ x → subst (λ k → k o< osuc o∅) (sym (proj1 x)) <-osuc }
|
|
|
55
|
|
|
56 ppp : { p : Set n } { a : HOD } → pred-od p ∋ a → p
|
|
|
57 ppp {p} {a} d = proj2 d
|
|
|
58
|
|
|
59 p∨¬p : ( p : Set n ) → p ∨ ( ¬ p ) -- assuming axiom of choice
|
|
|
60 p∨¬p p with is-o∅ ( & (pred-od p ))
|
|
|
61 p∨¬p p | yes eq = case2 (¬p eq) where
|
|
|
62 ps = pred-od p
|
|
|
63 eqo∅ : ps =h= od∅ → & ps ≡ o∅
|
|
|
64 eqo∅ eq = subst (λ k → & ps ≡ k) ord-od∅ ( cong (λ k → & k ) (==→o≡ eq))
|
|
|
65 lemma : ps =h= od∅ → p → ⊥
|
|
|
66 lemma eq p0 = ¬x<0 {& ps} (eq→ eq record { proj1 = eqo∅ eq ; proj2 = p0 } )
|
|
|
67 ¬p : (& ps ≡ o∅) → p → ⊥
|
|
|
68 ¬p eq = lemma ( subst₂ (λ j k → j =h= k ) *iso o∅≡od∅ ( o≡→== eq ))
|
|
|
69 p∨¬p p | no ¬p = case1 (ppp {p} {minimal ps (λ eq → ¬p (eqo∅ eq))} lemma) where
|
|
|
70 ps = pred-od p
|
|
|
71 eqo∅ : ps =h= od∅ → & ps ≡ o∅
|
|
|
72 eqo∅ eq = subst (λ k → & ps ≡ k) ord-od∅ ( cong (λ k → & k ) (==→o≡ eq))
|
|
|
73 lemma : ps ∋ minimal ps (λ eq → ¬p (eqo∅ eq))
|
|
|
74 lemma = x∋minimal ps (λ eq → ¬p (eqo∅ eq))
|
|
|
75
|
|
|
76 decp : ( p : Set n ) → Dec p -- assuming axiom of choice
|
|
|
77 decp p with p∨¬p p
|
|
|
78 decp p | case1 x = yes x
|
|
|
79 decp p | case2 x = no x
|
|
|
80
|
|
|
81 ∋-p : (A x : HOD ) → Dec ( A ∋ x )
|
|
|
82 ∋-p A x with p∨¬p ( A ∋ x ) -- LEM
|
|
|
83 ∋-p A x | case1 t = yes t
|
|
|
84 ∋-p A x | case2 t = no (λ x → t x)
|
|
|
85
|
|
|
86 double-neg-eilm : {A : Set n} → ¬ ¬ A → A -- we don't have this in intutionistic logic
|
|
|
87 double-neg-eilm {A} notnot with decp A -- assuming axiom of choice
|
|
|
88 ... | yes p = p
|
|
|
89 ... | no ¬p = ⊥-elim ( notnot ¬p )
|
|
|
90
|
|
|
91 open _⊆_
|
|
|
92
|
|
|
93 power→⊆ : ( A t : HOD) → Power A ∋ t → t ⊆ A
|
|
|
94 power→⊆ A t PA∋t = record { incl = λ {x} t∋x → double-neg-eilm (t1 t∋x) } where
|
|
|
95 t1 : {x : HOD } → t ∋ x → ¬ ¬ (A ∋ x)
|
|
|
96 t1 = power→ A t PA∋t
|
|
|
97
|
|
447
|
98 power-∩ : { A x y : HOD } → Power A ∋ x → Power A ∋ y → Power A ∋ ( x ∩ y )
|
|
|
99 power-∩ {A} {x} {y} ax ay = power← A (x ∩ y) p01 where
|
|
|
100 p01 : {z : HOD} → (x ∩ y) ∋ z → A ∋ z
|
|
|
101 p01 {z} xyz = double-neg-eilm ( power→ A x ax (proj1 xyz ))
|
|
|
102
|
|
431
|
103 OrdP : ( x : Ordinal ) ( y : HOD ) → Dec ( Ord x ∋ y )
|
|
|
104 OrdP x y with trio< x (& y)
|
|
|
105 OrdP x y | tri< a ¬b ¬c = no ¬c
|
|
|
106 OrdP x y | tri≈ ¬a refl ¬c = no ( o<¬≡ refl )
|
|
|
107 OrdP x y | tri> ¬a ¬b c = yes c
|
|
|
108
|
|
470
|
109 -- open import Relation.Binary.HeterogeneousEquality as HE -- using (_≅_;refl)
|
|
469
|
110
|
|
|
111 record Element (A : HOD) : Set (suc n) where
|
|
|
112 field
|
|
|
113 elm : HOD
|
|
|
114 is-elm : A ∋ elm
|
|
|
115
|
|
|
116 open Element
|
|
|
117
|
|
468
|
118 TotalOrderSet : ( A : HOD ) → (_<_ : (x y : HOD) → Set n ) → Set (suc n)
|
|
469
|
119 TotalOrderSet A _<_ = Trichotomous (λ (x : Element A) y → elm x ≡ elm y ) (λ x y → elm x < elm y )
|
|
|
120
|
|
470
|
121 PartialOrderSet : ( A : HOD ) → (_<_ : (x y : HOD) → Set n ) → Set (suc n)
|
|
|
122 PartialOrderSet A _<_ = (a b : Element A)
|
|
|
123 → (elm a < elm b → (¬ (elm b < elm a) ∧ (¬ (elm a ≡ elm b) ))) ∧ (elm a ≡ elm b → (¬ elm a < elm b) ∧ (¬ elm b < elm a))
|
|
|
124
|
|
469
|
125 me : { A a : HOD } → A ∋ a → Element A
|
|
|
126 me {A} {a} lt = record { elm = a ; is-elm = lt }
|
|
|
127
|
|
464
|
128 record SUP ( A B : HOD ) (_<_ : (x y : HOD) → Set n ) : Set (suc n) where
|
|
|
129 field
|
|
|
130 sup : HOD
|
|
|
131 A∋maximal : A ∋ sup
|
|
469
|
132 x≤sup : {x : HOD} → B ∋ x → (x ≡ sup ) ∨ (x < sup )
|
|
464
|
133
|
|
|
134 record Maximal ( A : HOD ) (_<_ : (x y : HOD) → Set n ) : Set (suc n) where
|
|
|
135 field
|
|
|
136 maximal : HOD
|
|
472
|
137 A∋maximal : A ∋ maximal
|
|
469
|
138 ¬maximal<x : {x : HOD} → A ∋ x → ¬ maximal < x
|
|
464
|
139
|
|
467
|
140 record ZChain ( A : HOD ) (y : Ordinal) (_<_ : (x y : HOD) → Set n ) : Set (suc n) where
|
|
464
|
141 field
|
|
467
|
142 B : HOD
|
|
|
143 B⊆A : B ⊆ A
|
|
468
|
144 total : TotalOrderSet B _<_
|
|
467
|
145 fb : {x : HOD } → A ∋ x → HOD
|
|
|
146 B∋fb : (x : HOD ) → (ax : A ∋ x) → B ∋ fb ax
|
|
472
|
147 ¬x≤sup : (sup : HOD) → (as : A ∋ sup ) → & sup o< osuc y → sup < fb as
|
|
464
|
148
|
|
|
149 Zorn-lemma : { A : HOD } → { _<_ : (x y : HOD) → Set n }
|
|
|
150 → o∅ o< & A
|
|
471
|
151 → ( {a b c : HOD} → a < b → b < c → a < c )
|
|
470
|
152 → PartialOrderSet A _<_
|
|
468
|
153 → ( ( B : HOD) → (B⊆A : B ⊆ A) → TotalOrderSet B _<_ → SUP A B _<_ )
|
|
464
|
154 → Maximal A _<_
|
|
471
|
155 Zorn-lemma {A} {_<_} 0<A TR PO supP = zorn00 where
|
|
472
|
156 someA : HOD
|
|
|
157 someA = minimal A (λ eq → ¬x<0 ( subst (λ k → o∅ o< k ) (=od∅→≡o∅ eq) 0<A ))
|
|
473
|
158 isSomeA : A ∋ someA
|
|
|
159 isSomeA = x∋minimal A (λ eq → ¬x<0 ( subst (λ k → o∅ o< k ) (=od∅→≡o∅ eq) 0<A ))
|
|
467
|
160 HasMaximal : HOD
|
|
474
|
161 HasMaximal = record { od = record { def = λ x → odef A x → (m : Ordinal) → odef A m → ¬ (* x < * m)} ; odmax = & A ; <odmax = {!!} } where
|
|
472
|
162 z07 : {y : Ordinal} → ((m : Ordinal) → odef A y ∧ odef A m ∧ (¬ (* y < * m))) → y o< & A
|
|
|
163 z07 {y} p = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) (proj1 (p (& someA)) )))
|
|
474
|
164 no-maximum : HasMaximal =h= od∅ → (x : Ordinal) → odef A x → ((m : Ordinal) → odef A m → ¬ (* x < * m) ) → ⊥
|
|
|
165 no-maximum nomx x ax P = ¬x<0 (eq→ nomx {x} (λ ax m am → P m am ))
|
|
472
|
166 Gtx : { x : HOD} → A ∋ x → HOD
|
|
473
|
167 Gtx {x} ax = record { od = record { def = λ y → odef A y → (x < (* y)) ∧ ( (& x) o< y ) } ; odmax = & A ; <odmax = {!!} }
|
|
474
|
168 no-gtx : { x : HOD} → (ax : A ∋ x ) → Gtx ax =h= od∅ → (( y : Ordinal) → odef A y → (x < (* y)) ∧ ( (& x) o< y )) → ⊥
|
|
|
169 no-gtx {x} ax nogt P = ¬x<0 (eq→ nogt (λ am → P (& x) am ))
|
|
470
|
170 z01 : {a b : HOD} → A ∋ a → A ∋ b → (a ≡ b ) ∨ (a < b ) → b < a → ⊥
|
|
|
171 z01 {a} {b} A∋a A∋b (case1 a=b) b<a = proj1 (proj2 (PO (me A∋b) (me A∋a)) (sym a=b)) b<a
|
|
|
172 z01 {a} {b} A∋a A∋b (case2 a<b) b<a = proj1 (PO (me A∋b) (me A∋a)) b<a ⟪ a<b , (λ b=a → proj1 (proj2 (PO (me A∋b) (me A∋a)) b=a ) b<a ) ⟫
|
|
467
|
173 ZChain→¬SUP : (z : ZChain A (& A) _<_ ) → ¬ (SUP A (ZChain.B z) _<_ )
|
|
470
|
174 ZChain→¬SUP z sp = ⊥-elim (z02 (ZChain.fb z (SUP.A∋maximal sp)) (ZChain.B∋fb z _ (SUP.A∋maximal sp)) (ZChain.¬x≤sup z _ (SUP.A∋maximal sp) z03 )) where
|
|
472
|
175 z03 : & (SUP.sup sp) o< osuc (& A)
|
|
|
176 z03 = ordtrans (c<→o< (SUP.A∋maximal sp)) <-osuc
|
|
470
|
177 z02 : (x : HOD) → ZChain.B z ∋ x → SUP.sup sp < x → ⊥
|
|
473
|
178 z02 x xe s<x = z01 (incl (ZChain.B⊆A z) xe) (SUP.A∋maximal sp) (SUP.x≤sup sp xe) s<x
|
|
471
|
179 ind : HasMaximal =h= od∅
|
|
|
180 → (x : Ordinal) → ((y : Ordinal) → y o< x → ZChain A y _<_ )
|
|
464
|
181 → ZChain A x _<_
|
|
471
|
182 ind nomx x prev with Oprev-p x
|
|
|
183 ... | yes op with ∋-p A (* x)
|
|
473
|
184 ... | no ¬Ax = record { B = ZChain.B zc1 ; B⊆A = ZChain.B⊆A zc1
|
|
|
185 ; total = ZChain.total zc1 ; fb = ZChain.fb zc1 ; B∋fb = ZChain.B∋fb zc1 ; ¬x≤sup = z04 } where
|
|
471
|
186 px = Oprev.oprev op
|
|
|
187 zc1 : ZChain A px _<_
|
|
|
188 zc1 = prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc)
|
|
472
|
189 z04 : (sup : HOD) (as : A ∋ sup) → & sup o< osuc x → sup < ZChain.fb zc1 as
|
|
471
|
190 z04 sup as s<x with trio< (& sup) x
|
|
|
191 ... | tri≈ ¬a b ¬c = ⊥-elim (¬Ax (subst (λ k → odef A k) (trans b (sym &iso)) as) )
|
|
472
|
192 ... | tri< a ¬b ¬c = ZChain.¬x≤sup zc1 _ as ( subst (λ k → & sup o< k ) (sym (Oprev.oprev=x op)) a )
|
|
|
193 ... | tri> ¬a ¬b c with osuc-≡< s<x
|
|
|
194 ... | case1 eq = ⊥-elim (¬Ax (subst (λ k → odef A k) (trans eq (sym &iso)) as) )
|
|
|
195 ... | case2 lt = ⊥-elim (¬a lt )
|
|
473
|
196 ... | yes ax = z06 where
|
|
472
|
197 px = Oprev.oprev op
|
|
|
198 zc1 : ZChain A px _<_
|
|
|
199 zc1 = prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc)
|
|
473
|
200 z06 : ZChain A x _<_
|
|
|
201 z06 with is-o∅ (& (Gtx ax))
|
|
474
|
202 ... | yes nogt = ⊥-elim (no-maximum nomx x (subst (λ k → odef A k) &iso ax) z06-is-maximal ) where
|
|
|
203 z06-is-maximal : (m : Ordinal ) → odef A m → ¬ ( * x < * m )
|
|
|
204 z06-is-maximal m am = z07 where
|
|
|
205 z07 : ¬ ( * x < * m )
|
|
|
206 z07 x<m = proj1 (PO (me ax) (me (subst (λ k → odef A k) (sym &iso) am))) x<m ⟪ {!!} , {!!} ⟫
|
|
|
207 z08 : ( ( y : Ordinal) → odef A y → (* x < (* y)) ∧ ( (& (* x)) o< y )) → ⊥
|
|
|
208 z08 p = no-gtx ax (≡o∅→=od∅ nogt) (λ y ay → p y ay )
|
|
473
|
209 ... | no not = record { B = ZChain.B (prev px (subst (λ k → px o< k ) (Oprev.oprev=x op) <-osuc)) , * x
|
|
|
210 ; B⊆A = {!!} ; total = {!!} ; fb = {!!} ; B∋fb = {!!} ; ¬x≤sup = {!!} }
|
|
|
211 -- minimal (Gtx ax) (λ eq → not (=od∅→≡o∅ eq))
|
|
471
|
212 ind nomx x prev | no ¬ox with trio< (& A) x
|
|
466
|
213 ... | tri< a ¬b ¬c = {!!}
|
|
|
214 ... | tri≈ ¬a b ¬c = {!!}
|
|
|
215 ... | tri> ¬a ¬b c = {!!}
|
|
467
|
216 zorn00 : Maximal A _<_
|
|
|
217 zorn00 with is-o∅ ( & HasMaximal )
|
|
472
|
218 ... | no not = record { maximal = minimal HasMaximal (λ eq → not (=od∅→≡o∅ eq)) ; A∋maximal = zorn01 ; ¬maximal<x = zorn02 } where
|
|
|
219 zorn03 : odef HasMaximal ( & ( minimal HasMaximal (λ eq → not (=od∅→≡o∅ eq)) ) )
|
|
|
220 zorn03 = x∋minimal HasMaximal (λ eq → not (=od∅→≡o∅ eq))
|
|
|
221 zorn01 : A ∋ minimal HasMaximal (λ eq → not (=od∅→≡o∅ eq))
|
|
474
|
222 zorn01 = {!!} -- proj1 (zorn03 ? ? (& someA) isSomeA )
|
|
472
|
223 zorn02 : {x : HOD} → A ∋ x → ¬ (minimal HasMaximal (λ eq → not (=od∅→≡o∅ eq)) < x)
|
|
474
|
224 zorn02 {x} ax m<x = {!!} -- proj2 (zorn03 (& x) ax) (subst₂ (λ j k → j < k) (sym *iso) (sym *iso) m<x )
|
|
471
|
225 ... | yes ¬Maximal = ⊥-elim ( ZChain→¬SUP (z (& A) (≡o∅→=od∅ ¬Maximal)) ( supP B (ZChain.B⊆A (z (& A) (≡o∅→=od∅ ¬Maximal))) (ZChain.total (z (& A) (≡o∅→=od∅ ¬Maximal))) )) where
|
|
|
226 z : (x : Ordinal) → HasMaximal =h= od∅ → ZChain A x _<_
|
|
|
227 z x nomx = TransFinite (ind nomx) x
|
|
|
228 B = ZChain.B (z (& A) (≡o∅→=od∅ ¬Maximal) )
|
|
464
|
229
|
|
431
|
230 open import zfc
|
|
|
231
|
|
|
232 HOD→ZFC : ZFC
|
|
|
233 HOD→ZFC = record {
|
|
|
234 ZFSet = HOD
|
|
|
235 ; _∋_ = _∋_
|
|
|
236 ; _≈_ = _=h=_
|
|
|
237 ; ∅ = od∅
|
|
|
238 ; Select = Select
|
|
|
239 ; isZFC = isZFC
|
|
|
240 } where
|
|
|
241 -- infixr 200 _∈_
|
|
|
242 -- infixr 230 _∩_ _∪_
|
|
|
243 isZFC : IsZFC (HOD ) _∋_ _=h=_ od∅ Select
|
|
|
244 isZFC = record {
|
|
|
245 choice-func = choice-func ;
|
|
|
246 choice = choice
|
|
|
247 } where
|
|
|
248 -- Axiom of choice ( is equivalent to the existence of minimal in our case )
|
|
|
249 -- ∀ X [ ∅ ∉ X → (∃ f : X → ⋃ X ) → ∀ A ∈ X ( f ( A ) ∈ A ) ]
|
|
|
250 choice-func : (X : HOD ) → {x : HOD } → ¬ ( x =h= od∅ ) → ( X ∋ x ) → HOD
|
|
|
251 choice-func X {x} not X∋x = minimal x not
|
|
|
252 choice : (X : HOD ) → {A : HOD } → ( X∋A : X ∋ A ) → (not : ¬ ( A =h= od∅ )) → A ∋ choice-func X not X∋A
|
|
|
253 choice X {A} X∋A not = x∋minimal A not
|
|
|
254
|
