# HG changeset patch # User Shinji KONO # Date 1563328351 -32400 # Node ID ea0e7927637a46e0235a600cde958080fba979e3 # Parent d16b8bf29f4f5a16ed177831e065d3408cf986cc use double negation diff -r d16b8bf29f4f -r ea0e7927637a HOD.agda --- a/HOD.agda Tue Jul 16 09:57:01 2019 +0900 +++ b/HOD.agda Wed Jul 17 10:52:31 2019 +0900 @@ -57,8 +57,8 @@ -- OD can be iso to a subset of Ordinal ( by means of Godel Set ) od→ord : {n : Level} → OD {n} → Ordinal {n} ord→od : {n : Level} → Ordinal {n} → OD {n} - c<→o< : {n : Level} {x y : OD {n} } → def y ( od→ord x ) → od→ord x o< od→ord y - oiso : {n : Level} {x : OD {n}} → ord→od ( od→ord x ) ≡ x + c<→o< : {n : Level} {x y : OD {n} } → def y ( od→ord x ) → od→ord x o< od→ord y + oiso : {n : Level} {x : OD {n}} → ord→od ( od→ord x ) ≡ x diso : {n : Level} {x : Ordinal {n}} → od→ord ( ord→od x ) ≡ x -- we should prove this in agda, but simply put here ==→o≡ : {n : Level} → { x y : OD {suc n} } → (x == y) → x ≡ y @@ -319,10 +319,9 @@ union→ X z u xx not = ⊥-elim ( not (od→ord u) ( record { proj1 = proj1 xx ; proj2 = subst ( λ k → def k (od→ord z)) (sym oiso) (proj2 xx) } )) union← : (X z : OD) (X∋z : Union X ∋ z) → ¬ ( (u : OD ) → ¬ ((X ∋ u) ∧ (u ∋ z ))) - union← X z UX∋z = TransFiniteExists' _ lemma UX∋z where + union← X z UX∋z = TransFiniteExists _ lemma UX∋z where lemma : {y : Ordinal} → def X y ∧ def (ord→od y) (od→ord z) → ¬ ((u : OD) → ¬ (X ∋ u) ∧ (u ∋ z)) lemma {y} xx not = not (ord→od y) record { proj1 = subst ( λ k → def X k ) (sym diso) (proj1 xx ) ; proj2 = proj2 xx } - -- ( λ {y} xx → ψiso : {ψ : OD {suc n} → Set (suc n)} {x y : OD {suc n}} → ψ x → x ≡ y → ψ y ψiso {ψ} t refl = t @@ -377,22 +376,27 @@ lemma : od→ord (ZFSubset (Ord a) (ord→od (od→ord t)) ) o< sup-o (λ x → od→ord (ZFSubset (Ord a) (ord→od x))) lemma = sup-o< + -- double-neg-eilm : {n : Level } {A : Set n} → ¬ ¬ A → A + -- double-neg-eilm {n} {A} notnot = ⊥-elim (notnot (λ A → {!!} )) -- -- Every set in OD is a subset of Ordinals -- -- Power A = Replace (Def (Ord (od→ord A))) ( λ y → A ∩ y ) - power→ : ( A t : OD) → Power A ∋ t → {x : OD} → t ∋ x → A ∋ x - power→ A t P∋t {x} t∋x = TransFiniteExists _ -- (λ y → (t == (A ∩ ord→od y))) - lemma4 lemma5 where + + -- we have oly double negation form because of the replacement axiom + -- + power→ : ( A t : OD) → Power A ∋ t → {x : OD} → t ∋ x → ¬ ¬ (A ∋ x) + power→ A t P∋t {x} t∋x = TransFiniteExists _ lemma5 lemma4 where a = od→ord A lemma2 : ¬ ( (y : OD) → ¬ (t == (A ∩ y))) lemma2 = replacement→ (Def (Ord (od→ord A))) t P∋t - lemma3 : (y : OD) → t == ( A ∩ y ) → A ∋ x - lemma3 y eq = proj1 (eq→ eq t∋x) + lemma3 : (y : OD) → t == ( A ∩ y ) → ¬ ¬ (A ∋ x) + lemma3 y eq not = not (proj1 (eq→ eq t∋x)) lemma4 : ¬ ((y : Ordinal) → ¬ (t == (A ∩ ord→od y))) lemma4 not = lemma2 ( λ y not1 → not (od→ord y) (subst (λ k → t == ( A ∩ k )) (sym oiso) not1 )) - lemma5 : {y : Ordinal} → t == (A ∩ ord→od y) → def A (od→ord x) - lemma5 {y} eq = lemma3 (ord→od y) eq + lemma5 : {y : Ordinal} → t == (A ∩ ord→od y) → ¬ ¬ (def A (od→ord x)) + lemma5 {y} eq not = (lemma3 (ord→od y) eq) not + power← : (A t : OD) → ({x : OD} → (t ∋ x → A ∋ x)) → Power A ∋ t power← A t t→A = record { proj1 = lemma1 ; proj2 = lemma2 } where a = od→ord A diff -r d16b8bf29f4f -r ea0e7927637a ordinal-definable.agda --- a/ordinal-definable.agda Tue Jul 16 09:57:01 2019 +0900 +++ b/ordinal-definable.agda Wed Jul 17 10:52:31 2019 +0900 @@ -368,8 +368,8 @@ -- then ZFSubset A ≡ t or ZFSubset A ∋ t. In the former case ZFSubset A ∋ x implies A ∋ x -- In case of later, ZFSubset A ∋ t and t ∋ x implies ZFSubset A ∋ x by transitivity -- - power→ : (A t : OD) → Power A ∋ t → {x : OD} → t ∋ x → A ∋ x - power→ A t P∋t {x} t∋x = proj1 lemma-s where + power→ : (A t : OD) → Power A ∋ t → {x : OD} → t ∋ x → ¬ ¬ (A ∋ x) + power→ A t P∋t {x} t∋x = double-neg (proj1 lemma-s) where minsup : OD minsup = ZFSubset A ( ord→od ( sup-x (λ x → od→ord ( ZFSubset A (ord→od x))))) lemma-t : csuc minsup ∋ t diff -r d16b8bf29f4f -r ea0e7927637a ordinal.agda --- a/ordinal.agda Tue Jul 16 09:57:01 2019 +0900 +++ b/ordinal.agda Wed Jul 17 10:52:31 2019 +0900 @@ -321,21 +321,20 @@ TransFinite caseΦ caseOSuc record { lv = lx ; ord = (OSuc lx ox) } = caseOSuc lx ox (TransFinite caseΦ caseOSuc record { lv = lx ; ord = ox }) +-- we cannot prove this in intutonistic logic -- (¬ (∀ y → ¬ ( ψ y ))) → (ψ y → p ) → p --- may be we can prove this... -postulate - TransFiniteExists : {n m l : Level} → ( ψ : Ordinal {n} → Set m ) - → (exists : ¬ (∀ y → ¬ ( ψ y ) )) - → {p : Set l} ( P : { y : Ordinal {n} } → ψ y → p ) - → p - --- TransFiniteExists {n} {ψ} exists {p} P = ⊥-elim ( exists lemma ) where --- lemma : (y : Ordinal {n} ) → ¬ ψ y --- lemma y ψy = ( TransFinite {n} {{!!}} {!!} {!!} y ) ψy -TransFiniteExists' : {n m l : Level} → ( ψ : Ordinal {n} → Set m ) +-- postulate +-- TransFiniteExists : {n m l : Level} → ( ψ : Ordinal {n} → Set m ) +-- → (exists : ¬ (∀ y → ¬ ( ψ y ) )) +-- → {p : Set l} ( P : { y : Ordinal {n} } → ψ y → p ) +-- → p +-- +-- Instead we prove +-- +TransFiniteExists : {n m l : Level} → ( ψ : Ordinal {n} → Set m ) → {p : Set l} ( P : { y : Ordinal {n} } → ψ y → ¬ p ) → (exists : ¬ (∀ y → ¬ ( ψ y ) )) → ¬ p -TransFiniteExists' {n} {m} {l} ψ {p} P = contra-position ( λ p y ψy → P {y} ψy p ) +TransFiniteExists {n} {m} {l} ψ {p} P = contra-position ( λ p y ψy → P {y} ψy p ) diff -r d16b8bf29f4f -r ea0e7927637a zf.agda --- a/zf.agda Tue Jul 16 09:57:01 2019 +0900 +++ b/zf.agda Wed Jul 17 10:52:31 2019 +0900 @@ -25,6 +25,9 @@ contra-position : {n m : Level } {A : Set n} {B : Set m} → (A → B) → ¬ B → ¬ A contra-position {n} {m} {A} {B} f ¬b a = ¬b ( f a ) +double-neg : {n : Level } {A : Set n} → A → ¬ ¬ A +double-neg A notnot = notnot A + infixr 130 _∧_ infixr 140 _∨_ infixr 150 _⇔_ @@ -64,7 +67,7 @@ field empty : ∀( x : ZFSet ) → ¬ ( ∅ ∋ x ) -- power : ∀ X ∃ A ∀ t ( t ∈ A ↔ t ⊆ X ) ) - power→ : ∀( A t : ZFSet ) → Power A ∋ t → ∀ {x} → _⊆_ t A {x} + power→ : ∀( A t : ZFSet ) → Power A ∋ t → ∀ {x} → t ∋ x → ¬ ¬ ( A ∋ x ) -- _⊆_ t A {x} power← : ∀( A t : ZFSet ) → ( ∀ {x} → _⊆_ t A {x}) → Power A ∋ t -- extensionality : ∀ z ( z ∈ x ⇔ z ∈ y ) ⇒ ∀ w ( x ∈ w ⇔ y ∈ w ) extensionality : { A B : ZFSet } → ( (z : ZFSet) → ( A ∋ z ) ⇔ (B ∋ z) ) → A ≈ B