Mercurial > hg > Members > kono > Proof > ZF-in-agda
annotate ODC.agda @ 276:6f10c47e4e7a
separate choice
fix sup-o
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Sat, 09 May 2020 09:02:52 +0900 |
parents | OD.agda@29a85a427ed2 |
children | d9d3654baee1 |
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 |
276 | 3 module ODC {n : Level } (O : Ordinals {n} ) where |
3 | 4 |
14
e11e95d5ddee
separete constructible set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
11
diff
changeset
|
5 open import zf |
23 | 6 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
|
7 open import Relation.Binary.PropositionalEquality |
e11e95d5ddee
separete constructible set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
11
diff
changeset
|
8 open import Data.Nat.Properties |
6 | 9 open import Data.Empty |
10 open import Relation.Nullary | |
11 open import Relation.Binary | |
12 open import Relation.Binary.Core | |
13 | |
213
22d435172d1a
separate logic and nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
210
diff
changeset
|
14 open import logic |
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._==_ | |
258 | 22 |
29
fce60b99dc55
posturate OD is isomorphic to Ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
23 postulate |
258 | 24 -- mimimul and x∋minimal is an Axiom of choice |
25 minimal : (x : OD ) → ¬ (x == od∅ )→ OD | |
117 | 26 -- this should be ¬ (x == od∅ )→ ∃ ox → x ∋ Ord ox ( minimum of x ) |
258 | 27 x∋minimal : (x : OD ) → ( ne : ¬ (x == od∅ ) ) → def x ( od→ord ( minimal x ne ) ) |
28 -- minimality (may proved by ε-induction ) | |
29 minimal-1 : (x : OD ) → ( ne : ¬ (x == od∅ ) ) → (y : OD ) → ¬ ( def (minimal x ne) (od→ord y)) ∧ (def x (od→ord y) ) | |
30 | |
188
1f2c8b094908
axiom of choice → p ∨ ¬ p
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
187
diff
changeset
|
31 |
189
540b845ea2de
Axiom of choies implies p ∨ ( ¬ p )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
188
diff
changeset
|
32 -- |
540b845ea2de
Axiom of choies implies p ∨ ( ¬ p )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
188
diff
changeset
|
33 -- 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
|
34 -- 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
|
35 -- |
257 | 36 |
37 ppp : { p : Set n } { a : OD } → record { def = λ x → p } ∋ a → p | |
38 ppp {p} {a} d = d | |
39 | |
223
2e1f19c949dc
sepration of ordinal from OD
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
219
diff
changeset
|
40 p∨¬p : ( p : Set n ) → p ∨ ( ¬ p ) -- assuming axiom of choice |
2e1f19c949dc
sepration of ordinal from OD
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
219
diff
changeset
|
41 p∨¬p p with is-o∅ ( od→ord ( record { def = λ x → p } )) |
2e1f19c949dc
sepration of ordinal from OD
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
219
diff
changeset
|
42 p∨¬p p | yes eq = case2 (¬p eq) where |
189
540b845ea2de
Axiom of choies implies p ∨ ( ¬ p )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
188
diff
changeset
|
43 ps = record { def = λ x → p } |
540b845ea2de
Axiom of choies implies p ∨ ( ¬ p )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
188
diff
changeset
|
44 lemma : ps == od∅ → p → ⊥ |
223
2e1f19c949dc
sepration of ordinal from OD
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
219
diff
changeset
|
45 lemma eq p0 = ¬x<0 {od→ord ps} (eq→ eq p0 ) |
189
540b845ea2de
Axiom of choies implies p ∨ ( ¬ p )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
188
diff
changeset
|
46 ¬p : (od→ord ps ≡ o∅) → p → ⊥ |
540b845ea2de
Axiom of choies implies p ∨ ( ¬ p )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
188
diff
changeset
|
47 ¬p eq = lemma ( subst₂ (λ j k → j == k ) oiso o∅≡od∅ ( o≡→== eq )) |
258 | 48 p∨¬p p | no ¬p = case1 (ppp {p} {minimal ps (λ eq → ¬p (eqo∅ eq))} lemma) where |
189
540b845ea2de
Axiom of choies implies p ∨ ( ¬ p )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
188
diff
changeset
|
49 ps = record { def = λ x → p } |
223
2e1f19c949dc
sepration of ordinal from OD
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
219
diff
changeset
|
50 eqo∅ : ps == od∅ → od→ord ps ≡ o∅ |
188
1f2c8b094908
axiom of choice → p ∨ ¬ p
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
187
diff
changeset
|
51 eqo∅ eq = subst (λ k → od→ord ps ≡ k) ord-od∅ ( cong (λ k → od→ord k ) (==→o≡ eq)) |
258 | 52 lemma : ps ∋ minimal ps (λ eq → ¬p (eqo∅ eq)) |
53 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
|
54 |
234
e06b76e5b682
ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
228
diff
changeset
|
55 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
|
56 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
|
57 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
|
58 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
|
59 |
223
2e1f19c949dc
sepration of ordinal from OD
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
219
diff
changeset
|
60 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
|
61 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
|
62 ... | yes p = p |
540b845ea2de
Axiom of choies implies p ∨ ( ¬ p )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
188
diff
changeset
|
63 ... | no ¬p = ⊥-elim ( notnot ¬p ) |
540b845ea2de
Axiom of choies implies p ∨ ( ¬ p )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
188
diff
changeset
|
64 |
223
2e1f19c949dc
sepration of ordinal from OD
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
219
diff
changeset
|
65 OrdP : ( x : Ordinal ) ( y : OD ) → Dec ( Ord x ∋ y ) |
2e1f19c949dc
sepration of ordinal from OD
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
219
diff
changeset
|
66 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
|
67 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
|
68 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
|
69 OrdP x y | tri> ¬a ¬b c = yes c |
119 | 70 |
276 | 71 open import zfc |
190 | 72 |
276 | 73 OD→ZFC : ZFC |
74 OD→ZFC = record { | |
223
2e1f19c949dc
sepration of ordinal from OD
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
219
diff
changeset
|
75 ZFSet = OD |
43
0d9b9db14361
equalitu and internal parametorisity
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
42
diff
changeset
|
76 ; _∋_ = _∋_ |
0d9b9db14361
equalitu and internal parametorisity
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
42
diff
changeset
|
77 ; _≈_ = _==_ |
29
fce60b99dc55
posturate OD is isomorphic to Ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
78 ; ∅ = od∅ |
28 | 79 ; Select = Select |
276 | 80 ; isZFC = isZFC |
28 | 81 } where |
276 | 82 -- infixr 200 _∈_ |
96 | 83 -- infixr 230 _∩_ _∪_ |
276 | 84 isZFC : IsZFC (OD ) _∋_ _==_ od∅ Select |
85 isZFC = record { | |
86 choice-func = choice-func ; | |
87 choice = choice | |
29
fce60b99dc55
posturate OD is isomorphic to Ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
88 } where |
258 | 89 -- Axiom of choice ( is equivalent to the existence of minimal in our case ) |
162 | 90 -- ∀ X [ ∅ ∉ X → (∃ f : X → ⋃ X ) → ∀ A ∈ X ( f ( A ) ∈ A ) ] |
223
2e1f19c949dc
sepration of ordinal from OD
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
219
diff
changeset
|
91 choice-func : (X : OD ) → {x : OD } → ¬ ( x == od∅ ) → ( X ∋ x ) → OD |
258 | 92 choice-func X {x} not X∋x = minimal x not |
223
2e1f19c949dc
sepration of ordinal from OD
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
219
diff
changeset
|
93 choice : (X : OD ) → {A : OD } → ( X∋A : X ∋ A ) → (not : ¬ ( A == od∅ )) → A ∋ choice-func X not X∋A |
258 | 94 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
|
95 |
234
e06b76e5b682
ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
228
diff
changeset
|
96 --- With assuption of OD is ordered, p ∨ ( ¬ p ) <=> axiom of choice |
e06b76e5b682
ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
228
diff
changeset
|
97 --- |
e06b76e5b682
ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
228
diff
changeset
|
98 record choiced ( X : OD) : Set (suc n) where |
e06b76e5b682
ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
228
diff
changeset
|
99 field |
e06b76e5b682
ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
228
diff
changeset
|
100 a-choice : OD |
e06b76e5b682
ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
228
diff
changeset
|
101 is-in : X ∋ a-choice |
e06b76e5b682
ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
228
diff
changeset
|
102 |
e06b76e5b682
ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
228
diff
changeset
|
103 choice-func' : (X : OD ) → (p∨¬p : ( p : Set (suc n)) → p ∨ ( ¬ p )) → ¬ ( X == od∅ ) → choiced X |
e06b76e5b682
ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
228
diff
changeset
|
104 choice-func' X p∨¬p not = have_to_find where |
e06b76e5b682
ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
228
diff
changeset
|
105 ψ : ( ox : Ordinal ) → Set (suc n) |
e06b76e5b682
ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
228
diff
changeset
|
106 ψ ox = (( x : Ordinal ) → x o< ox → ( ¬ def X x )) ∨ choiced X |
e06b76e5b682
ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
228
diff
changeset
|
107 lemma-ord : ( ox : Ordinal ) → ψ ox |
235 | 108 lemma-ord ox = TransFinite {ψ} induction ox where |
234
e06b76e5b682
ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
228
diff
changeset
|
109 ∋-p : (A x : OD ) → Dec ( A ∋ x ) |
271 | 110 ∋-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
|
111 ∋-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
|
112 ∋-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
|
113 ∀-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
|
114 → ((x : Ordinal ) → A x ∨ B) → ((x : Ordinal ) → A x) ∨ B |
271 | 115 ∀-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
|
116 ∀-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
|
117 ∀-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
|
118 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
|
119 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
|
120 lemma not | case1 b = b |
e06b76e5b682
ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
228
diff
changeset
|
121 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
|
122 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
|
123 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
|
124 ... | 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
|
125 ... | no ¬p = lemma where |
e06b76e5b682
ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
228
diff
changeset
|
126 lemma1 : (y : Ordinal) → (y o< x → def X y → ⊥) ∨ choiced X |
e06b76e5b682
ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
228
diff
changeset
|
127 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
|
128 lemma1 y | yes y<X = case2 ( record { a-choice = ord→od y ; is-in = y<X } ) |
e06b76e5b682
ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
228
diff
changeset
|
129 lemma1 y | no ¬y<X = case1 ( λ lt y<X → ¬y<X (subst (λ k → def X k ) (sym diso) y<X ) ) |
e06b76e5b682
ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
228
diff
changeset
|
130 lemma : ((y : Ordinals.ord O) → (O Ordinals.o< y) x → def X y → ⊥) ∨ choiced X |
e06b76e5b682
ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
228
diff
changeset
|
131 lemma = ∀-imply-or lemma1 |
e06b76e5b682
ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
228
diff
changeset
|
132 have_to_find : choiced X |
271 | 133 have_to_find = dont-or (lemma-ord (od→ord X )) ¬¬X∋x where |
234
e06b76e5b682
ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
228
diff
changeset
|
134 ¬¬X∋x : ¬ ((x : Ordinal) → x o< (od→ord X) → def X x → ⊥) |
e06b76e5b682
ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
228
diff
changeset
|
135 ¬¬X∋x nn = not record { |
e06b76e5b682
ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
228
diff
changeset
|
136 eq→ = λ {x} lt → ⊥-elim (nn x (def→o< lt) lt) |
e06b76e5b682
ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
228
diff
changeset
|
137 ; 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
|
138 } |
e06b76e5b682
ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
228
diff
changeset
|
139 |