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

comparison src/ODC.agda @ 467:c65cb6c07a38

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 23 Mar 2022 16:42:42 +0900
parents 14b0e0aa6487
children c70cf01b29f9
comparison
equal deleted inserted replaced
466:14b0e0aa6487 467:c65cb6c07a38
38 postulate 38 postulate
39 -- mimimul and x∋minimal is an Axiom of choice 39 -- mimimul and x∋minimal is an Axiom of choice
40 minimal : (x : HOD ) → ¬ (x =h= od∅ )→ HOD 40 minimal : (x : HOD ) → ¬ (x =h= od∅ )→ HOD
41 -- this should be ¬ (x =h= od∅ )→ ∃ ox → x ∋ Ord ox ( minimum of x ) 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 ) ) 42 x∋minimal : (x : HOD ) → ( ne : ¬ (x =h= od∅ ) ) → odef x ( & ( minimal x ne ) )
43 -- minimality (may proved by ε-induction with LEM) 43 -- minimality (proved by ε-induction with LEM)
44 minimal-1 : (x : HOD ) → ( ne : ¬ (x =h= od∅ ) ) → (y : HOD ) → ¬ ( odef (minimal x ne) (& y)) ∧ (odef x (& y) ) 44 minimal-1 : (x : HOD ) → ( ne : ¬ (x =h= od∅ ) ) → (y : HOD ) → ¬ ( odef (minimal x ne) (& y)) ∧ (odef x (& y) )
45 45
46 46
47 -- 47 --
48 -- Axiom of choice in intutionistic logic implies the exclude middle 48 -- Axiom of choice in intutionistic logic implies the exclude middle
109 record SUP ( A B : HOD ) (_<_ : (x y : HOD) → Set n ) : Set (suc n) where 109 record SUP ( A B : HOD ) (_<_ : (x y : HOD) → Set n ) : Set (suc n) where
110 field 110 field
111 sup : HOD 111 sup : HOD
112 A∋maximal : A ∋ sup 112 A∋maximal : A ∋ sup
113 tri : {a b : HOD} → B ∋ a → B ∋ b → (a < b) ∨ (a ≡ b) ∨ (b < a ) 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 ) 114 x≤sup : (x : HOD) → B ∋ x → (x ≡ sup ) ∨ (x < sup )
115 115
116 record Maximal ( A : HOD ) (_<_ : (x y : HOD) → Set n ) : Set (suc n) where 116 record Maximal ( A : HOD ) (_<_ : (x y : HOD) → Set n ) : Set (suc n) where
117 field 117 field
118 maximal : HOD 118 maximal : HOD
119 A∋maximal : HOD 119 A∋maximal : HOD
120 ¬maximal<x : (x : HOD) → (b : A ∋ x ) → ¬ maximal < x 120 ¬maximal<x : (x : HOD) → (b : A ∋ x ) → ¬ maximal < x
121 121
122 record ZChain ( A : HOD ) (x : Ordinal) (_<_ : (x y : HOD) → Set n ) : Set (suc n) where 122 record ZChain ( A : HOD ) (y : Ordinal) (_<_ : (x y : HOD) → Set n ) : Set (suc n) where
123 field 123 field
124 NOMAX : HOD 124 B : HOD
125 Chain : HOD 125 B⊆A : B ⊆ A
126 nomax : (y m : Ordinal) → odef NOMAX y → y o< x → ¬ ( * y < * m ) 126 tri : {a b : HOD} → B ∋ a → B ∋ b → (a < b) ∨ (a ≡ b) ∨ (b < a )
127 chain : (y : Ordinal) → odef Chain y → & NOMAX ≡ o∅ → SUP A (* y) _<_ 127 fb : {x : HOD } → A ∋ x → HOD
128 B∋fb : (x : HOD ) → (ax : A ∋ x) → B ∋ fb ax
129 ¬x≤sup : (sup : HOD) → (as : A ∋ sup ) → & sup o< y → sup < fb as
128 130
129 Zorn-lemma : { A : HOD } → { _<_ : (x y : HOD) → Set n } 131 Zorn-lemma : { A : HOD } → { _<_ : (x y : HOD) → Set n }
130 → o∅ o< & A 132 → o∅ o< & A
131 → ( ( B : HOD) → (B⊆A : B ⊆ A) → SUP A B _<_ ) 133 → ( ( B : HOD) → (B⊆A : B ⊆ A) → SUP A B _<_ )
132 → Maximal A _<_ 134 → Maximal A _<_
133 Zorn-lemma {A} {_<_} 0<A SUP = zorn01 (TransFinite ind (& A)) where 135 Zorn-lemma {A} {_<_} 0<A supP = zorn00 where
134 HasGreater : Ordinal → HOD 136 HasMaximal : HOD
135 HasGreater m = record { od = record { def = λ x → odef A x ∧ (* m < * x) } ; odmax = & A ; <odmax = {!!} } 137 HasMaximal = record { od = record { def = λ x → (m : Ordinal) → odef A x ∧ odef A m ∧ (¬ (* x < * m))} ; odmax = & A ; <odmax = {!!} }
136 zorn01 : ZChain A (& A) _<_ → Maximal A _<_ 138 ZChain→¬SUP : (z : ZChain A (& A) _<_ ) → ¬ (SUP A (ZChain.B z) _<_ )
137 zorn01 zc with is-o∅ ( & (ZChain.NOMAX zc) ) 139 ZChain→¬SUP z sp = {!!}
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)) ) {!!} {!!} }
141 ind : (x : Ordinal) → ((y : Ordinal) → y o< x → ZChain A y _<_ ) 140 ind : (x : Ordinal) → ((y : Ordinal) → y o< x → ZChain A y _<_ )
142 → ZChain A x _<_ 141 → ZChain A x _<_
143 ind x prev with Oprev-p x 142 ind x prev with Oprev-p x
144 ... | yes ox with is-o∅ (& (HasGreater x)) 143 ... | yes _ = {!!}
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 144 ind x prev | no ¬ox with trio< (& A) x
148 ... | tri< a ¬b ¬c = {!!} 145 ... | tri< a ¬b ¬c = {!!}
149 ... | tri≈ ¬a b ¬c = {!!} 146 ... | tri≈ ¬a b ¬c = {!!}
150 ... | tri> ¬a ¬b c = {!!} 147 ... | tri> ¬a ¬b c = {!!}
148 zorn00 : Maximal A _<_
149 zorn00 with is-o∅ ( & HasMaximal )
150 ... | no not = record { maximal = minimal HasMaximal (λ eq → not (=od∅→≡o∅ eq)) ; A∋maximal = {!!}; ¬maximal<x = {!!} }
151 ... | yes ¬Maximal = ⊥-elim ( ZChain→¬SUP (z (& A)) ( supP (ZChain.B (z (& A))) (ZChain.B⊆A (z (& A))) ) ) where
152 z : (x : Ordinal) → ZChain A x _<_
153 z = TransFinite ind
151 154
152 open import zfc 155 open import zfc
153 156
154 HOD→ZFC : ZFC 157 HOD→ZFC : ZFC
155 HOD→ZFC = record { 158 HOD→ZFC = record {