Mercurial > hg > Members > kono > Proof > ZF-in-agda
annotate src/ODC.agda @ 1120:e086a266c6b7
FIP fix
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 03 Jan 2023 09:28:23 +0900 |
| parents | 55ab5de1ae02 |
| children | 45cd80181a29 |
| rev | line source |
|---|---|
| 431 | 1 {-# OPTIONS --allow-unsolved-metas #-} |
| 2 open import Level | |
| 3 open import Ordinals | |
| 4 module ODC {n : Level } (O : Ordinals {n} ) where | |
| 5 | |
| 6 open import zf | |
| 1120 | 7 open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ; _⊔_ to _n⊔_ ) |
| 431 | 8 open import Relation.Binary.PropositionalEquality |
| 1120 | 9 open import Data.Nat.Properties |
| 431 | 10 open import Data.Empty |
| 11 open import Relation.Nullary | |
| 12 open import Relation.Binary | |
| 13 open import Relation.Binary.Core | |
| 14 | |
| 15 import OrdUtil | |
| 16 open import logic | |
| 17 open import nat | |
| 18 import OD | |
| 19 import ODUtil | |
| 20 | |
| 21 open inOrdinal O | |
| 22 open OD O | |
| 23 open OD.OD | |
| 24 open OD._==_ | |
| 25 open ODAxiom odAxiom | |
| 26 open ODUtil O | |
| 27 | |
| 28 open Ordinals.Ordinals O | |
| 29 open Ordinals.IsOrdinals isOrdinal | |
| 30 open Ordinals.IsNext isNext | |
| 31 open OrdUtil O | |
| 32 | |
| 33 | |
| 34 open HOD | |
| 35 | |
| 36 open _∧_ | |
| 37 | |
| 1120 | 38 postulate |
| 431 | 39 -- mimimul and x∋minimal is an Axiom of choice |
| 1120 | 40 minimal : (x : HOD ) → ¬ (x =h= od∅ )→ HOD |
| 431 | 41 -- this should be ¬ (x =h= od∅ )→ ∃ ox → x ∋ Ord ox ( minimum of x ) |
| 42 x∋minimal : (x : HOD ) → ( ne : ¬ (x =h= od∅ ) ) → odef x ( & ( minimal x ne ) ) | |
| 467 | 43 -- minimality (proved by ε-induction with LEM) |
| 431 | 44 minimal-1 : (x : HOD ) → ( ne : ¬ (x =h= od∅ ) ) → (y : HOD ) → ¬ ( odef (minimal x ne) (& y)) ∧ (odef x (& y) ) |
| 45 | |
| 46 | |
| 47 -- | |
| 48 -- Axiom of choice in intutionistic logic implies the exclude middle | |
| 49 -- https://plato.stanford.edu/entries/axiom-choice/#AxiChoLog | |
| 50 -- | |
| 51 | |
| 52 pred-od : ( p : Set n ) → HOD | |
| 53 pred-od p = record { od = record { def = λ x → (x ≡ o∅) ∧ p } ; | |
| 1120 | 54 odmax = osuc o∅; <odmax = λ x → subst (λ k → k o< osuc o∅) (sym (proj1 x)) <-osuc } |
| 431 | 55 |
| 56 ppp : { p : Set n } { a : HOD } → pred-od p ∋ a → p | |
| 57 ppp {p} {a} d = proj2 d | |
| 58 | |
| 59 p∨¬p : ( p : Set n ) → p ∨ ( ¬ p ) -- assuming axiom of choice | |
| 60 p∨¬p p with is-o∅ ( & (pred-od p )) | |
| 61 p∨¬p p | yes eq = case2 (¬p eq) where | |
| 1120 | 62 ps = pred-od p |
| 63 eqo∅ : ps =h= od∅ → & ps ≡ o∅ | |
| 64 eqo∅ eq = subst (λ k → & ps ≡ k) ord-od∅ ( cong (λ k → & k ) (==→o≡ eq)) | |
| 431 | 65 lemma : ps =h= od∅ → p → ⊥ |
| 66 lemma eq p0 = ¬x<0 {& ps} (eq→ eq record { proj1 = eqo∅ eq ; proj2 = p0 } ) | |
| 67 ¬p : (& ps ≡ o∅) → p → ⊥ | |
| 68 ¬p eq = lemma ( subst₂ (λ j k → j =h= k ) *iso o∅≡od∅ ( o≡→== eq )) | |
| 69 p∨¬p p | no ¬p = case1 (ppp {p} {minimal ps (λ eq → ¬p (eqo∅ eq))} lemma) where | |
| 1120 | 70 ps = pred-od p |
| 71 eqo∅ : ps =h= od∅ → & ps ≡ o∅ | |
| 72 eqo∅ eq = subst (λ k → & ps ≡ k) ord-od∅ ( cong (λ k → & k ) (==→o≡ eq)) | |
| 73 lemma : ps ∋ minimal ps (λ eq → ¬p (eqo∅ eq)) | |
| 431 | 74 lemma = x∋minimal ps (λ eq → ¬p (eqo∅ eq)) |
| 75 | |
| 1120 | 76 decp : ( p : Set n ) → Dec p -- assuming axiom of choice |
| 431 | 77 decp p with p∨¬p p |
| 78 decp p | case1 x = yes x | |
| 79 decp p | case2 x = no x | |
| 80 | |
| 1120 | 81 ∋-p : (A x : HOD ) → Dec ( A ∋ x ) |
| 431 | 82 ∋-p A x with p∨¬p ( A ∋ x ) -- LEM |
| 83 ∋-p A x | case1 t = yes t | |
| 84 ∋-p A x | case2 t = no (λ x → t x) | |
| 85 | |
| 1120 | 86 double-neg-elim : {A : Set n} → ¬ ¬ A → A -- we don't have this in intutionistic logic |
| 87 double-neg-elim {A} notnot with decp A -- assuming axiom of choice | |
| 431 | 88 ... | yes p = p |
| 89 ... | no ¬p = ⊥-elim ( notnot ¬p ) | |
| 90 | |
|
860
105f8d6c51fb
no-extension on immidate ordinal passed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
477
diff
changeset
|
91 or-exclude : {A B : Set n} → A ∨ B → A ∨ ( (¬ A) ∧ B ) |
|
105f8d6c51fb
no-extension on immidate ordinal passed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
477
diff
changeset
|
92 or-exclude {A} {B} ab with p∨¬p A |
|
105f8d6c51fb
no-extension on immidate ordinal passed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
477
diff
changeset
|
93 or-exclude {A} {B} (case1 a) | case1 a0 = case1 a |
|
105f8d6c51fb
no-extension on immidate ordinal passed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
477
diff
changeset
|
94 or-exclude {A} {B} (case1 a) | case2 ¬a = ⊥-elim ( ¬a a ) |
|
105f8d6c51fb
no-extension on immidate ordinal passed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
477
diff
changeset
|
95 or-exclude {A} {B} (case2 b) | case1 a = case1 a |
|
105f8d6c51fb
no-extension on immidate ordinal passed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
477
diff
changeset
|
96 or-exclude {A} {B} (case2 b) | case2 ¬a = case2 ⟪ ¬a , b ⟫ |
|
105f8d6c51fb
no-extension on immidate ordinal passed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
477
diff
changeset
|
97 |
| 1120 | 98 -- record By-contradiction (A : Set n) (B : A → Set n) : Set (suc n) where |
| 99 -- field | |
| 100 -- a : A | |
| 101 -- b : B a | |
| 102 -- | |
| 103 -- by-contradiction : {A : Set n} {B : A → Set n} → ¬ ( (a : A ) → ¬ B a ) → By-contradiction A B | |
| 104 -- by-contradiction {A} {B} not with p∨¬p A | |
| 105 -- ... | case2 ¬a = ⊥-elim (not (λ a → ⊥-elim (¬a a ))) | |
| 106 -- ... | case1 a with p∨¬p (B a) | |
| 107 -- ... | case1 b = record { a = a ; b = b } | |
| 108 -- ... | case2 ¬b = ⊥-elim ( not ( λ a b → ⊥-elim ( ¬b ? ))) | |
| 109 -- | |
| 431 | 110 power→⊆ : ( A t : HOD) → Power A ∋ t → t ⊆ A |
| 1096 | 111 power→⊆ A t PA∋t tx = subst (λ k → odef A k ) &iso ( power→ A t PA∋t (subst (λ k → odef t k) (sym &iso) tx ) ) |
| 431 | 112 |
| 447 | 113 power-∩ : { A x y : HOD } → Power A ∋ x → Power A ∋ y → Power A ∋ ( x ∩ y ) |
| 114 power-∩ {A} {x} {y} ax ay = power← A (x ∩ y) p01 where | |
| 115 p01 : {z : HOD} → (x ∩ y) ∋ z → A ∋ z | |
| 1096 | 116 p01 {z} xyz = power→ A x ax (proj1 xyz ) |
| 447 | 117 |
| 431 | 118 OrdP : ( x : Ordinal ) ( y : HOD ) → Dec ( Ord x ∋ y ) |
| 119 OrdP x y with trio< x (& y) | |
| 120 OrdP x y | tri< a ¬b ¬c = no ¬c | |
| 121 OrdP x y | tri≈ ¬a refl ¬c = no ( o<¬≡ refl ) | |
| 122 OrdP x y | tri> ¬a ¬b c = yes c | |
| 123 | |
| 124 open import zfc | |
| 125 | |
| 126 HOD→ZFC : ZFC | |
| 1120 | 127 HOD→ZFC = record { |
| 128 ZFSet = HOD | |
| 129 ; _∋_ = _∋_ | |
| 130 ; _≈_ = _=h=_ | |
| 431 | 131 ; ∅ = od∅ |
| 132 ; Select = Select | |
| 133 ; isZFC = isZFC | |
| 134 } where | |
| 135 -- infixr 200 _∈_ | |
| 136 -- infixr 230 _∩_ _∪_ | |
| 137 isZFC : IsZFC (HOD ) _∋_ _=h=_ od∅ Select | |
| 138 isZFC = record { | |
| 139 choice-func = choice-func ; | |
| 140 choice = choice | |
| 141 } where | |
| 142 -- Axiom of choice ( is equivalent to the existence of minimal in our case ) | |
| 1120 | 143 -- ∀ X [ ∅ ∉ X → (∃ f : X → ⋃ X ) → ∀ A ∈ X ( f ( A ) ∈ A ) ] |
| 431 | 144 choice-func : (X : HOD ) → {x : HOD } → ¬ ( x =h= od∅ ) → ( X ∋ x ) → HOD |
| 145 choice-func X {x} not X∋x = minimal x not | |
| 1120 | 146 choice : (X : HOD ) → {A : HOD } → ( X∋A : X ∋ A ) → (not : ¬ ( A =h= od∅ )) → A ∋ choice-func X not X∋A |
| 431 | 147 choice X {A} X∋A not = x∋minimal A not |
| 148 |