Mercurial > hg > Members > kono > Proof > ZF-in-agda
annotate ODC.agda @ 329:5544f4921a44
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Sun, 05 Jul 2020 12:32:09 +0900 |
parents | 197e0b3d39dc |
children | 0faa7120e4b5 |
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._==_ | |
277
d9d3654baee1
seperate choice from LEM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
276
diff
changeset
|
22 open ODAxiom odAxiom |
258 | 23 |
329 | 24 open HOD |
25 | |
26 _=h=_ : (x y : HOD) → Set n | |
27 x =h= y = od x == od y | |
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 ) ) | |
258 | 34 -- minimality (may proved by ε-induction ) |
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 |
329 | 43 -- ppp : { p : Set n } { a : HOD } → record { def = λ x → p } ∋ a → p |
44 -- ppp {p} {a} d = d | |
257 | 45 |
329 | 46 -- p∨¬p : ( p : Set n ) → p ∨ ( ¬ p ) -- assuming axiom of choice |
47 -- p∨¬p p with is-o∅ ( od→ord ( record { odef = λ x → p } )) | |
48 -- p∨¬p p | yes eq = case2 (¬p eq) where | |
49 -- ps = record { odef = λ x → p } | |
50 -- lemma : ps =h= od∅ → p → ⊥ | |
51 -- lemma eq p0 = ¬x<0 {od→ord ps} (eq→ eq p0 ) | |
52 -- ¬p : (od→ord ps ≡ o∅) → p → ⊥ | |
53 -- ¬p eq = lemma ( subst₂ (λ j k → j =h= k ) oiso o∅≡od∅ ( o≡→== eq )) | |
54 -- p∨¬p p | no ¬p = case1 (ppp {p} {minimal ps (λ eq → ¬p (eqo∅ eq))} lemma) where | |
55 -- ps = record { odef = λ x → p } | |
56 -- eqo∅ : ps =h= od∅ → od→ord ps ≡ o∅ | |
57 -- eqo∅ eq = subst (λ k → od→ord ps ≡ k) ord-od∅ ( cong (λ k → od→ord k ) (==→o≡ eq)) | |
58 -- lemma : ps ∋ minimal ps (λ eq → ¬p (eqo∅ eq)) | |
59 -- lemma = x∋minimal ps (λ eq → ¬p (eqo∅ eq)) | |
60 | |
61 postulate | |
62 p∨¬p : ( p : Set n ) → p ∨ ( ¬ p ) -- assuming axiom of choice | |
188
1f2c8b094908
axiom of choice → p ∨ ¬ p
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
187
diff
changeset
|
63 |
234
e06b76e5b682
ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
228
diff
changeset
|
64 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
|
65 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
|
66 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
|
67 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
|
68 |
223
2e1f19c949dc
sepration of ordinal from OD
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
219
diff
changeset
|
69 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
|
70 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
|
71 ... | yes p = p |
540b845ea2de
Axiom of choies implies p ∨ ( ¬ p )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
188
diff
changeset
|
72 ... | no ¬p = ⊥-elim ( notnot ¬p ) |
540b845ea2de
Axiom of choies implies p ∨ ( ¬ p )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
188
diff
changeset
|
73 |
329 | 74 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
|
75 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
|
76 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
|
77 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
|
78 OrdP x y | tri> ¬a ¬b c = yes c |
119 | 79 |
276 | 80 open import zfc |
190 | 81 |
329 | 82 HOD→ZFC : ZFC |
83 HOD→ZFC = record { | |
84 ZFSet = HOD | |
43
0d9b9db14361
equalitu and internal parametorisity
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
42
diff
changeset
|
85 ; _∋_ = _∋_ |
329 | 86 ; _≈_ = _=h=_ |
29
fce60b99dc55
posturate OD is isomorphic to Ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
87 ; ∅ = od∅ |
28 | 88 ; Select = Select |
276 | 89 ; isZFC = isZFC |
28 | 90 } where |
276 | 91 -- infixr 200 _∈_ |
96 | 92 -- infixr 230 _∩_ _∪_ |
329 | 93 isZFC : IsZFC (HOD ) _∋_ _=h=_ od∅ Select |
276 | 94 isZFC = record { |
95 choice-func = choice-func ; | |
96 choice = choice | |
29
fce60b99dc55
posturate OD is isomorphic to Ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
97 } where |
258 | 98 -- Axiom of choice ( is equivalent to the existence of minimal in our case ) |
162 | 99 -- ∀ X [ ∅ ∉ X → (∃ f : X → ⋃ X ) → ∀ A ∈ X ( f ( A ) ∈ A ) ] |
329 | 100 choice-func : (X : HOD ) → {x : HOD } → ¬ ( x =h= od∅ ) → ( X ∋ x ) → HOD |
258 | 101 choice-func X {x} not X∋x = minimal x not |
329 | 102 choice : (X : HOD ) → {A : HOD } → ( X∋A : X ∋ A ) → (not : ¬ ( A =h= od∅ )) → A ∋ choice-func X not X∋A |
258 | 103 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
|
104 |