|
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 ) )
|
|
|
43 -- minimality (may proved by ε-induction with LEM)
|
|
|
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
|
|
464
|
109 record SUP ( A B : HOD ) (_<_ : (x y : HOD) → Set n ) : Set (suc n) where
|
|
|
110 field
|
|
|
111 sup : HOD
|
|
|
112 A∋maximal : A ∋ sup
|
|
|
113 tri : {a b : HOD} → B ∋ a → B ∋ b → (a < b) ∨ (a ≡ b) ∨ (b < a )
|
|
|
114 x≤sup : (x : HOD) → (b : B ∋ x ) → (x ≡ sup ) ∨ (x < sup )
|
|
|
115
|
|
|
116 record Maximal ( A : HOD ) (_<_ : (x y : HOD) → Set n ) : Set (suc n) where
|
|
|
117 field
|
|
|
118 maximal : HOD
|
|
|
119 A∋maximal : HOD
|
|
|
120 ¬maximal<x : (x : HOD) → (b : A ∋ x ) → ¬ maximal < x
|
|
|
121
|
|
|
122 record ZChain ( A : HOD ) (x : Ordinal) (_<_ : (x y : HOD) → Set n ) : Set (suc n) where
|
|
|
123 field
|
|
466
|
124 NOMAX : HOD
|
|
|
125 Chain : HOD
|
|
|
126 nomax : (y m : Ordinal) → odef NOMAX y → y o< x → ¬ ( * y < * m )
|
|
|
127 chain : (y : Ordinal) → odef Chain y → & NOMAX ≡ o∅ → SUP A (* y) _<_
|
|
464
|
128
|
|
|
129 Zorn-lemma : { A : HOD } → { _<_ : (x y : HOD) → Set n }
|
|
|
130 → o∅ o< & A
|
|
|
131 → ( ( B : HOD) → (B⊆A : B ⊆ A) → SUP A B _<_ )
|
|
|
132 → Maximal A _<_
|
|
466
|
133 Zorn-lemma {A} {_<_} 0<A SUP = zorn01 (TransFinite ind (& A)) where
|
|
464
|
134 HasGreater : Ordinal → HOD
|
|
|
135 HasGreater m = record { od = record { def = λ x → odef A x ∧ (* m < * x) } ; odmax = & A ; <odmax = {!!} }
|
|
466
|
136 zorn01 : ZChain A (& A) _<_ → Maximal A _<_
|
|
|
137 zorn01 zc with is-o∅ ( & (ZChain.NOMAX zc) )
|
|
|
138 ... | yes _ = {!!}
|
|
|
139 ... | no not = record { maximal = minimal (ZChain.NOMAX zc) (λ eq → not (=od∅→≡o∅ eq)) ; A∋maximal = {!!}
|
|
|
140 ; ¬maximal<x = λ x lt m<x → ZChain.nomax zc {!!} {!!} (x∋minimal (ZChain.NOMAX zc) (λ eq → not (=od∅→≡o∅ eq)) ) {!!} {!!} }
|
|
464
|
141 ind : (x : Ordinal) → ((y : Ordinal) → y o< x → ZChain A y _<_ )
|
|
|
142 → ZChain A x _<_
|
|
466
|
143 ind x prev with Oprev-p x
|
|
|
144 ... | yes ox with is-o∅ (& (HasGreater x))
|
|
|
145 ... | yes _ = record { NOMAX = {!!} ; nomax = {!!} ; Chain = {!!} ; chain = {!!} } where
|
|
|
146 ... | no _ = record { NOMAX = {!!} ; nomax = {!!} ; Chain = {!!} ; chain = {!!} } where
|
|
|
147 ind x prev | no ¬ox with trio< (& A) x
|
|
|
148 ... | tri< a ¬b ¬c = {!!}
|
|
|
149 ... | tri≈ ¬a b ¬c = {!!}
|
|
|
150 ... | tri> ¬a ¬b c = {!!}
|
|
464
|
151
|
|
431
|
152 open import zfc
|
|
|
153
|
|
|
154 HOD→ZFC : ZFC
|
|
|
155 HOD→ZFC = record {
|
|
|
156 ZFSet = HOD
|
|
|
157 ; _∋_ = _∋_
|
|
|
158 ; _≈_ = _=h=_
|
|
|
159 ; ∅ = od∅
|
|
|
160 ; Select = Select
|
|
|
161 ; isZFC = isZFC
|
|
|
162 } where
|
|
|
163 -- infixr 200 _∈_
|
|
|
164 -- infixr 230 _∩_ _∪_
|
|
|
165 isZFC : IsZFC (HOD ) _∋_ _=h=_ od∅ Select
|
|
|
166 isZFC = record {
|
|
|
167 choice-func = choice-func ;
|
|
|
168 choice = choice
|
|
|
169 } where
|
|
|
170 -- Axiom of choice ( is equivalent to the existence of minimal in our case )
|
|
|
171 -- ∀ X [ ∅ ∉ X → (∃ f : X → ⋃ X ) → ∀ A ∈ X ( f ( A ) ∈ A ) ]
|
|
|
172 choice-func : (X : HOD ) → {x : HOD } → ¬ ( x =h= od∅ ) → ( X ∋ x ) → HOD
|
|
|
173 choice-func X {x} not X∋x = minimal x not
|
|
|
174 choice : (X : HOD ) → {A : HOD } → ( X∋A : X ∋ A ) → (not : ¬ ( A =h= od∅ )) → A ∋ choice-func X not X∋A
|
|
|
175 choice X {A} X∋A not = x∋minimal A not
|
|
|
176
|
