Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison OD.agda @ 189:540b845ea2de
Axiom of choies implies p ∨ ( ¬ p )
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Thu, 25 Jul 2019 14:42:19 +0900 |
parents | 1f2c8b094908 |
children | 6e778b0a7202 |
comparison
equal
deleted
inserted
replaced
188:1f2c8b094908 | 189:540b845ea2de |
---|---|
192 is-o∅ {n} record { lv = (Suc lv₁) ; ord = ord } = no (λ()) | 192 is-o∅ {n} record { lv = (Suc lv₁) ; ord = ord } = no (λ()) |
193 | 193 |
194 ppp : { n : Level } → { p : Set (suc n) } { a : OD {suc n} } → record { def = λ x → p } ∋ a → p | 194 ppp : { n : Level } → { p : Set (suc n) } { a : OD {suc n} } → record { def = λ x → p } ∋ a → p |
195 ppp {n} {p} {a} d = d | 195 ppp {n} {p} {a} d = d |
196 | 196 |
197 p∨¬p : { n : Level } → { p : Set (suc n) } → p ∨ ( ¬ p ) | 197 -- |
198 p∨¬p {n} {p} with record { def = λ x → p } | record { def = λ x → ¬ p } | 198 -- Axiom of choice in intutionistic logic implies the exclude middle |
199 ... | ps | ¬ps with is-o∅ ( od→ord ps) | 199 -- https://plato.stanford.edu/entries/axiom-choice/#AxiChoLog |
200 p∨¬p {n} {p} | ps | ¬ps | yes eq = case2 (¬p eq) where | 200 -- |
201 ¬p : {ps1 : Ordinal {suc n}} → ( ps1 ≡ o∅ {suc n} ) → p → ⊥ | 201 p∨¬p : { n : Level } → ( p : Set (suc n) ) → p ∨ ( ¬ p ) |
202 ¬p refl = {!!} | 202 p∨¬p {n} p with is-o∅ ( od→ord ( record { def = λ x → p } )) |
203 p∨¬p {n} {p} | ps | ¬ps | no ¬p = case1 (ppp {n} {p} {minimul ps (λ eq → ¬p (eqo∅ eq))} ( | 203 p∨¬p {n} p | yes eq = case2 (¬p eq) where |
204 def-subst {suc n} {ps} {_} {record { def = λ x → p }} {od→ord (minimul ps (λ eq → ¬p (eqo∅ eq)))} lemma {!!} refl )) where | 204 ps = record { def = λ x → p } |
205 lemma : ps == od∅ → p → ⊥ | |
206 lemma eq p0 = ¬x<0 {n} {od→ord ps} (eq→ eq p0 ) | |
207 ¬p : (od→ord ps ≡ o∅) → p → ⊥ | |
208 ¬p eq = lemma ( subst₂ (λ j k → j == k ) oiso o∅≡od∅ ( o≡→== eq )) | |
209 p∨¬p {n} p | no ¬p = case1 (ppp {n} {p} {minimul ps (λ eq → ¬p (eqo∅ eq))} lemma) where | |
210 ps = record { def = λ x → p } | |
205 eqo∅ : ps == od∅ {suc n} → od→ord ps ≡ o∅ {suc n} | 211 eqo∅ : ps == od∅ {suc n} → od→ord ps ≡ o∅ {suc n} |
206 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)) |
207 lemma : ps ∋ minimul ps (λ eq → ¬p (eqo∅ eq)) | 213 lemma : ps ∋ minimul ps (λ eq → ¬p (eqo∅ eq)) |
208 lemma = x∋minimul ps (λ eq → ¬p (eqo∅ eq)) | 214 lemma = x∋minimul ps (λ eq → ¬p (eqo∅ eq)) |
215 | |
216 ∋-p : { n : Level } → ( p : Set (suc n) ) → Dec p | |
217 ∋-p {n} p with p∨¬p p | |
218 ∋-p {n} p | case1 x = yes x | |
219 ∋-p {n} p | case2 x = no x | |
220 | |
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 | |
223 ... | yes p = p | |
224 ... | no ¬p = ⊥-elim ( notnot ¬p ) | |
209 | 225 |
210 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 ) |
211 OrdP {n} x y with trio< x (od→ord y) | 227 OrdP {n} x y with trio< x (od→ord y) |
212 OrdP {n} x y | tri< a ¬b ¬c = no ¬c | 228 OrdP {n} x y | tri< a ¬b ¬c = no ¬c |
213 OrdP {n} x y | tri≈ ¬a refl ¬c = no ( o<¬≡ refl ) | 229 OrdP {n} x y | tri≈ ¬a refl ¬c = no ( o<¬≡ refl ) |
384 → (eq : ZFSubset (Ord a) t == t) → od→ord (ZFSubset (Ord a) (ord→od (od→ord t))) ≡ od→ord t | 400 → (eq : ZFSubset (Ord a) t == t) → od→ord (ZFSubset (Ord a) (ord→od (od→ord t))) ≡ od→ord t |
385 lemma1 {n} {a} {t} eq = subst (λ k → od→ord (ZFSubset (Ord a) k) ≡ od→ord t ) (sym oiso) (cong (λ k → od→ord k ) (==→o≡ eq )) | 401 lemma1 {n} {a} {t} eq = subst (λ k → od→ord (ZFSubset (Ord a) k) ≡ od→ord t ) (sym oiso) (cong (λ k → od→ord k ) (==→o≡ eq )) |
386 lemma : od→ord (ZFSubset (Ord a) (ord→od (od→ord t)) ) o< sup-o (λ x → od→ord (ZFSubset (Ord a) (ord→od x))) | 402 lemma : od→ord (ZFSubset (Ord a) (ord→od (od→ord t)) ) o< sup-o (λ x → od→ord (ZFSubset (Ord a) (ord→od x))) |
387 lemma = sup-o< | 403 lemma = sup-o< |
388 | 404 |
389 -- double-neg-eilm : {n : Level } {A : Set n} → ¬ ¬ A → A -- we don't have this in intutionistic logic | |
390 -- | 405 -- |
391 -- Every set in OD is a subset of Ordinals | 406 -- Every set in OD is a subset of Ordinals |
392 -- | 407 -- |
393 -- Power A = Replace (Def (Ord (od→ord A))) ( λ y → A ∩ y ) | 408 -- Power A = Replace (Def (Ord (od→ord A))) ( λ y → A ∩ y ) |
394 | 409 |
472 choice-func : (X : OD {suc n} ) → {x : OD } → ¬ ( x == od∅ ) → ( X ∋ x ) → OD | 487 choice-func : (X : OD {suc n} ) → {x : OD } → ¬ ( x == od∅ ) → ( X ∋ x ) → OD |
473 choice-func X {x} not X∋x = minimul x not | 488 choice-func X {x} not X∋x = minimul x not |
474 choice : (X : OD {suc n} ) → {A : OD } → ( X∋A : X ∋ A ) → (not : ¬ ( A == od∅ )) → A ∋ choice-func X not X∋A | 489 choice : (X : OD {suc n} ) → {A : OD } → ( X∋A : X ∋ A ) → (not : ¬ ( A == od∅ )) → A ∋ choice-func X not X∋A |
475 choice X {A} X∋A not = x∋minimul A not | 490 choice X {A} X∋A not = x∋minimul A not |
476 | 491 |
477 -- choice-func' : (X : OD {suc n} ) → (∋-p : (A x : OD {suc n} ) → Dec ( A ∋ x ) ) → {x : OD } → ¬ ( x == od∅ ) → ( X ∋ x ) → OD {suc n} | 492 -- choice-func' : (X : OD {suc n} ) → (∋-p : (A x : OD {suc n} ) → Dec ( A ∋ x ) ) → ¬ ( X == od∅ ) → OD {suc n} |
478 | 493 -- |
479 -- another form of regularity | 494 -- another form of regularity |
480 -- | 495 -- |
481 ε-induction : {n m : Level} { ψ : OD {suc n} → Set m} | 496 ε-induction : {n m : Level} { ψ : OD {suc n} → Set m} |
482 → ( {x : OD {suc n} } → ({ y : OD {suc n} } → x ∋ y → ψ y ) → ψ x ) | 497 → ( {x : OD {suc n} } → ({ y : OD {suc n} } → x ∋ y → ψ y ) → ψ x ) |
483 → (x : OD {suc n} ) → ψ x | 498 → (x : OD {suc n} ) → ψ x |