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

comparison OD.agda @ 304:2c111bfcc89a

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
HOD using <maxod
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 29 Jun 2020 18:31:56 +0900
parents 7963b76df6e1
children 4804f3f3485f
comparison
equal deleted inserted replaced
303:7963b76df6e1 304:2c111bfcc89a
75 Ords = record { def = λ x → One } 75 Ords = record { def = λ x → One }
76 76
77 record HOD : Set (suc n) where 77 record HOD : Set (suc n) where
78 field 78 field
79 od : OD 79 od : OD
80 ¬odmax : ¬ (od ≡ Ords) 80 odmax : Ordinal
81 <odmax : {x : Ordinal} → def od x → x o< odmax
81 82
82 record OrdinalSubset (maxordinal : Ordinal) : Set (suc n) where 83 record OrdinalSubset (maxordinal : Ordinal) : Set (suc n) where
83 field 84 field
84 os→ : (x : Ordinal) → x o< maxordinal → Ordinal 85 os→ : (x : Ordinal) → x o< maxordinal → Ordinal
85 os← : Ordinal → Ordinal 86 os← : Ordinal → Ordinal
87 os-iso← : {x : Ordinal} → os→ (os← x) (os←limit x) ≡ x 88 os-iso← : {x : Ordinal} → os→ (os← x) (os←limit x) ≡ x
88 os-iso→ : {x : Ordinal} → (lt : x o< maxordinal ) → os← (os→ x lt) ≡ x 89 os-iso→ : {x : Ordinal} → (lt : x o< maxordinal ) → os← (os→ x lt) ≡ x
89 90
90 open HOD 91 open HOD
91 92
92 -- HOD→OD : {x : Ordinal} → HOD x → OD
93 -- HOD→OD hod = record { def = hdef {!!} }
94
95 record ODAxiom : Set (suc n) where 93 record ODAxiom : Set (suc n) where
96 -- OD can be iso to a subset of Ordinal ( by means of Godel Set )
97 field 94 field
95 -- HOD is isomorphic to Ordinal (by means of Goedel number)
98 od→ord : HOD → Ordinal 96 od→ord : HOD → Ordinal
99 ord→od : Ordinal → HOD 97 ord→od : Ordinal → HOD
100 c<→o< : {x y : HOD } → def (od y) ( od→ord x ) → od→ord x o< od→ord y 98 c<→o< : {x y : HOD } → def (od y) ( od→ord x ) → od→ord x o< od→ord y
101 oiso : {x : HOD } → ord→od ( od→ord x ) ≡ x 99 oiso : {x : HOD } → ord→od ( od→ord x ) ≡ x
102 diso : {x : Ordinal } → od→ord ( ord→od x ) ≡ x 100 diso : {x : Ordinal } → od→ord ( ord→od x ) ≡ x
112 open ODAxiom odAxiom 110 open ODAxiom odAxiom
113 111
114 -- maxod : {x : OD} → od→ord x o< od→ord Ords 112 -- maxod : {x : OD} → od→ord x o< od→ord Ords
115 -- maxod {x} = c<→o< OneObj 113 -- maxod {x} = c<→o< OneObj
116 114
117 -- we have to avoid this contradiction 115 -- we have not this contradiction
118
119 -- bad-bad : ⊥ 116 -- bad-bad : ⊥
120 -- bad-bad = osuc-< <-osuc (c<→o< { record { def = λ x → One }} OneObj) 117 -- bad-bad = osuc-< <-osuc (c<→o< { record { od = record { def = λ x → One }; <odmax = {!!} } } OneObj)
121 118
122 -- Ordinal in OD ( and ZFSet ) Transitive Set 119 -- Ordinal in OD ( and ZFSet ) Transitive Set
123 Ord : ( a : Ordinal ) → HOD 120 Ord : ( a : Ordinal ) → HOD
124 Ord a = record { od = record { def = λ y → y o< a } ; ¬odmax = ? } 121 Ord a = record { od = record { def = λ y → y o< a } ; odmax = a ; <odmax = lemma } where
122 lemma : {x : Ordinal} → x o< a → x o< a
123 lemma {x} lt = lt
125 124
126 od∅ : HOD 125 od∅ : HOD
127 od∅ = Ord o∅ 126 od∅ = Ord o∅
128 127
129 sup-o : ( HOD → Ordinal ) → Ordinal 128 sup-o : ( HOD → Ordinal ) → Ordinal
130 sup-o = ? 129 sup-o = {!!}
131 sup-o< : { ψ : HOD → Ordinal } → ∀ {x : HOD } → ψ x o< sup-o ψ 130 sup-o< : { ψ : HOD → Ordinal } → ∀ {x : HOD } → ψ x o< sup-o ψ
132 sup-o< = ? 131 sup-o< = {!!}
133 132
134 odef : HOD → Ordinal → Set n 133 odef : HOD → Ordinal → Set n
135 odef A x = def ( od A ) x 134 odef A x = def ( od A ) x
136 135
137 o<→c<→HOD=Ord : ( {x y : Ordinal } → x o< y → odef (ord→od y) x ) → {x : HOD } → x ≡ Ord (od→ord x) 136 o<→c<→HOD=Ord : ( {x y : Ordinal } → x o< y → odef (ord→od y) x ) → {x : HOD } → x ≡ Ord (od→ord x)
146 145
147 _c<_ : ( x a : HOD ) → Set n 146 _c<_ : ( x a : HOD ) → Set n
148 x c< a = a ∋ x 147 x c< a = a ∋ x
149 148
150 cseq : {n : Level} → HOD → HOD 149 cseq : {n : Level} → HOD → HOD
151 cseq x = record { od = record { def = λ y → odef x (osuc y) } ; ¬odmax = ? } where 150 cseq x = record { od = record { def = λ y → odef x (osuc y) } ; odmax = {!!} ; <odmax = {!!} } where
152 151
153 odef-subst : {Z : HOD } {X : Ordinal }{z : HOD } {x : Ordinal }→ odef Z X → Z ≡ z → X ≡ x → odef z x 152 odef-subst : {Z : HOD } {X : Ordinal }{z : HOD } {x : Ordinal }→ odef Z X → Z ≡ z → X ≡ x → odef z x
154 odef-subst df refl refl = df 153 odef-subst df refl refl = df
155 154
156 otrans : {n : Level} {a x y : Ordinal } → odef (Ord a) x → odef (Ord x) y → odef (Ord a) y 155 otrans : {n : Level} {a x y : Ordinal } → odef (Ord a) x → odef (Ord x) y → odef (Ord a) y
214 is-o∅ x | tri< a ¬b ¬c = no ¬b 213 is-o∅ x | tri< a ¬b ¬c = no ¬b
215 is-o∅ x | tri≈ ¬a b ¬c = yes b 214 is-o∅ x | tri≈ ¬a b ¬c = yes b
216 is-o∅ x | tri> ¬a ¬b c = no ¬b 215 is-o∅ x | tri> ¬a ¬b c = no ¬b
217 216
218 _,_ : HOD → HOD → HOD 217 _,_ : HOD → HOD → HOD
219 x , y = record { od = record { def = λ t → (t ≡ od→ord x ) ∨ ( t ≡ od→ord y ) } ; ¬odmax = ? } -- Ord (omax (od→ord x) (od→ord y)) 218 x , y = record { od = record { def = λ t → (t ≡ od→ord x ) ∨ ( t ≡ od→ord y ) } ; odmax = {!!} ; <odmax = {!!} } -- Ord (omax (od→ord x) (od→ord y))
220 219
221 -- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 220 -- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ )
222 -- postulate f-extensionality : { n : Level} → Relation.Binary.PropositionalEquality.Extensionality n (suc n) 221 -- postulate f-extensionality : { n : Level} → Relation.Binary.PropositionalEquality.Extensionality n (suc n)
223 222
224 in-codomain : (X : HOD ) → ( ψ : HOD → HOD ) → HOD 223 in-codomain : (X : HOD ) → ( ψ : HOD → HOD ) → HOD
225 in-codomain X ψ = record { od = record { def = λ x → ¬ ( (y : Ordinal ) → ¬ ( odef X y ∧ ( x ≡ od→ord (ψ (ord→od y ))))) } ; ¬odmax = ? } 224 in-codomain X ψ = record { od = record { def = λ x → ¬ ( (y : Ordinal ) → ¬ ( odef X y ∧ ( x ≡ od→ord (ψ (ord→od y ))))) } ; odmax = {!!} ; <odmax = {!!} }
226 225
227 -- Power Set of X ( or constructible by λ y → odef X (od→ord y ) 226 -- Power Set of X ( or constructible by λ y → odef X (od→ord y )
228 227
229 ZFSubset : (A x : HOD ) → HOD 228 ZFSubset : (A x : HOD ) → HOD
230 ZFSubset A x = record { od = record { def = λ y → odef A y ∧ odef x y } ; ¬odmax = ? } -- roughly x = A → Set 229 ZFSubset A x = record { od = record { def = λ y → odef A y ∧ odef x y } ; odmax = {!!} ; <odmax = {!!} } -- roughly x = A → Set
231 230
232 OPwr : (A : HOD ) → HOD 231 OPwr : (A : HOD ) → HOD
233 OPwr A = Ord ( sup-o ( λ x → od→ord ( ZFSubset A x) ) ) 232 OPwr A = Ord ( sup-o ( λ x → od→ord ( ZFSubset A x) ) )
234 233
235 -- _⊆_ : ( A B : HOD ) → ∀{ x : HOD } → Set n 234 -- _⊆_ : ( A B : HOD ) → ∀{ x : HOD } → Set n
277 ; infinite = infinite 276 ; infinite = infinite
278 ; isZF = isZF 277 ; isZF = isZF
279 } where 278 } where
280 ZFSet = HOD -- is less than Ords because of maxod 279 ZFSet = HOD -- is less than Ords because of maxod
281 Select : (X : HOD ) → ((x : HOD ) → Set n ) → HOD 280 Select : (X : HOD ) → ((x : HOD ) → Set n ) → HOD
282 Select X ψ = record { od = record { def = λ x → ( odef X x ∧ ψ ( ord→od x )) } ; ¬odmax = ? } 281 Select X ψ = record { od = record { def = λ x → ( odef X x ∧ ψ ( ord→od x )) } ; odmax = {!!} ; <odmax = {!!} }
283 Replace : HOD → (HOD → HOD ) → HOD 282 Replace : HOD → (HOD → HOD ) → HOD
284 Replace X ψ = record { od = record { def = λ x → (x o< sup-o ( λ x → od→ord (ψ x))) ∧ odef (in-codomain X ψ) x } ; ¬odmax = ? } 283 Replace X ψ = record { od = record { def = λ x → (x o< sup-o ( λ x → od→ord (ψ x))) ∧ odef (in-codomain X ψ) x } ; odmax = {!!} ; <odmax = {!!} }
285 _∩_ : ( A B : ZFSet ) → ZFSet 284 _∩_ : ( A B : ZFSet ) → ZFSet
286 A ∩ B = record { od = record { def = λ x → odef A x ∧ odef B x } ; ¬odmax = ? } 285 A ∩ B = record { od = record { def = λ x → odef A x ∧ odef B x } ; odmax = {!!} ; <odmax = {!!} }
287 Union : HOD → HOD 286 Union : HOD → HOD
288 Union U = record { od = record { def = λ x → ¬ (∀ (u : Ordinal ) → ¬ ((odef U u) ∧ (odef (ord→od u) x))) } ; ¬odmax = ? } 287 Union U = record { od = record { def = λ x → ¬ (∀ (u : Ordinal ) → ¬ ((odef U u) ∧ (odef (ord→od u) x))) } ; odmax = {!!} ; <odmax = {!!} }
289 _∈_ : ( A B : ZFSet ) → Set n 288 _∈_ : ( A B : ZFSet ) → Set n
290 A ∈ B = B ∋ A 289 A ∈ B = B ∋ A
291 Power : HOD → HOD 290 Power : HOD → HOD
292 Power A = Replace (OPwr (Ord (od→ord A))) ( λ x → A ∩ x ) 291 Power A = Replace (OPwr (Ord (od→ord A))) ( λ x → A ∩ x )
293 -- ｛_｝ : ZFSet → ZFSet 292 -- ｛_｝ : ZFSet → ZFSet
297 iφ : infinite-d o∅ 296 iφ : infinite-d o∅
298 isuc : {x : Ordinal } → infinite-d x → 297 isuc : {x : Ordinal } → infinite-d x →
299 infinite-d (od→ord ( Union (ord→od x , (ord→od x , ord→od x ) ) )) 298 infinite-d (od→ord ( Union (ord→od x , (ord→od x , ord→od x ) ) ))
300 299
301 infinite : HOD 300 infinite : HOD
302 infinite = record { od = record { def = λ x → infinite-d x } ; ¬odmax = ? } 301 infinite = record { od = record { def = λ x → infinite-d x } ; odmax = {!!} ; <odmax = {!!} }
303 302
304 _=h=_ : (x y : HOD) → Set n 303 _=h=_ : (x y : HOD) → Set n
305 x =h= y = od x == od y 304 x =h= y = od x == od y
306 305
307 infixr 200 _∈_ 306 infixr 200 _∈_
362 selection {ψ} {X} {y} = record { 361 selection {ψ} {X} {y} = record {
363 proj1 = λ cond → record { proj1 = proj1 cond ; proj2 = ψiso {ψ} (proj2 cond) (sym oiso) } 362 proj1 = λ cond → record { proj1 = proj1 cond ; proj2 = ψiso {ψ} (proj2 cond) (sym oiso) }
364 ; proj2 = λ select → record { proj1 = proj1 select ; proj2 = ψiso {ψ} (proj2 select) oiso } 363 ; proj2 = λ select → record { proj1 = proj1 select ; proj2 = ψiso {ψ} (proj2 select) oiso }
365 } 364 }
366 replacement← : {ψ : HOD → HOD} (X x : HOD) → X ∋ x → Replace X ψ ∋ ψ x 365 replacement← : {ψ : HOD → HOD} (X x : HOD) → X ∋ x → Replace X ψ ∋ ψ x
367 replacement← {ψ} X x lt = record { proj1 = ? ; proj2 = lemma } where -- sup-c< ψ {x} 366 replacement← {ψ} X x lt = record { proj1 = {!!} ; proj2 = lemma } where -- sup-c< ψ {x}
368 lemma : odef (in-codomain X ψ) (od→ord (ψ x)) 367 lemma : odef (in-codomain X ψ) (od→ord (ψ x))
369 lemma not = ⊥-elim ( not ( od→ord x ) (record { proj1 = lt ; proj2 = cong (λ k → od→ord (ψ k)) (sym oiso)} )) 368 lemma not = ⊥-elim ( not ( od→ord x ) (record { proj1 = lt ; proj2 = cong (λ k → od→ord (ψ k)) (sym oiso)} ))
370 replacement→ : {ψ : HOD → HOD} (X x : HOD) → (lt : Replace X ψ ∋ x) → ¬ ( (y : HOD) → ¬ (x =h= ψ y)) 369 replacement→ : {ψ : HOD → HOD} (X x : HOD) → (lt : Replace X ψ ∋ x) → ¬ ( (y : HOD) → ¬ (x =h= ψ y))
371 replacement→ {ψ} X x lt = contra-position lemma (lemma2 (proj2 lt)) where 370 replacement→ {ψ} X x lt = contra-position lemma (lemma2 (proj2 lt)) where
372 lemma2 : ¬ ((y : Ordinal) → ¬ odef X y ∧ ((od→ord x) ≡ od→ord (ψ (ord→od y)))) 371 lemma2 : ¬ ((y : Ordinal) → ¬ odef X y ∧ ((od→ord x) ≡ od→ord (ψ (ord→od y))))