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