|
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
|
|
469
|
109 open import Relation.Binary.HeterogeneousEquality as HE -- using (_≅_;refl)
|
|
|
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
|
|
|
121 me : { A a : HOD } → A ∋ a → Element A
|
|
|
122 me {A} {a} lt = record { elm = a ; is-elm = lt }
|
|
|
123
|
|
|
124 -- elm-cmp : {A a b : HOD} → {_<_ : (x y : HOD) → Set n } → A ∋ a → A ∋ b → TotalOrderSet A _<_ → Tri _ _ _
|
|
|
125 -- elm-cmp {A} {a} {b} ax bx cmp = cmp (me ax) (me bx)
|
|
468
|
126
|
|
464
|
127 record SUP ( A B : HOD ) (_<_ : (x y : HOD) → Set n ) : Set (suc n) where
|
|
|
128 field
|
|
|
129 sup : HOD
|
|
|
130 A∋maximal : A ∋ sup
|
|
469
|
131 x≤sup : {x : HOD} → B ∋ x → (x ≡ sup ) ∨ (x < sup )
|
|
464
|
132
|
|
|
133 record Maximal ( A : HOD ) (_<_ : (x y : HOD) → Set n ) : Set (suc n) where
|
|
|
134 field
|
|
|
135 maximal : HOD
|
|
|
136 A∋maximal : HOD
|
|
469
|
137 ¬maximal<x : {x : HOD} → A ∋ x → ¬ maximal < x
|
|
464
|
138
|
|
467
|
139 record ZChain ( A : HOD ) (y : Ordinal) (_<_ : (x y : HOD) → Set n ) : Set (suc n) where
|
|
464
|
140 field
|
|
467
|
141 B : HOD
|
|
|
142 B⊆A : B ⊆ A
|
|
468
|
143 total : TotalOrderSet B _<_
|
|
467
|
144 fb : {x : HOD } → A ∋ x → HOD
|
|
|
145 B∋fb : (x : HOD ) → (ax : A ∋ x) → B ∋ fb ax
|
|
|
146 ¬x≤sup : (sup : HOD) → (as : A ∋ sup ) → & sup o< y → sup < fb as
|
|
464
|
147
|
|
|
148 Zorn-lemma : { A : HOD } → { _<_ : (x y : HOD) → Set n }
|
|
|
149 → o∅ o< & A
|
|
468
|
150 → ( ( B : HOD) → (B⊆A : B ⊆ A) → TotalOrderSet B _<_ → SUP A B _<_ )
|
|
464
|
151 → Maximal A _<_
|
|
467
|
152 Zorn-lemma {A} {_<_} 0<A supP = zorn00 where
|
|
|
153 HasMaximal : HOD
|
|
|
154 HasMaximal = record { od = record { def = λ x → (m : Ordinal) → odef A x ∧ odef A m ∧ (¬ (* x < * m))} ; odmax = & A ; <odmax = {!!} }
|
|
469
|
155 z01 : {B a b : HOD} → TotalOrderSet B _<_ → B ∋ a → B ∋ b → (a ≡ b ) ∨ (a < b ) → b < a → ⊥
|
|
|
156 z01 {B} {a} {b} Tri B∋a B∋b (case1 a=b) b<a with Tri (me B∋a) (me B∋b)
|
|
|
157 ... | tri< a₁ ¬b ¬c = ¬b a=b
|
|
|
158 ... | tri≈ ¬a b₁ ¬c = ¬c b<a
|
|
|
159 ... | tri> ¬a ¬b c = ¬b a=b
|
|
|
160 z01 {B} {a} {b} Tri B∋a B∋b (case2 a<b) b<a with Tri (me B∋a) (me B∋b)
|
|
|
161 ... | tri< a₁ ¬b ¬c = ¬c b<a
|
|
|
162 ... | tri≈ ¬a b₁ ¬c = ¬c b<a
|
|
|
163 ... | tri> ¬a ¬b c = ¬a a<b
|
|
467
|
164 ZChain→¬SUP : (z : ZChain A (& A) _<_ ) → ¬ (SUP A (ZChain.B z) _<_ )
|
|
469
|
165 ZChain→¬SUP z sp = ⊥-elim {!!} where
|
|
|
166 z02 : (x : HOD) → ZChain.B z ∋ x → ⊥
|
|
|
167 z02 x xe = ( z01 (ZChain.total z) xe {!!} (SUP.x≤sup sp xe) {!!} )
|
|
464
|
168 ind : (x : Ordinal) → ((y : Ordinal) → y o< x → ZChain A y _<_ )
|
|
|
169 → ZChain A x _<_
|
|
466
|
170 ind x prev with Oprev-p x
|
|
467
|
171 ... | yes _ = {!!}
|
|
466
|
172 ind x prev | no ¬ox with trio< (& A) x
|
|
|
173 ... | tri< a ¬b ¬c = {!!}
|
|
|
174 ... | tri≈ ¬a b ¬c = {!!}
|
|
|
175 ... | tri> ¬a ¬b c = {!!}
|
|
467
|
176 zorn00 : Maximal A _<_
|
|
|
177 zorn00 with is-o∅ ( & HasMaximal )
|
|
|
178 ... | no not = record { maximal = minimal HasMaximal (λ eq → not (=od∅→≡o∅ eq)) ; A∋maximal = {!!}; ¬maximal<x = {!!} }
|
|
468
|
179 ... | yes ¬Maximal = ⊥-elim ( ZChain→¬SUP (z (& A)) ( supP B (ZChain.B⊆A (z (& A))) (ZChain.total (z (& A)))) ) where
|
|
467
|
180 z : (x : Ordinal) → ZChain A x _<_
|
|
|
181 z = TransFinite ind
|
|
468
|
182 B = ZChain.B (z (& A))
|
|
464
|
183
|
|
431
|
184 open import zfc
|
|
|
185
|
|
|
186 HOD→ZFC : ZFC
|
|
|
187 HOD→ZFC = record {
|
|
|
188 ZFSet = HOD
|
|
|
189 ; _∋_ = _∋_
|
|
|
190 ; _≈_ = _=h=_
|
|
|
191 ; ∅ = od∅
|
|
|
192 ; Select = Select
|
|
|
193 ; isZFC = isZFC
|
|
|
194 } where
|
|
|
195 -- infixr 200 _∈_
|
|
|
196 -- infixr 230 _∩_ _∪_
|
|
|
197 isZFC : IsZFC (HOD ) _∋_ _=h=_ od∅ Select
|
|
|
198 isZFC = record {
|
|
|
199 choice-func = choice-func ;
|
|
|
200 choice = choice
|
|
|
201 } where
|
|
|
202 -- Axiom of choice ( is equivalent to the existence of minimal in our case )
|
|
|
203 -- ∀ X [ ∅ ∉ X → (∃ f : X → ⋃ X ) → ∀ A ∈ X ( f ( A ) ∈ A ) ]
|
|
|
204 choice-func : (X : HOD ) → {x : HOD } → ¬ ( x =h= od∅ ) → ( X ∋ x ) → HOD
|
|
|
205 choice-func X {x} not X∋x = minimal x not
|
|
|
206 choice : (X : HOD ) → {A : HOD } → ( X∋A : X ∋ A ) → (not : ¬ ( A =h= od∅ )) → A ∋ choice-func X not X∋A
|
|
|
207 choice X {A} X∋A not = x∋minimal A not
|
|
|
208
|
