Mercurial > hg > Members > kono > Proof > ZF-in-agda

annotate ODC.agda @ 324:fbabb20f222e

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 04 Jul 2020 18:18:17 +0900
parents 197e0b3d39dc
children 5544f4921a44
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
16
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
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
6f10c47e4e7a separate choice
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 274
diff changeset
3 module ODC {n : Level } (O : Ordinals {n} ) where
3
e7990ff544bf reocrd ZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
4
14
e11e95d5ddee separete constructible set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 11
diff changeset
5 open import zf
23
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 22
diff changeset
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
d9b704508281 isEquiv and isZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
9 open import Data.Empty
d9b704508281 isEquiv and isZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
10 open import Relation.Nullary
d9b704508281 isEquiv and isZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
11 open import Relation.Binary
d9b704508281 isEquiv and isZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
12 open import Relation.Binary.Core
d9b704508281 isEquiv and isZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
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
6f10c47e4e7a separate choice
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 274
diff changeset
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
6f10c47e4e7a separate choice
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 274
diff changeset
19 open OD O
6f10c47e4e7a separate choice
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 274
diff changeset
20 open OD.OD
6f10c47e4e7a separate choice
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 274
diff changeset
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
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 257
diff changeset
23
29
fce60b99dc55 posturate OD is isomorphic to Ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 28
diff changeset
24 postulate
258
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 257
diff changeset
25 -- mimimul and x∋minimal is an Axiom of choice
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 257
diff changeset
26 minimal : (x : OD ) → ¬ (x == od∅ )→ OD
117
a4c97390d312 minimum assuption
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 116
diff changeset
27 -- this should be ¬ (x == od∅ )→ ∃ ox → x ∋ Ord ox ( minimum of x )
258
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 257
diff changeset
28 x∋minimal : (x : OD ) → ( ne : ¬ (x == od∅ ) ) → def x ( od→ord ( minimal x ne ) )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 257
diff changeset
29 -- minimality (may proved by ε-induction )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 257
diff changeset
30 minimal-1 : (x : OD ) → ( ne : ¬ (x == od∅ ) ) → (y : OD ) → ¬ ( def (minimal x ne) (od→ord y)) ∧ (def x (od→ord y) )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 257
diff changeset
31
188
1f2c8b094908 axiom of choice → p ∨ ¬ p
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 187
diff changeset
32
189
540b845ea2de Axiom of choies implies p ∨ ( ¬ p )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 188
diff changeset
33 --
540b845ea2de Axiom of choies implies p ∨ ( ¬ p )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 188
diff changeset
34 -- 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
35 -- 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
36 --
257
53b7acd63481 move product to OD
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 254
diff changeset
37
53b7acd63481 move product to OD
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 254
diff changeset
38 ppp : { p : Set n } { a : OD } → record { def = λ x → p } ∋ a → p
53b7acd63481 move product to OD
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 254
diff changeset
39 ppp {p} {a} d = d
53b7acd63481 move product to OD
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 254
diff changeset
40
223
2e1f19c949dc sepration of ordinal from OD
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 219
diff changeset
41 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
42 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
43 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
44 ps = record { def = λ x → p }
540b845ea2de Axiom of choies implies p ∨ ( ¬ p )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 188
diff changeset
45 lemma : ps == od∅ → p → ⊥
223
2e1f19c949dc sepration of ordinal from OD
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 219
diff changeset
46 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
47 ¬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
48 ¬p eq = lemma ( subst₂ (λ j k → j == k ) oiso o∅≡od∅ ( o≡→== eq ))
258
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 257
diff changeset
49 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
50 ps = record { def = λ x → p }
223
2e1f19c949dc sepration of ordinal from OD
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 219
diff changeset
51 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
52 eqo∅ eq = subst (λ k → od→ord ps ≡ k) ord-od∅ ( cong (λ k → od→ord k ) (==→o≡ eq))
258
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 257
diff changeset
53 lemma : ps ∋ minimal ps (λ eq → ¬p (eqo∅ eq))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 257
diff changeset
54 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
55
234
e06b76e5b682 ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 228
diff changeset
56 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
57 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
58 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
59 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
60
223
2e1f19c949dc sepration of ordinal from OD
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 219
diff changeset
61 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
62 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
63 ... | yes p = p
540b845ea2de Axiom of choies implies p ∨ ( ¬ p )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 188
diff changeset
64 ... | no ¬p = ⊥-elim ( notnot ¬p )
540b845ea2de Axiom of choies implies p ∨ ( ¬ p )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 188
diff changeset
65
223
2e1f19c949dc sepration of ordinal from OD
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 219
diff changeset
66 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
67 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
68 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
69 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
70 OrdP x y | tri> ¬a ¬b c = yes c
119
6e264c78e420 infinite
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 118
diff changeset
71
276
6f10c47e4e7a separate choice
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 274
diff changeset
72 open import zfc
190
6e778b0a7202 add filter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 189
diff changeset
73
276
6f10c47e4e7a separate choice
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 274
diff changeset
74 OD→ZFC : ZFC
6f10c47e4e7a separate choice
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 274
diff changeset
75 OD→ZFC = record {
223
2e1f19c949dc sepration of ordinal from OD
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 219
diff changeset
76 ZFSet = OD
43
0d9b9db14361 equalitu and internal parametorisity
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 42
diff changeset
77 ; _∋_ = _∋_
0d9b9db14361 equalitu and internal parametorisity
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 42
diff changeset
78 ; _≈_ = _==_
29
fce60b99dc55 posturate OD is isomorphic to Ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 28
diff changeset
79 ; ∅ = od∅
28
f36e40d5d2c3 OD continue
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 27
diff changeset
80 ; Select = Select
276
6f10c47e4e7a separate choice
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 274
diff changeset
81 ; isZFC = isZFC
28
f36e40d5d2c3 OD continue
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 27
diff changeset
82 } where
276
6f10c47e4e7a separate choice
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 274
diff changeset
83 -- infixr 200 _∈_
96
f239ffc27fd0 Power Set and L
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 95
diff changeset
84 -- infixr 230 _∩_ _∪_
276
6f10c47e4e7a separate choice
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 274
diff changeset
85 isZFC : IsZFC (OD ) _∋_ _==_ od∅ Select
6f10c47e4e7a separate choice
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 274
diff changeset
86 isZFC = record {
6f10c47e4e7a separate choice
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 274
diff changeset
87 choice-func = choice-func ;
6f10c47e4e7a separate choice
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 274
diff changeset
88 choice = choice
29
fce60b99dc55 posturate OD is isomorphic to Ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 28
diff changeset
89 } where
258
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 257
diff changeset
90 -- Axiom of choice ( is equivalent to the existence of minimal in our case )
162
b06f5d2f34b1 Axiom of choice
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 161
diff changeset
91 -- ∀ 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
92 choice-func : (X : OD ) → {x : OD } → ¬ ( x == od∅ ) → ( X ∋ x ) → OD
258
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 257
diff changeset
93 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
94 choice : (X : OD ) → {A : OD } → ( X∋A : X ∋ A ) → (not : ¬ ( A == od∅ )) → A ∋ choice-func X not X∋A
258
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 257
diff changeset
95 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
96