Mercurial > hg > Members > kono > Proof > ZF-in-agda
annotate LEMC.agda @ 403:ce2ce3f62023
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 28 Jul 2020 10:51:08 +0900 |
| parents | 8c092c042093 |
| children | 44a484f17f26 |
| rev | line source |
|---|---|
| 16 | 1 open import Level |
|
223
2e1f19c949dc
sepration of ordinal from OD
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
219
diff
changeset
|
2 open import Ordinals |
|
277
d9d3654baee1
seperate choice from LEM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
276
diff
changeset
|
3 open import logic |
|
d9d3654baee1
seperate choice from LEM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
276
diff
changeset
|
4 open import Relation.Nullary |
| 387 | 5 module LEMC {n : Level } (O : Ordinals {n} ) (p∨¬p : ( p : Set n) → p ∨ ( ¬ p )) where |
| 3 | 6 |
|
14
e11e95d5ddee
separete constructible set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
11
diff
changeset
|
7 open import zf |
| 23 | 8 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
|
9 open import Relation.Binary.PropositionalEquality |
|
e11e95d5ddee
separete constructible set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
11
diff
changeset
|
10 open import Data.Nat.Properties |
| 6 | 11 open import Data.Empty |
| 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 nat |
| 276 | 16 import OD |
|
213
22d435172d1a
separate logic and nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
210
diff
changeset
|
17 |
|
223
2e1f19c949dc
sepration of ordinal from OD
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
219
diff
changeset
|
18 open inOrdinal O |
| 276 | 19 open OD O |
| 20 open OD.OD | |
| 21 open OD._==_ | |
|
277
d9d3654baee1
seperate choice from LEM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
276
diff
changeset
|
22 open ODAxiom odAxiom |
| 119 | 23 |
| 276 | 24 open import zfc |
| 190 | 25 |
| 387 | 26 open HOD |
| 27 | |
| 28 open _⊆_ | |
| 29 | |
| 30 decp : ( p : Set n ) → Dec p -- assuming axiom of choice | |
| 31 decp p with p∨¬p p | |
| 32 decp p | case1 x = yes x | |
| 33 decp p | case2 x = no x | |
| 34 | |
| 35 ∋-p : (A x : HOD ) → Dec ( A ∋ x ) | |
| 36 ∋-p A x with p∨¬p ( A ∋ x) -- LEM | |
| 37 ∋-p A x | case1 t = yes t | |
| 38 ∋-p A x | case2 t = no (λ x → t x) | |
| 39 | |
| 40 double-neg-eilm : {A : Set n} → ¬ ¬ A → A -- we don't have this in intutionistic logic | |
| 41 double-neg-eilm {A} notnot with decp A -- assuming axiom of choice | |
| 42 ... | yes p = p | |
| 43 ... | no ¬p = ⊥-elim ( notnot ¬p ) | |
| 44 | |
| 45 power→⊆ : ( A t : HOD) → Power A ∋ t → t ⊆ A | |
| 46 power→⊆ A t PA∋t = record { incl = λ {x} t∋x → double-neg-eilm (λ not → t1 t∋x (λ x → not x) ) } where | |
| 47 t1 : {x : HOD } → t ∋ x → ¬ ¬ (A ∋ x) | |
| 396 | 48 t1 = power→ A t PA∋t |
| 387 | 49 |
| 330 | 50 --- With assuption of HOD is ordered, p ∨ ( ¬ p ) <=> axiom of choice |
|
277
d9d3654baee1
seperate choice from LEM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
276
diff
changeset
|
51 --- |
| 387 | 52 record choiced ( X : Ordinal ) : Set n where |
|
277
d9d3654baee1
seperate choice from LEM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
276
diff
changeset
|
53 field |
| 387 | 54 a-choice : Ordinal |
| 55 is-in : odef (ord→od X) a-choice | |
| 330 | 56 |
|
277
d9d3654baee1
seperate choice from LEM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
276
diff
changeset
|
57 open choiced |
|
d9d3654baee1
seperate choice from LEM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
276
diff
changeset
|
58 |
| 387 | 59 -- ∋→d : ( a : HOD ) { x : HOD } → ord→od (od→ord a) ∋ x → X ∋ ord→od (a-choice (choice-func X not)) |
| 60 -- ∋→d a lt = subst₂ (λ j k → odef j k) oiso (sym diso) lt | |
| 61 | |
| 62 oo∋ : { a : HOD} { x : Ordinal } → odef (ord→od (od→ord a)) x → a ∋ ord→od x | |
| 63 oo∋ lt = subst₂ (λ j k → odef j k) oiso (sym diso) lt | |
| 64 | |
| 65 ∋oo : { a : HOD} { x : Ordinal } → a ∋ ord→od x → odef (ord→od (od→ord a)) x | |
| 66 ∋oo lt = subst₂ (λ j k → odef j k ) (sym oiso) diso lt | |
| 67 | |
| 276 | 68 OD→ZFC : ZFC |
| 69 OD→ZFC = record { | |
| 330 | 70 ZFSet = HOD |
|
43
0d9b9db14361
equalitu and internal parametorisity
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
42
diff
changeset
|
71 ; _∋_ = _∋_ |
| 330 | 72 ; _≈_ = _=h=_ |
|
29
fce60b99dc55
posturate OD is isomorphic to Ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
73 ; ∅ = od∅ |
| 376 | 74 ; Select = Select |
| 276 | 75 ; isZFC = isZFC |
| 28 | 76 } where |
| 276 | 77 -- infixr 200 _∈_ |
| 96 | 78 -- infixr 230 _∩_ _∪_ |
| 376 | 79 isZFC : IsZFC (HOD ) _∋_ _=h=_ od∅ Select |
| 276 | 80 isZFC = record { |
| 387 | 81 choice-func = λ A {X} not A∋X → ord→od (a-choice (choice-func X not) ); |
| 82 choice = λ A {X} A∋X not → oo∋ (is-in (choice-func X not)) | |
|
29
fce60b99dc55
posturate OD is isomorphic to Ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
83 } where |
| 360 | 84 -- |
| 85 -- the axiom choice from LEM and OD ordering | |
| 86 -- | |
| 387 | 87 choice-func : (X : HOD ) → ¬ ( X =h= od∅ ) → choiced (od→ord X) |
|
277
d9d3654baee1
seperate choice from LEM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
276
diff
changeset
|
88 choice-func X not = have_to_find where |
| 387 | 89 ψ : ( ox : Ordinal ) → Set n |
| 90 ψ ox = (( x : Ordinal ) → x o< ox → ( ¬ odef X x )) ∨ choiced (od→ord X) | |
|
234
e06b76e5b682
ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
228
diff
changeset
|
91 lemma-ord : ( ox : Ordinal ) → ψ ox |
| 387 | 92 lemma-ord ox = TransFinite {ψ} induction ox where |
| 93 -- ∋-p : (A x : HOD ) → Dec ( A ∋ x ) | |
| 94 -- ∋-p A x with p∨¬p (Lift (suc n) ( A ∋ x )) -- LEM | |
| 95 -- ∋-p A x | case1 (lift t) = yes t | |
| 96 -- ∋-p A x | case2 t = no (λ x → t (lift x )) | |
| 97 ∀-imply-or : {A : Ordinal → Set n } {B : Set n } | |
|
234
e06b76e5b682
ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
228
diff
changeset
|
98 → ((x : Ordinal ) → A x ∨ B) → ((x : Ordinal ) → A x) ∨ B |
| 387 | 99 ∀-imply-or {A} {B} ∀AB with p∨¬p ((x : Ordinal ) → A x) -- LEM |
| 100 ∀-imply-or {A} {B} ∀AB | case1 t = case1 t | |
| 101 ∀-imply-or {A} {B} ∀AB | case2 x = case2 (lemma (λ not → x not )) where | |
|
234
e06b76e5b682
ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
228
diff
changeset
|
102 lemma : ¬ ((x : Ordinal ) → A x) → B |
|
e06b76e5b682
ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
228
diff
changeset
|
103 lemma not with p∨¬p B |
|
e06b76e5b682
ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
228
diff
changeset
|
104 lemma not | case1 b = b |
|
e06b76e5b682
ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
228
diff
changeset
|
105 lemma not | case2 ¬b = ⊥-elim (not (λ x → dont-orb (∀AB x) ¬b )) |
|
e06b76e5b682
ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
228
diff
changeset
|
106 induction : (x : Ordinal) → ((y : Ordinal) → y o< x → ψ y) → ψ x |
|
e06b76e5b682
ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
228
diff
changeset
|
107 induction x prev with ∋-p X ( ord→od x) |
| 387 | 108 ... | yes p = case2 ( record { a-choice = x ; is-in = ∋oo p } ) |
|
234
e06b76e5b682
ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
228
diff
changeset
|
109 ... | no ¬p = lemma where |
| 387 | 110 lemma1 : (y : Ordinal) → (y o< x → odef X y → ⊥) ∨ choiced (od→ord X) |
|
234
e06b76e5b682
ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
228
diff
changeset
|
111 lemma1 y with ∋-p X (ord→od y) |
| 387 | 112 lemma1 y | yes y<X = case2 ( record { a-choice = y ; is-in = ∋oo y<X } ) |
| 396 | 113 lemma1 y | no ¬y<X = case1 ( λ lt y<X → ¬y<X (d→∋ X y<X) ) |
| 387 | 114 lemma : ((y : Ordinals.ord O) → (O Ordinals.o< y) x → odef X y → ⊥) ∨ choiced (od→ord X) |
|
234
e06b76e5b682
ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
228
diff
changeset
|
115 lemma = ∀-imply-or lemma1 |
| 387 | 116 have_to_find : choiced (od→ord X) |
| 271 | 117 have_to_find = dont-or (lemma-ord (od→ord X )) ¬¬X∋x where |
| 330 | 118 ¬¬X∋x : ¬ ((x : Ordinal) → x o< (od→ord X) → odef X x → ⊥) |
|
234
e06b76e5b682
ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
228
diff
changeset
|
119 ¬¬X∋x nn = not record { |
| 330 | 120 eq→ = λ {x} lt → ⊥-elim (nn x (odef→o< lt) lt) |
|
234
e06b76e5b682
ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
228
diff
changeset
|
121 ; eq← = λ {x} lt → ⊥-elim ( ¬x<0 lt ) |
|
e06b76e5b682
ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
228
diff
changeset
|
122 } |
| 360 | 123 |
| 124 -- | |
| 125 -- axiom regurality from ε-induction (using axiom of choice above) | |
| 126 -- | |
| 127 -- from https://math.stackexchange.com/questions/2973777/is-it-possible-to-prove-regularity-with-transfinite-induction-only | |
| 128 -- | |
| 388 | 129 -- FIXME : don't use HOD make this level n, so we can remove ε-induction1 |
| 330 | 130 record Minimal (x : HOD) : Set (suc n) where |
| 280 | 131 field |
| 330 | 132 min : HOD |
| 281 | 133 x∋min : x ∋ min |
| 330 | 134 min-empty : (y : HOD ) → ¬ ( min ∋ y) ∧ (x ∋ y) |
| 280 | 135 open Minimal |
| 281 | 136 open _∧_ |
| 330 | 137 induction : {x : HOD} → ({y : HOD} → x ∋ y → (u : HOD ) → (u∋x : u ∋ y) → Minimal u ) |
| 138 → (u : HOD ) → (u∋x : u ∋ x) → Minimal u | |
| 387 | 139 induction {x} prev u u∋x with p∨¬p ((y : Ordinal ) → ¬ (odef x y) ∧ (odef u y)) |
| 284 | 140 ... | case1 P = |
| 141 record { min = x | |
| 387 | 142 ; x∋min = u∋x |
| 143 ; min-empty = λ y → P (od→ord y) | |
| 284 | 144 } |
| 285 | 145 ... | case2 NP = min2 where |
| 330 | 146 p : HOD |
| 147 p = record { od = record { def = λ y1 → odef x y1 ∧ odef u y1 } ; odmax = omin (odmax x) (odmax u) ; <odmax = lemma } where | |
| 148 lemma : {y : Ordinal} → OD.def (od x) y ∧ OD.def (od u) y → y o< omin (odmax x) (odmax u) | |
| 149 lemma {y} lt = min1 (<odmax x (proj1 lt)) (<odmax u (proj2 lt)) | |
| 150 np : ¬ (p =h= od∅) | |
| 396 | 151 np p∅ = NP (λ y p∋y → ∅< {p} {_} (d→∋ p p∋y) p∅ ) |
| 387 | 152 y1choice : choiced (od→ord p) |
| 284 | 153 y1choice = choice-func p np |
| 330 | 154 y1 : HOD |
| 387 | 155 y1 = ord→od (a-choice y1choice) |
| 284 | 156 y1prop : (x ∋ y1) ∧ (u ∋ y1) |
| 387 | 157 y1prop = oo∋ (is-in y1choice) |
| 285 | 158 min2 : Minimal u |
| 284 | 159 min2 = prev (proj1 y1prop) u (proj2 y1prop) |
| 330 | 160 Min2 : (x : HOD) → (u : HOD ) → (u∋x : u ∋ x) → Minimal u |
| 388 | 161 Min2 x u u∋x = (ε-induction1 {λ y → (u : HOD ) → (u∋x : u ∋ y) → Minimal u } induction x u u∋x ) |
| 387 | 162 cx : {x : HOD} → ¬ (x =h= od∅ ) → choiced (od→ord x ) |
| 284 | 163 cx {x} nx = choice-func x nx |
| 330 | 164 minimal : (x : HOD ) → ¬ (x =h= od∅ ) → HOD |
| 387 | 165 minimal x ne = min (Min2 (ord→od (a-choice (cx {x} ne) )) x ( oo∋ (is-in (cx ne))) ) |
| 330 | 166 x∋minimal : (x : HOD ) → ( ne : ¬ (x =h= od∅ ) ) → odef x ( od→ord ( minimal x ne ) ) |
| 387 | 167 x∋minimal x ne = x∋min (Min2 (ord→od (a-choice (cx {x} ne) )) x ( oo∋ (is-in (cx ne))) ) |
| 330 | 168 minimal-1 : (x : HOD ) → ( ne : ¬ (x =h= od∅ ) ) → (y : HOD ) → ¬ ( odef (minimal x ne) (od→ord y)) ∧ (odef x (od→ord y) ) |
| 387 | 169 minimal-1 x ne y = min-empty (Min2 (ord→od (a-choice (cx ne) )) x ( oo∋ (is-in (cx ne)))) y |
| 279 | 170 |
| 171 | |
| 172 | |
|
234
e06b76e5b682
ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
228
diff
changeset
|
173 |