Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison OD.agda @ 190:6e778b0a7202
add filter
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Fri, 26 Jul 2019 21:08:06 +0900 |
parents | 540b845ea2de |
children | 9eb6a8691f02 |
comparison
equal
deleted
inserted
replaced
189:540b845ea2de | 190:6e778b0a7202 |
---|---|
196 | 196 |
197 -- | 197 -- |
198 -- Axiom of choice in intutionistic logic implies the exclude middle | 198 -- Axiom of choice in intutionistic logic implies the exclude middle |
199 -- https://plato.stanford.edu/entries/axiom-choice/#AxiChoLog | 199 -- https://plato.stanford.edu/entries/axiom-choice/#AxiChoLog |
200 -- | 200 -- |
201 p∨¬p : { n : Level } → ( p : Set (suc n) ) → p ∨ ( ¬ p ) | 201 p∨¬p : { n : Level } → ( p : Set (suc n) ) → p ∨ ( ¬ p ) -- assuming axiom of choice |
202 p∨¬p {n} p with is-o∅ ( od→ord ( record { def = λ x → p } )) | 202 p∨¬p {n} p with is-o∅ ( od→ord ( record { def = λ x → p } )) |
203 p∨¬p {n} p | yes eq = case2 (¬p eq) where | 203 p∨¬p {n} p | yes eq = case2 (¬p eq) where |
204 ps = record { def = λ x → p } | 204 ps = record { def = λ x → p } |
205 lemma : ps == od∅ → p → ⊥ | 205 lemma : ps == od∅ → p → ⊥ |
206 lemma eq p0 = ¬x<0 {n} {od→ord ps} (eq→ eq p0 ) | 206 lemma eq p0 = ¬x<0 {n} {od→ord ps} (eq→ eq p0 ) |
211 eqo∅ : ps == od∅ {suc n} → od→ord ps ≡ o∅ {suc n} | 211 eqo∅ : ps == od∅ {suc n} → od→ord ps ≡ o∅ {suc n} |
212 eqo∅ eq = subst (λ k → od→ord ps ≡ k) ord-od∅ ( cong (λ k → od→ord k ) (==→o≡ eq)) | 212 eqo∅ eq = subst (λ k → od→ord ps ≡ k) ord-od∅ ( cong (λ k → od→ord k ) (==→o≡ eq)) |
213 lemma : ps ∋ minimul ps (λ eq → ¬p (eqo∅ eq)) | 213 lemma : ps ∋ minimul ps (λ eq → ¬p (eqo∅ eq)) |
214 lemma = x∋minimul ps (λ eq → ¬p (eqo∅ eq)) | 214 lemma = x∋minimul ps (λ eq → ¬p (eqo∅ eq)) |
215 | 215 |
216 ∋-p : { n : Level } → ( p : Set (suc n) ) → Dec p | 216 ∋-p : { n : Level } → ( p : Set (suc n) ) → Dec p -- assuming axiom of choice |
217 ∋-p {n} p with p∨¬p p | 217 ∋-p {n} p with p∨¬p p |
218 ∋-p {n} p | case1 x = yes x | 218 ∋-p {n} p | case1 x = yes x |
219 ∋-p {n} p | case2 x = no x | 219 ∋-p {n} p | case2 x = no x |
220 | 220 |
221 double-neg-eilm : {n : Level } {A : Set (suc n)} → ¬ ¬ A → A -- we don't have this in intutionistic logic | 221 double-neg-eilm : {n : Level } {A : Set (suc n)} → ¬ ¬ A → A -- we don't have this in intutionistic logic |
222 double-neg-eilm {n} {A} notnot with ∋-p A | 222 double-neg-eilm {n} {A} notnot with ∋-p A -- assuming axiom of choice |
223 ... | yes p = p | 223 ... | yes p = p |
224 ... | no ¬p = ⊥-elim ( notnot ¬p ) | 224 ... | no ¬p = ⊥-elim ( notnot ¬p ) |
225 | 225 |
226 OrdP : {n : Level} → ( x : Ordinal {suc n} ) ( y : OD {suc n} ) → Dec ( Ord x ∋ y ) | 226 OrdP : {n : Level} → ( x : Ordinal {suc n} ) ( y : OD {suc n} ) → Dec ( Ord x ∋ y ) |
227 OrdP {n} x y with trio< x (od→ord y) | 227 OrdP {n} x y with trio< x (od→ord y) |
240 ZFSubset : {n : Level} → (A x : OD {suc n} ) → OD {suc n} | 240 ZFSubset : {n : Level} → (A x : OD {suc n} ) → OD {suc n} |
241 ZFSubset A x = record { def = λ y → def A y ∧ def x y } where | 241 ZFSubset A x = record { def = λ y → def A y ∧ def x y } where |
242 | 242 |
243 Def : {n : Level} → (A : OD {suc n}) → OD {suc n} | 243 Def : {n : Level} → (A : OD {suc n}) → OD {suc n} |
244 Def {n} A = Ord ( sup-o ( λ x → od→ord ( ZFSubset A (ord→od x )) ) ) -- Ord x does not help ord-power→ | 244 Def {n} A = Ord ( sup-o ( λ x → od→ord ( ZFSubset A (ord→od x )) ) ) -- Ord x does not help ord-power→ |
245 | |
246 | |
247 _⊆_ : {n : Level} ( A B : OD {suc n} ) → ∀{ x : OD {suc n} } → Set (suc n) | |
248 _⊆_ A B {x} = A ∋ x → B ∋ x | |
249 | |
250 infixr 220 _⊆_ | |
251 | |
252 subset-lemma : {n : Level} → {A x y : OD {suc n} } → ( x ∋ y → ZFSubset A x ∋ y ) ⇔ ( _⊆_ x A {y} ) | |
253 subset-lemma {n} {A} {x} {y} = record { | |
254 proj1 = λ z lt → proj1 (z lt) | |
255 ; proj2 = λ x⊆A lt → record { proj1 = x⊆A lt ; proj2 = lt } | |
256 } | |
257 | |
258 Def=A→Set : {n : Level} → (A : Ordinal {suc n}) → Def (Ord A) == record { def = λ x → x o< A → Set n } | |
259 Def=A→Set {n} A = record { | |
260 eq→ = λ {y} DAx y<A → {!!} | |
261 ; eq← = {!!} -- λ {y} f → {!!} | |
262 } where | |
245 | 263 |
246 -- Constructible Set on α | 264 -- Constructible Set on α |
247 -- Def X = record { def = λ y → ∀ (x : OD ) → y < X ∧ y < od→ord x } | 265 -- Def X = record { def = λ y → ∀ (x : OD ) → y < X ∧ y < od→ord x } |
248 -- L (Φ 0) = Φ | 266 -- L (Φ 0) = Φ |
249 -- L (OSuc lv n) = { Def ( L n ) } | 267 -- L (OSuc lv n) = { Def ( L n ) } |
283 A ∩ B = record { def = λ x → def A x ∧ def B x } | 301 A ∩ B = record { def = λ x → def A x ∧ def B x } |
284 Union : OD {suc n} → OD {suc n} | 302 Union : OD {suc n} → OD {suc n} |
285 Union U = record { def = λ x → ¬ (∀ (u : Ordinal ) → ¬ ((def U u) ∧ (def (ord→od u) x))) } | 303 Union U = record { def = λ x → ¬ (∀ (u : Ordinal ) → ¬ ((def U u) ∧ (def (ord→od u) x))) } |
286 _∈_ : ( A B : ZFSet ) → Set (suc n) | 304 _∈_ : ( A B : ZFSet ) → Set (suc n) |
287 A ∈ B = B ∋ A | 305 A ∈ B = B ∋ A |
288 _⊆_ : ( A B : ZFSet ) → ∀{ x : ZFSet } → Set (suc n) | |
289 _⊆_ A B {x} = A ∋ x → B ∋ x | |
290 Power : OD {suc n} → OD {suc n} | 306 Power : OD {suc n} → OD {suc n} |
291 Power A = Replace (Def (Ord (od→ord A))) ( λ x → A ∩ x ) | 307 Power A = Replace (Def (Ord (od→ord A))) ( λ x → A ∩ x ) |
292 {_} : ZFSet → ZFSet | 308 {_} : ZFSet → ZFSet |
293 { x } = ( x , x ) | 309 { x } = ( x , x ) |
294 | 310 |
300 infinite : OD {suc n} | 316 infinite : OD {suc n} |
301 infinite = record { def = λ x → infinite-d x } | 317 infinite = record { def = λ x → infinite-d x } |
302 | 318 |
303 infixr 200 _∈_ | 319 infixr 200 _∈_ |
304 -- infixr 230 _∩_ _∪_ | 320 -- infixr 230 _∩_ _∪_ |
305 infixr 220 _⊆_ | |
306 isZF : IsZF (OD {suc n}) _∋_ _==_ od∅ _,_ Union Power Select Replace infinite | 321 isZF : IsZF (OD {suc n}) _∋_ _==_ od∅ _,_ Union Power Select Replace infinite |
307 isZF = record { | 322 isZF = record { |
308 isEquivalence = record { refl = eq-refl ; sym = eq-sym; trans = eq-trans } | 323 isEquivalence = record { refl = eq-refl ; sym = eq-sym; trans = eq-trans } |
309 ; pair = pair | 324 ; pair = pair |
310 ; union→ = union→ | 325 ; union→ = union→ |
444 lemma2 : def (in-codomain (Def (Ord (od→ord A))) (_∩_ A)) (od→ord t) | 459 lemma2 : def (in-codomain (Def (Ord (od→ord A))) (_∩_ A)) (od→ord t) |
445 lemma2 not = ⊥-elim ( not (od→ord t) (record { proj1 = lemma3 ; proj2 = lemma6 }) ) where | 460 lemma2 not = ⊥-elim ( not (od→ord t) (record { proj1 = lemma3 ; proj2 = lemma6 }) ) where |
446 lemma6 : od→ord t ≡ od→ord (A ∩ ord→od (od→ord t)) | 461 lemma6 : od→ord t ≡ od→ord (A ∩ ord→od (od→ord t)) |
447 lemma6 = cong ( λ k → od→ord k ) (==→o≡ (subst (λ k → t == (A ∩ k)) (sym oiso) ( ∩-≡ t→A ))) | 462 lemma6 = cong ( λ k → od→ord k ) (==→o≡ (subst (λ k → t == (A ∩ k)) (sym oiso) ( ∩-≡ t→A ))) |
448 | 463 |
464 -- assuming axiom of choice | |
449 regularity : (x : OD) (not : ¬ (x == od∅)) → | 465 regularity : (x : OD) (not : ¬ (x == od∅)) → |
450 (x ∋ minimul x not) ∧ (Select (minimul x not) (λ x₁ → (minimul x not ∋ x₁) ∧ (x ∋ x₁)) == od∅) | 466 (x ∋ minimul x not) ∧ (Select (minimul x not) (λ x₁ → (minimul x not ∋ x₁) ∧ (x ∋ x₁)) == od∅) |
451 proj1 (regularity x not ) = x∋minimul x not | 467 proj1 (regularity x not ) = x∋minimul x not |
452 proj2 (regularity x not ) = record { eq→ = lemma1 ; eq← = λ {y} d → lemma2 {y} d } where | 468 proj2 (regularity x not ) = record { eq→ = lemma1 ; eq← = λ {y} d → lemma2 {y} d } where |
453 lemma1 : {x₁ : Ordinal} → def (Select (minimul x not) (λ x₂ → (minimul x not ∋ x₂) ∧ (x ∋ x₂))) x₁ → def od∅ x₁ | 469 lemma1 : {x₁ : Ordinal} → def (Select (minimul x not) (λ x₂ → (minimul x not ∋ x₂) ∧ (x ∋ x₂))) x₁ → def od∅ x₁ |