Mercurial > hg > Members > kono > Proof > ZF-in-agda
annotate LEMC.agda @ 370:1425104bb5d8
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Sun, 19 Jul 2020 12:26:17 +0900 |
parents | 17adeeee0c2a |
children | 6c72bee25653 |
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 |
d9d3654baee1
seperate choice from LEM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
276
diff
changeset
|
5 module LEMC {n : Level } (O : Ordinals {n} ) (p∨¬p : ( p : Set (suc 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 |
330 | 26 --- 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
|
27 --- |
330 | 28 record choiced ( X : HOD) : Set (suc n) where |
277
d9d3654baee1
seperate choice from LEM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
276
diff
changeset
|
29 field |
330 | 30 a-choice : HOD |
277
d9d3654baee1
seperate choice from LEM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
276
diff
changeset
|
31 is-in : X ∋ a-choice |
d9d3654baee1
seperate choice from LEM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
276
diff
changeset
|
32 |
330 | 33 open HOD |
34 | |
277
d9d3654baee1
seperate choice from LEM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
276
diff
changeset
|
35 open choiced |
d9d3654baee1
seperate choice from LEM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
276
diff
changeset
|
36 |
276 | 37 OD→ZFC : ZFC |
38 OD→ZFC = record { | |
330 | 39 ZFSet = HOD |
43
0d9b9db14361
equalitu and internal parametorisity
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
42
diff
changeset
|
40 ; _∋_ = _∋_ |
330 | 41 ; _≈_ = _=h=_ |
29
fce60b99dc55
posturate OD is isomorphic to Ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
42 ; ∅ = od∅ |
370 | 43 ; Select = {!!} |
276 | 44 ; isZFC = isZFC |
28 | 45 } where |
276 | 46 -- infixr 200 _∈_ |
96 | 47 -- infixr 230 _∩_ _∪_ |
370 | 48 isZFC : IsZFC (HOD ) _∋_ _=h=_ od∅ {!!} |
276 | 49 isZFC = record { |
277
d9d3654baee1
seperate choice from LEM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
276
diff
changeset
|
50 choice-func = λ A {X} not A∋X → a-choice (choice-func X not ); |
d9d3654baee1
seperate choice from LEM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
276
diff
changeset
|
51 choice = λ A {X} A∋X not → 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
|
52 } where |
360 | 53 -- |
54 -- the axiom choice from LEM and OD ordering | |
55 -- | |
330 | 56 choice-func : (X : HOD ) → ¬ ( X =h= od∅ ) → choiced X |
277
d9d3654baee1
seperate choice from LEM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
276
diff
changeset
|
57 choice-func X not = have_to_find where |
234
e06b76e5b682
ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
228
diff
changeset
|
58 ψ : ( ox : Ordinal ) → Set (suc n) |
330 | 59 ψ ox = (( x : Ordinal ) → x o< ox → ( ¬ odef X x )) ∨ choiced X |
234
e06b76e5b682
ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
228
diff
changeset
|
60 lemma-ord : ( ox : Ordinal ) → ψ ox |
330 | 61 lemma-ord ox = TransFinite1 {ψ} induction ox where |
62 ∋-p : (A x : HOD ) → Dec ( A ∋ x ) | |
271 | 63 ∋-p A x with p∨¬p (Lift (suc n) ( A ∋ x )) -- LEM |
234
e06b76e5b682
ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
228
diff
changeset
|
64 ∋-p A x | case1 (lift t) = yes t |
e06b76e5b682
ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
228
diff
changeset
|
65 ∋-p A x | case2 t = no (λ x → t (lift x )) |
e06b76e5b682
ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
228
diff
changeset
|
66 ∀-imply-or : {A : Ordinal → Set n } {B : Set (suc n) } |
e06b76e5b682
ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
228
diff
changeset
|
67 → ((x : Ordinal ) → A x ∨ B) → ((x : Ordinal ) → A x) ∨ B |
271 | 68 ∀-imply-or {A} {B} ∀AB with p∨¬p (Lift ( suc n ) ((x : Ordinal ) → A x)) -- LEM |
234
e06b76e5b682
ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
228
diff
changeset
|
69 ∀-imply-or {A} {B} ∀AB | case1 (lift t) = case1 t |
e06b76e5b682
ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
228
diff
changeset
|
70 ∀-imply-or {A} {B} ∀AB | case2 x = case2 (lemma (λ not → x (lift not ))) where |
e06b76e5b682
ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
228
diff
changeset
|
71 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
|
72 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
|
73 lemma not | case1 b = b |
e06b76e5b682
ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
228
diff
changeset
|
74 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
|
75 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
|
76 induction x prev with ∋-p X ( ord→od x) |
e06b76e5b682
ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
228
diff
changeset
|
77 ... | yes p = case2 ( record { a-choice = ord→od x ; is-in = p } ) |
e06b76e5b682
ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
228
diff
changeset
|
78 ... | no ¬p = lemma where |
330 | 79 lemma1 : (y : Ordinal) → (y o< x → odef X y → ⊥) ∨ choiced X |
234
e06b76e5b682
ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
228
diff
changeset
|
80 lemma1 y with ∋-p X (ord→od y) |
e06b76e5b682
ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
228
diff
changeset
|
81 lemma1 y | yes y<X = case2 ( record { a-choice = ord→od y ; is-in = y<X } ) |
330 | 82 lemma1 y | no ¬y<X = case1 ( λ lt y<X → ¬y<X (subst (λ k → odef X k ) (sym diso) y<X ) ) |
83 lemma : ((y : Ordinals.ord O) → (O Ordinals.o< y) x → odef X y → ⊥) ∨ choiced X | |
234
e06b76e5b682
ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
228
diff
changeset
|
84 lemma = ∀-imply-or lemma1 |
e06b76e5b682
ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
228
diff
changeset
|
85 have_to_find : choiced X |
271 | 86 have_to_find = dont-or (lemma-ord (od→ord X )) ¬¬X∋x where |
330 | 87 ¬¬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
|
88 ¬¬X∋x nn = not record { |
330 | 89 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
|
90 ; 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
|
91 } |
360 | 92 |
93 -- | |
94 -- axiom regurality from ε-induction (using axiom of choice above) | |
95 -- | |
96 -- from https://math.stackexchange.com/questions/2973777/is-it-possible-to-prove-regularity-with-transfinite-induction-only | |
97 -- | |
330 | 98 record Minimal (x : HOD) : Set (suc n) where |
280 | 99 field |
330 | 100 min : HOD |
281 | 101 x∋min : x ∋ min |
330 | 102 min-empty : (y : HOD ) → ¬ ( min ∋ y) ∧ (x ∋ y) |
280 | 103 open Minimal |
281 | 104 open _∧_ |
330 | 105 induction : {x : HOD} → ({y : HOD} → x ∋ y → (u : HOD ) → (u∋x : u ∋ y) → Minimal u ) |
106 → (u : HOD ) → (u∋x : u ∋ x) → Minimal u | |
107 induction {x} prev u u∋x with p∨¬p ((y : HOD) → ¬ (x ∋ y) ∧ (u ∋ y)) | |
284 | 108 ... | case1 P = |
109 record { min = x | |
110 ; x∋min = u∋x | |
111 ; min-empty = P | |
112 } | |
285 | 113 ... | case2 NP = min2 where |
330 | 114 p : HOD |
115 p = record { od = record { def = λ y1 → odef x y1 ∧ odef u y1 } ; odmax = omin (odmax x) (odmax u) ; <odmax = lemma } where | |
116 lemma : {y : Ordinal} → OD.def (od x) y ∧ OD.def (od u) y → y o< omin (odmax x) (odmax u) | |
117 lemma {y} lt = min1 (<odmax x (proj1 lt)) (<odmax u (proj2 lt)) | |
118 np : ¬ (p =h= od∅) | |
331 | 119 np p∅ = NP (λ y p∋y → ∅< {p} {_} p∋y p∅ ) |
284 | 120 y1choice : choiced p |
121 y1choice = choice-func p np | |
330 | 122 y1 : HOD |
284 | 123 y1 = a-choice y1choice |
124 y1prop : (x ∋ y1) ∧ (u ∋ y1) | |
125 y1prop = is-in y1choice | |
285 | 126 min2 : Minimal u |
284 | 127 min2 = prev (proj1 y1prop) u (proj2 y1prop) |
330 | 128 Min2 : (x : HOD) → (u : HOD ) → (u∋x : u ∋ x) → Minimal u |
129 Min2 x u u∋x = (ε-induction1 {λ y → (u : HOD ) → (u∋x : u ∋ y) → Minimal u } induction x u u∋x ) | |
130 cx : {x : HOD} → ¬ (x =h= od∅ ) → choiced x | |
284 | 131 cx {x} nx = choice-func x nx |
330 | 132 minimal : (x : HOD ) → ¬ (x =h= od∅ ) → HOD |
331 | 133 minimal x ne = min (Min2 (a-choice (cx {x} ne) ) x (is-in (cx ne))) |
330 | 134 x∋minimal : (x : HOD ) → ( ne : ¬ (x =h= od∅ ) ) → odef x ( od→ord ( minimal x ne ) ) |
331 | 135 x∋minimal x ne = x∋min (Min2 (a-choice (cx {x} ne) ) x (is-in (cx ne))) |
330 | 136 minimal-1 : (x : HOD ) → ( ne : ¬ (x =h= od∅ ) ) → (y : HOD ) → ¬ ( odef (minimal x ne) (od→ord y)) ∧ (odef x (od→ord y) ) |
284 | 137 minimal-1 x ne y = min-empty (Min2 (a-choice (cx ne) ) x (is-in (cx ne))) y |
279 | 138 |
139 | |
140 | |
234
e06b76e5b682
ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
228
diff
changeset
|
141 |