comparison 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
comparison
equal deleted inserted replaced
275:455792eaa611 276:6f10c47e4e7a
1 open import Level
2 open import Ordinals
3 module ODC {n : Level } (O : Ordinals {n} ) where
4
5 open import zf
6 open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ; _⊔_ to _n⊔_ )
7 open import Relation.Binary.PropositionalEquality
8 open import Data.Nat.Properties
9 open import Data.Empty
10 open import Relation.Nullary
11 open import Relation.Binary
12 open import Relation.Binary.Core
13
14 open import logic
15 open import nat
16 import OD
17
18 open inOrdinal O
19 open OD O
20 open OD.OD
21 open OD._==_
22
23 postulate
24 -- mimimul and x∋minimal is an Axiom of choice
25 minimal : (x : OD ) → ¬ (x == od∅ )→ OD
26 -- this should be ¬ (x == od∅ )→ ∃ ox → x ∋ Ord ox ( minimum of x )
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
31
32 --
33 -- Axiom of choice in intutionistic logic implies the exclude middle
34 -- https://plato.stanford.edu/entries/axiom-choice/#AxiChoLog
35 --
36
37 ppp : { p : Set n } { a : OD } → record { def = λ x → p } ∋ a → p
38 ppp {p} {a} d = d
39
40 p∨¬p : ( p : Set n ) → p ∨ ( ¬ p ) -- assuming axiom of choice
41 p∨¬p p with is-o∅ ( od→ord ( record { def = λ x → p } ))
42 p∨¬p p | yes eq = case2 (¬p eq) where
43 ps = record { def = λ x → p }
44 lemma : ps == od∅ → p → ⊥
45 lemma eq p0 = ¬x<0 {od→ord ps} (eq→ eq p0 )
46 ¬p : (od→ord ps ≡ o∅) → p → ⊥
47 ¬p eq = lemma ( subst₂ (λ j k → j == k ) oiso o∅≡od∅ ( o≡→== eq ))
48 p∨¬p p | no ¬p = case1 (ppp {p} {minimal ps (λ eq → ¬p (eqo∅ eq))} lemma) where
49 ps = record { def = λ x → p }
50 eqo∅ : ps == od∅ → od→ord ps ≡ o∅
51 eqo∅ eq = subst (λ k → od→ord ps ≡ k) ord-od∅ ( cong (λ k → od→ord k ) (==→o≡ eq))
52 lemma : ps ∋ minimal ps (λ eq → ¬p (eqo∅ eq))
53 lemma = x∋minimal ps (λ eq → ¬p (eqo∅ eq))
54
55 decp : ( p : Set n ) → Dec p -- assuming axiom of choice
56 decp p with p∨¬p p
57 decp p | case1 x = yes x
58 decp p | case2 x = no x
59
60 double-neg-eilm : {A : Set n} → ¬ ¬ A → A -- we don't have this in intutionistic logic
61 double-neg-eilm {A} notnot with decp A -- assuming axiom of choice
62 ... | yes p = p
63 ... | no ¬p = ⊥-elim ( notnot ¬p )
64
65 OrdP : ( x : Ordinal ) ( y : OD ) → Dec ( Ord x ∋ y )
66 OrdP x y with trio< x (od→ord y)
67 OrdP x y | tri< a ¬b ¬c = no ¬c
68 OrdP x y | tri≈ ¬a refl ¬c = no ( o<¬≡ refl )
69 OrdP x y | tri> ¬a ¬b c = yes c
70
71 open import zfc
72
73 OD→ZFC : ZFC
74 OD→ZFC = record {
75 ZFSet = OD
76 ; _∋_ = _∋_
77 ; _≈_ = _==_
78 ; ∅ = od∅
79 ; Select = Select
80 ; isZFC = isZFC
81 } where
82 -- infixr 200 _∈_
83 -- infixr 230 _∩_ _∪_
84 isZFC : IsZFC (OD ) _∋_ _==_ od∅ Select
85 isZFC = record {
86 choice-func = choice-func ;
87 choice = choice
88 } where
89 -- Axiom of choice ( is equivalent to the existence of minimal in our case )
90 -- ∀ X [ ∅ ∉ X → (∃ f : X → ⋃ X ) → ∀ A ∈ X ( f ( A ) ∈ A ) ]
91 choice-func : (X : OD ) → {x : OD } → ¬ ( x == od∅ ) → ( X ∋ x ) → OD
92 choice-func X {x} not X∋x = minimal x not
93 choice : (X : OD ) → {A : OD } → ( X∋A : X ∋ A ) → (not : ¬ ( A == od∅ )) → A ∋ choice-func X not X∋A
94 choice X {A} X∋A not = x∋minimal A not
95
96 --- With assuption of OD is ordered, p ∨ ( ¬ p ) <=> axiom of choice
97 ---
98 record choiced ( X : OD) : Set (suc n) where
99 field
100 a-choice : OD
101 is-in : X ∋ a-choice
102
103 choice-func' : (X : OD ) → (p∨¬p : ( p : Set (suc n)) → p ∨ ( ¬ p )) → ¬ ( X == od∅ ) → choiced X
104 choice-func' X p∨¬p not = have_to_find where
105 ψ : ( ox : Ordinal ) → Set (suc n)
106 ψ ox = (( x : Ordinal ) → x o< ox → ( ¬ def X x )) ∨ choiced X
107 lemma-ord : ( ox : Ordinal ) → ψ ox
108 lemma-ord ox = TransFinite {ψ} induction ox where
109 ∋-p : (A x : OD ) → Dec ( A ∋ x )
110 ∋-p A x with p∨¬p (Lift (suc n) ( A ∋ x )) -- LEM
111 ∋-p A x | case1 (lift t) = yes t
112 ∋-p A x | case2 t = no (λ x → t (lift x ))
113 ∀-imply-or : {A : Ordinal → Set n } {B : Set (suc n) }
114 → ((x : Ordinal ) → A x ∨ B) → ((x : Ordinal ) → A x) ∨ B
115 ∀-imply-or {A} {B} ∀AB with p∨¬p (Lift ( suc n ) ((x : Ordinal ) → A x)) -- LEM
116 ∀-imply-or {A} {B} ∀AB | case1 (lift t) = case1 t
117 ∀-imply-or {A} {B} ∀AB | case2 x = case2 (lemma (λ not → x (lift not ))) where
118 lemma : ¬ ((x : Ordinal ) → A x) → B
119 lemma not with p∨¬p B
120 lemma not | case1 b = b
121 lemma not | case2 ¬b = ⊥-elim (not (λ x → dont-orb (∀AB x) ¬b ))
122 induction : (x : Ordinal) → ((y : Ordinal) → y o< x → ψ y) → ψ x
123 induction x prev with ∋-p X ( ord→od x)
124 ... | yes p = case2 ( record { a-choice = ord→od x ; is-in = p } )
125 ... | no ¬p = lemma where
126 lemma1 : (y : Ordinal) → (y o< x → def X y → ⊥) ∨ choiced X
127 lemma1 y with ∋-p X (ord→od y)
128 lemma1 y | yes y<X = case2 ( record { a-choice = ord→od y ; is-in = y<X } )
129 lemma1 y | no ¬y<X = case1 ( λ lt y<X → ¬y<X (subst (λ k → def X k ) (sym diso) y<X ) )
130 lemma : ((y : Ordinals.ord O) → (O Ordinals.o< y) x → def X y → ⊥) ∨ choiced X
131 lemma = ∀-imply-or lemma1
132 have_to_find : choiced X
133 have_to_find = dont-or (lemma-ord (od→ord X )) ¬¬X∋x where
134 ¬¬X∋x : ¬ ((x : Ordinal) → x o< (od→ord X) → def X x → ⊥)
135 ¬¬X∋x nn = not record {
136 eq→ = λ {x} lt → ⊥-elim (nn x (def→o< lt) lt)
137 ; eq← = λ {x} lt → ⊥-elim ( ¬x<0 lt )
138 }
139