Mercurial > hg > Members > kono > Proof > ZF-in-agda
annotate ODC.agda @ 387:8b0715e28b33
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 25 Jul 2020 09:09:00 +0900 |
| parents | 6c72bee25653 |
| children | 8c092c042093 |
| rev | line source |
|---|---|
|
369
17adeeee0c2a
fix Select and Replace
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
365
diff
changeset
|
1 {-# OPTIONS --allow-unsolved-metas #-} |
| 16 | 2 open import Level |
|
223
2e1f19c949dc
sepration of ordinal from OD
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
219
diff
changeset
|
3 open import Ordinals |
| 276 | 4 module ODC {n : Level } (O : Ordinals {n} ) where |
| 3 | 5 |
|
14
e11e95d5ddee
separete constructible set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
11
diff
changeset
|
6 open import zf |
| 23 | 7 open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ; _⊔_ to _n⊔_ ) |
|
14
e11e95d5ddee
separete constructible set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
11
diff
changeset
|
8 open import Relation.Binary.PropositionalEquality |
|
e11e95d5ddee
separete constructible set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
11
diff
changeset
|
9 open import Data.Nat.Properties |
| 6 | 10 open import Data.Empty |
| 11 open import Relation.Nullary | |
| 12 open import Relation.Binary | |
| 13 open import Relation.Binary.Core | |
| 14 | |
|
213
22d435172d1a
separate logic and nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
210
diff
changeset
|
15 open import logic |
|
22d435172d1a
separate logic and nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
210
diff
changeset
|
16 open import nat |
| 276 | 17 import OD |
|
213
22d435172d1a
separate logic and nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
210
diff
changeset
|
18 |
|
223
2e1f19c949dc
sepration of ordinal from OD
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
219
diff
changeset
|
19 open inOrdinal O |
| 276 | 20 open OD O |
| 21 open OD.OD | |
| 22 open OD._==_ | |
|
277
d9d3654baee1
seperate choice from LEM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
276
diff
changeset
|
23 open ODAxiom odAxiom |
| 258 | 24 |
| 329 | 25 open HOD |
| 26 | |
| 331 | 27 open _∧_ |
| 28 | |
|
29
fce60b99dc55
posturate OD is isomorphic to Ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
29 postulate |
| 258 | 30 -- mimimul and x∋minimal is an Axiom of choice |
| 329 | 31 minimal : (x : HOD ) → ¬ (x =h= od∅ )→ HOD |
| 32 -- this should be ¬ (x =h= od∅ )→ ∃ ox → x ∋ Ord ox ( minimum of x ) | |
| 33 x∋minimal : (x : HOD ) → ( ne : ¬ (x =h= od∅ ) ) → odef x ( od→ord ( minimal x ne ) ) | |
| 330 | 34 -- minimality (may proved by ε-induction with LEM) |
| 329 | 35 minimal-1 : (x : HOD ) → ( ne : ¬ (x =h= od∅ ) ) → (y : HOD ) → ¬ ( odef (minimal x ne) (od→ord y)) ∧ (odef x (od→ord y) ) |
| 258 | 36 |
|
188
1f2c8b094908
axiom of choice → p ∨ ¬ p
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
187
diff
changeset
|
37 |
|
189
540b845ea2de
Axiom of choies implies p ∨ ( ¬ p )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
188
diff
changeset
|
38 -- |
|
540b845ea2de
Axiom of choies implies p ∨ ( ¬ p )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
188
diff
changeset
|
39 -- Axiom of choice in intutionistic logic implies the exclude middle |
|
540b845ea2de
Axiom of choies implies p ∨ ( ¬ p )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
188
diff
changeset
|
40 -- https://plato.stanford.edu/entries/axiom-choice/#AxiChoLog |
|
540b845ea2de
Axiom of choies implies p ∨ ( ¬ p )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
188
diff
changeset
|
41 -- |
| 257 | 42 |
| 331 | 43 pred-od : ( p : Set n ) → HOD |
| 44 pred-od p = record { od = record { def = λ x → (x ≡ o∅) ∧ p } ; | |
| 45 odmax = osuc o∅; <odmax = λ x → subst (λ k → k o< osuc o∅) (sym (proj1 x)) <-osuc } | |
| 46 | |
| 47 ppp : { p : Set n } { a : HOD } → pred-od p ∋ a → p | |
| 48 ppp {p} {a} d = proj2 d | |
| 257 | 49 |
| 331 | 50 p∨¬p : ( p : Set n ) → p ∨ ( ¬ p ) -- assuming axiom of choice |
| 51 p∨¬p p with is-o∅ ( od→ord (pred-od p )) | |
| 52 p∨¬p p | yes eq = case2 (¬p eq) where | |
| 53 ps = pred-od p | |
| 54 eqo∅ : ps =h= od∅ → od→ord ps ≡ o∅ | |
| 55 eqo∅ eq = subst (λ k → od→ord ps ≡ k) ord-od∅ ( cong (λ k → od→ord k ) (==→o≡ eq)) | |
| 56 lemma : ps =h= od∅ → p → ⊥ | |
| 57 lemma eq p0 = ¬x<0 {od→ord ps} (eq→ eq record { proj1 = eqo∅ eq ; proj2 = p0 } ) | |
| 58 ¬p : (od→ord ps ≡ o∅) → p → ⊥ | |
| 59 ¬p eq = lemma ( subst₂ (λ j k → j =h= k ) oiso o∅≡od∅ ( o≡→== eq )) | |
| 60 p∨¬p p | no ¬p = case1 (ppp {p} {minimal ps (λ eq → ¬p (eqo∅ eq))} lemma) where | |
| 61 ps = pred-od p | |
| 62 eqo∅ : ps =h= od∅ → od→ord ps ≡ o∅ | |
| 63 eqo∅ eq = subst (λ k → od→ord ps ≡ k) ord-od∅ ( cong (λ k → od→ord k ) (==→o≡ eq)) | |
| 64 lemma : ps ∋ minimal ps (λ eq → ¬p (eqo∅ eq)) | |
| 65 lemma = x∋minimal ps (λ eq → ¬p (eqo∅ eq)) | |
|
188
1f2c8b094908
axiom of choice → p ∨ ¬ p
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
187
diff
changeset
|
66 |
|
234
e06b76e5b682
ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
228
diff
changeset
|
67 decp : ( p : Set n ) → Dec p -- assuming axiom of choice |
|
e06b76e5b682
ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
228
diff
changeset
|
68 decp p with p∨¬p p |
|
e06b76e5b682
ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
228
diff
changeset
|
69 decp p | case1 x = yes x |
|
e06b76e5b682
ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
228
diff
changeset
|
70 decp p | case2 x = no x |
|
189
540b845ea2de
Axiom of choies implies p ∨ ( ¬ p )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
188
diff
changeset
|
71 |
| 370 | 72 ∋-p : (A x : HOD ) → Dec ( A ∋ x ) |
| 73 ∋-p A x with p∨¬p ( A ∋ x ) -- LEM | |
| 74 ∋-p A x | case1 t = yes t | |
| 75 ∋-p A x | case2 t = no (λ x → t x) | |
| 76 | |
|
223
2e1f19c949dc
sepration of ordinal from OD
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
219
diff
changeset
|
77 double-neg-eilm : {A : Set n} → ¬ ¬ A → A -- we don't have this in intutionistic logic |
|
234
e06b76e5b682
ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
228
diff
changeset
|
78 double-neg-eilm {A} notnot with decp A -- assuming axiom of choice |
|
189
540b845ea2de
Axiom of choies implies p ∨ ( ¬ p )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
188
diff
changeset
|
79 ... | yes p = p |
|
540b845ea2de
Axiom of choies implies p ∨ ( ¬ p )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
188
diff
changeset
|
80 ... | no ¬p = ⊥-elim ( notnot ¬p ) |
|
540b845ea2de
Axiom of choies implies p ∨ ( ¬ p )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
188
diff
changeset
|
81 |
| 387 | 82 open _⊆_ |
| 83 | |
| 84 power→⊆ : ( A t : HOD) → Power A ∋ t → t ⊆ A | |
| 85 power→⊆ A t PA∋t = record { incl = λ {x} t∋x → double-neg-eilm (t1 t∋x) } where | |
| 86 t1 : {x : HOD } → t ∋ x → ¬ ¬ (A ∋ x) | |
| 87 t1 = zf.IsZF.power→ isZF A t PA∋t | |
| 88 | |
| 329 | 89 OrdP : ( x : Ordinal ) ( y : HOD ) → Dec ( Ord x ∋ y ) |
|
223
2e1f19c949dc
sepration of ordinal from OD
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
219
diff
changeset
|
90 OrdP x y with trio< x (od→ord y) |
|
2e1f19c949dc
sepration of ordinal from OD
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
219
diff
changeset
|
91 OrdP x y | tri< a ¬b ¬c = no ¬c |
|
2e1f19c949dc
sepration of ordinal from OD
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
219
diff
changeset
|
92 OrdP x y | tri≈ ¬a refl ¬c = no ( o<¬≡ refl ) |
|
2e1f19c949dc
sepration of ordinal from OD
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
219
diff
changeset
|
93 OrdP x y | tri> ¬a ¬b c = yes c |
| 119 | 94 |
| 276 | 95 open import zfc |
| 190 | 96 |
| 329 | 97 HOD→ZFC : ZFC |
| 98 HOD→ZFC = record { | |
| 99 ZFSet = HOD | |
|
43
0d9b9db14361
equalitu and internal parametorisity
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
42
diff
changeset
|
100 ; _∋_ = _∋_ |
| 329 | 101 ; _≈_ = _=h=_ |
|
29
fce60b99dc55
posturate OD is isomorphic to Ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
102 ; ∅ = od∅ |
| 376 | 103 ; Select = Select |
| 276 | 104 ; isZFC = isZFC |
| 28 | 105 } where |
| 276 | 106 -- infixr 200 _∈_ |
| 96 | 107 -- infixr 230 _∩_ _∪_ |
| 376 | 108 isZFC : IsZFC (HOD ) _∋_ _=h=_ od∅ Select |
| 276 | 109 isZFC = record { |
| 110 choice-func = choice-func ; | |
| 111 choice = choice | |
|
29
fce60b99dc55
posturate OD is isomorphic to Ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
112 } where |
| 258 | 113 -- Axiom of choice ( is equivalent to the existence of minimal in our case ) |
| 162 | 114 -- ∀ X [ ∅ ∉ X → (∃ f : X → ⋃ X ) → ∀ A ∈ X ( f ( A ) ∈ A ) ] |
| 329 | 115 choice-func : (X : HOD ) → {x : HOD } → ¬ ( x =h= od∅ ) → ( X ∋ x ) → HOD |
| 258 | 116 choice-func X {x} not X∋x = minimal x not |
| 329 | 117 choice : (X : HOD ) → {A : HOD } → ( X∋A : X ∋ A ) → (not : ¬ ( A =h= od∅ )) → A ∋ choice-func X not X∋A |
| 258 | 118 choice X {A} X∋A not = x∋minimal A not |
|
78
9a7a64b2388c
infinite and replacement begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
77
diff
changeset
|
119 |