Mercurial > hg > Members > kono > Proof > ZF-in-agda
diff ordinal.agda @ 211:6bb5d57c9561 release
Axiom of choice from exclude middle
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Thu, 01 Aug 2019 12:24:26 +0900 |
parents | d4802eb159ff |
children | 22d435172d1a |
line wrap: on
line diff
--- a/ordinal.agda Sat Jul 20 08:04:20 2019 +0900 +++ b/ordinal.agda Thu Aug 01 12:24:26 2019 +0900 @@ -13,13 +13,11 @@ OSuc : (lv : Nat) → OrdinalD {n} lv → OrdinalD lv record Ordinal {n : Level} : Set n where + constructor ordinal field lv : Nat ord : OrdinalD {n} lv --- --- Φ (Suc lv) < ℵ lv < OSuc (Suc lv) (ℵ lv) < OSuc ... < OSuc (Suc lv) (Φ (Suc lv)) < OSuc ... < ℵ (Suc lv) --- data _d<_ {n : Level} : {lx ly : Nat} → OrdinalD {n} lx → OrdinalD {n} ly → Set n where Φ< : {lx : Nat} → {x : OrdinalD {n} lx} → Φ lx d< OSuc lx x s< : {lx : Nat} → {x y : OrdinalD {n} lx} → x d< y → OSuc lx x d< OSuc lx y @@ -114,10 +112,22 @@ ¬a≤a : {la : Nat} → Suc la ≤ la → ⊥ ¬a≤a (s≤s lt) = ¬a≤a lt +a<sa : {la : Nat} → la < Suc la +a<sa {Zero} = s≤s z≤n +a<sa {Suc la} = s≤s a<sa + =→¬< : {x : Nat } → ¬ ( x < x ) =→¬< {Zero} () =→¬< {Suc x} (s≤s lt) = =→¬< lt +<-∨ : { x y : Nat } → x < Suc y → ( (x ≡ y ) ∨ (x < y) ) +<-∨ {Zero} {Zero} (s≤s z≤n) = case1 refl +<-∨ {Zero} {Suc y} (s≤s lt) = case2 (s≤s z≤n) +<-∨ {Suc x} {Zero} (s≤s ()) +<-∨ {Suc x} {Suc y} (s≤s lt) with <-∨ {x} {y} lt +<-∨ {Suc x} {Suc y} (s≤s lt) | case1 eq = case1 (cong (λ k → Suc k ) eq) +<-∨ {Suc x} {Suc y} (s≤s lt) | case2 lt1 = case2 (s≤s lt1) + case12-⊥ : {n : Level} {x y : Ordinal {suc n}} → lv x < lv y → ord x d< ord y → ⊥ case12-⊥ {x} {y} lt1 lt2 with d<→lv lt2 ... | refl = nat-≡< refl lt1 @@ -126,7 +136,7 @@ case21-⊥ {x} {y} lt1 lt2 with d<→lv lt2 ... | refl = nat-≡< refl lt1 -o<¬≡ : {n : Level } { ox oy : Ordinal {n}} → ox ≡ oy → ox o< oy → ⊥ +o<¬≡ : {n : Level } { ox oy : Ordinal {suc n}} → ox ≡ oy → ox o< oy → ⊥ o<¬≡ {_} {ox} {ox} refl (case1 lt) = =→¬< lt o<¬≡ {_} {ox} {ox} refl (case2 (s< lt)) = trio<≡ refl lt @@ -224,6 +234,12 @@ lemma1 (case1 x) = ¬a x lemma1 (case2 x) = ≡→¬d< x +xo<ab : {n : Level} {oa ob : Ordinal {suc n}} → ( {ox : Ordinal {suc n}} → ox o< oa → ox o< ob ) → oa o< osuc ob +xo<ab {n} {oa} {ob} a→b with trio< oa ob +xo<ab {n} {oa} {ob} a→b | tri< a ¬b ¬c = ordtrans a <-osuc +xo<ab {n} {oa} {ob} a→b | tri≈ ¬a refl ¬c = <-osuc +xo<ab {n} {oa} {ob} a→b | tri> ¬a ¬b c = ⊥-elim ( o<¬≡ refl (a→b c ) ) + maxα : {n : Level} → Ordinal {suc n} → Ordinal → Ordinal maxα x y with trio< x y maxα x y | tri< a ¬b ¬c = y @@ -294,8 +310,6 @@ proj2 (osuc2 {n} x y) (case2 lt) with d<→lv lt ... | refl = case2 (s< lt) --- omax≡ (omax x x ) (osuc x) (omxx x) - OrdTrans : {n : Level} → Transitive {suc n} _o≤_ OrdTrans (case1 refl) (case1 refl) = case1 refl OrdTrans (case1 refl) (case2 lt2) = case2 lt2 @@ -313,15 +327,31 @@ } } -TransFinite : {n m : Level} → { ψ : Ordinal {n} → Set m } - → ( ∀ (lx : Nat ) → ψ ( record { lv = lx ; ord = Φ lx } ) ) +TransFinite : {n m : Level} → { ψ : Ordinal {suc n} → Set m } + → ( ∀ (lx : Nat ) → ( (x : Ordinal {suc n} ) → x o< ordinal lx (Φ lx) → ψ x ) → ψ ( record { lv = lx ; ord = Φ lx } ) ) → ( ∀ (lx : Nat ) → (x : OrdinalD lx ) → ψ ( record { lv = lx ; ord = x } ) → ψ ( record { lv = lx ; ord = OSuc lx x } ) ) → ∀ (x : Ordinal) → ψ x -TransFinite caseΦ caseOSuc record { lv = lv ; ord = (Φ (lv)) } = caseΦ lv -TransFinite caseΦ caseOSuc record { lv = lx ; ord = (OSuc lx ox) } = - caseOSuc lx ox (TransFinite caseΦ caseOSuc record { lv = lx ; ord = ox }) +TransFinite {n} {m} {ψ} caseΦ caseOSuc x = proj1 (TransFinite1 (lv x) (ord x) ) where + TransFinite1 : (lx : Nat) (ox : OrdinalD lx ) → ψ (ordinal lx ox) ∧ ( ( (x : Ordinal {suc n} ) → x o< ordinal lx (Φ lx) → ψ x ) ) + TransFinite1 Zero (Φ 0) = record { proj1 = caseΦ Zero lemma ; proj2 = lemma1 } where + lemma : (x : Ordinal) → x o< ordinal Zero (Φ Zero) → ψ x + lemma x (case1 ()) + lemma x (case2 ()) + lemma1 : (x : Ordinal) → x o< ordinal Zero (Φ Zero) → ψ x + lemma1 x (case1 ()) + lemma1 x (case2 ()) + TransFinite1 (Suc lx) (Φ (Suc lx)) = record { proj1 = caseΦ (Suc lx) (λ x → lemma (lv x) (ord x)) ; proj2 = (λ x → lemma (lv x) (ord x)) } where + lemma0 : (ly : Nat) (oy : OrdinalD ly ) → ordinal ly oy o< ordinal lx (Φ lx) → ψ (ordinal ly oy) + lemma0 ly oy lt = proj2 ( TransFinite1 lx (Φ lx) ) (ordinal ly oy) lt + lemma : (ly : Nat) (oy : OrdinalD ly ) → ordinal ly oy o< ordinal (Suc lx) (Φ (Suc lx)) → ψ (ordinal ly oy) + lemma lx1 ox1 (case1 lt) with <-∨ lt + lemma lx (Φ lx) (case1 lt) | case1 refl = proj1 ( TransFinite1 lx (Φ lx) ) + lemma lx (OSuc lx ox1) (case1 lt) | case1 refl = caseOSuc lx ox1 ( lemma lx ox1 (case1 a<sa)) + lemma lx (Φ lx) (case1 lt) | case2 (s≤s lt1) = lemma0 lx (Φ lx) (case1 (s≤s lt1)) + lemma lx1 (OSuc lx1 ox1) (case1 lt) | case2 lt1 = caseOSuc lx1 ox1 ( lemma lx1 ox1 (case1 (<-trans lt1 a<sa ))) + TransFinite1 lx (OSuc lx ox) = record { proj1 = caseOSuc lx ox (proj1 (TransFinite1 lx ox )) ; proj2 = proj2 (TransFinite1 lx ox )} --- we cannot prove this in intutonistic logic +-- we cannot prove this in intutionistic logic -- (¬ (∀ y → ¬ ( ψ y ))) → (ψ y → p ) → p -- postulate -- TransFiniteExists : {n m l : Level} → ( ψ : Ordinal {n} → Set m ) @@ -337,4 +367,3 @@ → ¬ p TransFiniteExists {n} {m} {l} ψ {p} P = contra-position ( λ p y ψy → P {y} ψy p ) -