|
431
|
1 open import Level
|
|
|
2 open import Ordinals
|
|
|
3 open import logic
|
|
|
4 open import Relation.Nullary
|
|
1120
|
5 module LEMC {n : Level } (O : Ordinals {n} ) where
|
|
431
|
6
|
|
|
7 open import zf
|
|
|
8 open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ; _⊔_ to _n⊔_ )
|
|
|
9 open import Relation.Binary.PropositionalEquality
|
|
|
10 open import Data.Nat.Properties
|
|
|
11 open import Data.Empty
|
|
|
12 open import Relation.Binary
|
|
|
13 open import Relation.Binary.Core
|
|
|
14
|
|
|
15 open import nat
|
|
|
16 import OD
|
|
|
17
|
|
|
18 open inOrdinal O
|
|
|
19 open OD O
|
|
|
20 open OD.OD
|
|
|
21 open OD._==_
|
|
|
22 open ODAxiom odAxiom
|
|
|
23 import OrdUtil
|
|
|
24 import ODUtil
|
|
|
25 open Ordinals.Ordinals O
|
|
|
26 open Ordinals.IsOrdinals isOrdinal
|
|
|
27 open Ordinals.IsNext isNext
|
|
|
28 open OrdUtil O
|
|
|
29 open ODUtil O
|
|
|
30
|
|
|
31 open import zfc
|
|
|
32
|
|
|
33 open HOD
|
|
|
34
|
|
1120
|
35 postulate
|
|
|
36 p∨¬p : ( p : Set n) → p ∨ ( ¬ p )
|
|
|
37
|
|
431
|
38 decp : ( p : Set n ) → Dec p -- assuming axiom of choice
|
|
|
39 decp p with p∨¬p p
|
|
|
40 decp p | case1 x = yes x
|
|
|
41 decp p | case2 x = no x
|
|
|
42
|
|
|
43 ∋-p : (A x : HOD ) → Dec ( A ∋ x )
|
|
|
44 ∋-p A x with p∨¬p ( A ∋ x) -- LEM
|
|
|
45 ∋-p A x | case1 t = yes t
|
|
|
46 ∋-p A x | case2 t = no (λ x → t x)
|
|
|
47
|
|
1120
|
48 double-neg-elim : {A : Set n} → ¬ ¬ A → A -- we don't have this in intutionistic logic
|
|
|
49 double-neg-elim {A} notnot with decp A -- assuming axiom of choice
|
|
431
|
50 ... | yes p = p
|
|
|
51 ... | no ¬p = ⊥-elim ( notnot ¬p )
|
|
|
52
|
|
1120
|
53 -- by-contradiction : {A : Set n} {B : A → Set n} → ¬ ( (a : A ) → ¬ B a ) → A
|
|
|
54 -- by-contradiction {A} {B} not with p∨¬p A
|
|
|
55 -- ... | case2 ¬a = ⊥-elim (not (λ a → ⊥-elim (¬a a )))
|
|
|
56 -- ... | case1 a = a
|
|
|
57
|
|
431
|
58 power→⊆ : ( A t : HOD) → Power A ∋ t → t ⊆ A
|
|
1096
|
59 power→⊆ A t PA∋t t∋x = subst (λ k → odef A k ) &iso ( t1 (subst (λ k → odef t k ) (sym &iso) t∋x)) where
|
|
|
60 t1 : {x : HOD } → t ∋ x → A ∋ x
|
|
431
|
61 t1 = power→ A t PA∋t
|
|
|
62
|
|
|
63 --- With assuption of HOD is ordered, p ∨ ( ¬ p ) <=> axiom of choice
|
|
|
64 ---
|
|
|
65 record choiced ( X : Ordinal ) : Set n where
|
|
|
66 field
|
|
|
67 a-choice : Ordinal
|
|
|
68 is-in : odef (* X) a-choice
|
|
|
69
|
|
|
70 open choiced
|
|
|
71
|
|
|
72 -- ∋→d : ( a : HOD ) { x : HOD } → * (& a) ∋ x → X ∋ * (a-choice (choice-func X not))
|
|
|
73 -- ∋→d a lt = subst₂ (λ j k → odef j k) *iso (sym &iso) lt
|
|
|
74
|
|
|
75 oo∋ : { a : HOD} { x : Ordinal } → odef (* (& a)) x → a ∋ * x
|
|
|
76 oo∋ lt = subst₂ (λ j k → odef j k) *iso (sym &iso) lt
|
|
|
77
|
|
|
78 ∋oo : { a : HOD} { x : Ordinal } → a ∋ * x → odef (* (& a)) x
|
|
|
79 ∋oo lt = subst₂ (λ j k → odef j k ) (sym *iso) &iso lt
|
|
|
80
|
|
|
81 OD→ZFC : ZFC
|
|
|
82 OD→ZFC = record {
|
|
|
83 ZFSet = HOD
|
|
|
84 ; _∋_ = _∋_
|
|
|
85 ; _≈_ = _=h=_
|
|
|
86 ; ∅ = od∅
|
|
|
87 ; Select = Select
|
|
|
88 ; isZFC = isZFC
|
|
|
89 } where
|
|
|
90 -- infixr 200 _∈_
|
|
|
91 -- infixr 230 _∩_ _∪_
|
|
|
92 isZFC : IsZFC (HOD ) _∋_ _=h=_ od∅ Select
|
|
|
93 isZFC = record {
|
|
|
94 choice-func = λ A {X} not A∋X → * (a-choice (choice-func X not) );
|
|
|
95 choice = λ A {X} A∋X not → oo∋ (is-in (choice-func X not))
|
|
|
96 } where
|
|
|
97 --
|
|
|
98 -- the axiom choice from LEM and OD ordering
|
|
|
99 --
|
|
|
100 choice-func : (X : HOD ) → ¬ ( X =h= od∅ ) → choiced (& X)
|
|
|
101 choice-func X not = have_to_find where
|
|
|
102 ψ : ( ox : Ordinal ) → Set n
|
|
|
103 ψ ox = (( x : Ordinal ) → x o< ox → ( ¬ odef X x )) ∨ choiced (& X)
|
|
|
104 lemma-ord : ( ox : Ordinal ) → ψ ox
|
|
|
105 lemma-ord ox = TransFinite0 {ψ} induction ox where
|
|
|
106 ∀-imply-or : {A : Ordinal → Set n } {B : Set n }
|
|
|
107 → ((x : Ordinal ) → A x ∨ B) → ((x : Ordinal ) → A x) ∨ B
|
|
|
108 ∀-imply-or {A} {B} ∀AB with p∨¬p ((x : Ordinal ) → A x) -- LEM
|
|
|
109 ∀-imply-or {A} {B} ∀AB | case1 t = case1 t
|
|
|
110 ∀-imply-or {A} {B} ∀AB | case2 x = case2 (lemma (λ not → x not )) where
|
|
|
111 lemma : ¬ ((x : Ordinal ) → A x) → B
|
|
|
112 lemma not with p∨¬p B
|
|
|
113 lemma not | case1 b = b
|
|
|
114 lemma not | case2 ¬b = ⊥-elim (not (λ x → dont-orb (∀AB x) ¬b ))
|
|
|
115 induction : (x : Ordinal) → ((y : Ordinal) → y o< x → ψ y) → ψ x
|
|
|
116 induction x prev with ∋-p X ( * x)
|
|
|
117 ... | yes p = case2 ( record { a-choice = x ; is-in = ∋oo p } )
|
|
|
118 ... | no ¬p = lemma where
|
|
|
119 lemma1 : (y : Ordinal) → (y o< x → odef X y → ⊥) ∨ choiced (& X)
|
|
|
120 lemma1 y with ∋-p X (* y)
|
|
|
121 lemma1 y | yes y<X = case2 ( record { a-choice = y ; is-in = ∋oo y<X } )
|
|
|
122 lemma1 y | no ¬y<X = case1 ( λ lt y<X → ¬y<X (d→∋ X y<X) )
|
|
|
123 lemma : ((y : Ordinal) → y o< x → odef X y → ⊥) ∨ choiced (& X)
|
|
|
124 lemma = ∀-imply-or lemma1
|
|
|
125 odef→o< : {X : HOD } → {x : Ordinal } → odef X x → x o< & X
|
|
|
126 odef→o< {X} {x} lt = o<-subst {_} {_} {x} {& X} ( c<→o< ( subst₂ (λ j k → odef j k ) (sym *iso) (sym &iso) lt )) &iso &iso
|
|
|
127 have_to_find : choiced (& X)
|
|
|
128 have_to_find = dont-or (lemma-ord (& X )) ¬¬X∋x where
|
|
|
129 ¬¬X∋x : ¬ ((x : Ordinal) → x o< (& X) → odef X x → ⊥)
|
|
|
130 ¬¬X∋x nn = not record {
|
|
|
131 eq→ = λ {x} lt → ⊥-elim (nn x (odef→o< lt) lt)
|
|
|
132 ; eq← = λ {x} lt → ⊥-elim ( ¬x<0 lt )
|
|
|
133 }
|
|
|
134
|
|
|
135 --
|
|
|
136 -- axiom regurality from ε-induction (using axiom of choice above)
|
|
|
137 --
|
|
|
138 -- from https://math.stackexchange.com/questions/2973777/is-it-possible-to-prove-regularity-with-transfinite-induction-only
|
|
|
139 --
|
|
|
140 record Minimal (x : HOD) : Set (suc n) where
|
|
|
141 field
|
|
|
142 min : HOD
|
|
|
143 x∋min : x ∋ min
|
|
|
144 min-empty : (y : HOD ) → ¬ ( min ∋ y) ∧ (x ∋ y)
|
|
|
145 open Minimal
|
|
|
146 open _∧_
|
|
|
147 induction : {x : HOD} → ({y : HOD} → x ∋ y → (u : HOD ) → (u∋x : u ∋ y) → Minimal u )
|
|
|
148 → (u : HOD ) → (u∋x : u ∋ x) → Minimal u
|
|
|
149 induction {x} prev u u∋x with p∨¬p ((y : Ordinal ) → ¬ (odef x y) ∧ (odef u y))
|
|
|
150 ... | case1 P =
|
|
|
151 record { min = x
|
|
|
152 ; x∋min = u∋x
|
|
|
153 ; min-empty = λ y → P (& y)
|
|
|
154 }
|
|
|
155 ... | case2 NP = min2 where
|
|
|
156 p : HOD
|
|
|
157 p = record { od = record { def = λ y1 → odef x y1 ∧ odef u y1 } ; odmax = omin (odmax x) (odmax u) ; <odmax = lemma } where
|
|
|
158 lemma : {y : Ordinal} → OD.def (od x) y ∧ OD.def (od u) y → y o< omin (odmax x) (odmax u)
|
|
|
159 lemma {y} lt = min1 (<odmax x (proj1 lt)) (<odmax u (proj2 lt))
|
|
|
160 np : ¬ (p =h= od∅)
|
|
|
161 np p∅ = NP (λ y p∋y → ∅< {p} {_} (d→∋ p p∋y) p∅ )
|
|
|
162 y1choice : choiced (& p)
|
|
|
163 y1choice = choice-func p np
|
|
|
164 y1 : HOD
|
|
|
165 y1 = * (a-choice y1choice)
|
|
|
166 y1prop : (x ∋ y1) ∧ (u ∋ y1)
|
|
|
167 y1prop = oo∋ (is-in y1choice)
|
|
|
168 min2 : Minimal u
|
|
|
169 min2 = prev (proj1 y1prop) u (proj2 y1prop)
|
|
|
170 Min2 : (x : HOD) → (u : HOD ) → (u∋x : u ∋ x) → Minimal u
|
|
|
171 Min2 x u u∋x = (ε-induction {λ y → (u : HOD ) → (u∋x : u ∋ y) → Minimal u } induction x u u∋x )
|
|
|
172 cx : {x : HOD} → ¬ (x =h= od∅ ) → choiced (& x )
|
|
|
173 cx {x} nx = choice-func x nx
|
|
|
174 minimal : (x : HOD ) → ¬ (x =h= od∅ ) → HOD
|
|
|
175 minimal x ne = min (Min2 (* (a-choice (cx {x} ne) )) x ( oo∋ (is-in (cx ne))) )
|
|
|
176 x∋minimal : (x : HOD ) → ( ne : ¬ (x =h= od∅ ) ) → odef x ( & ( minimal x ne ) )
|
|
|
177 x∋minimal x ne = x∋min (Min2 (* (a-choice (cx {x} ne) )) x ( oo∋ (is-in (cx ne))) )
|
|
|
178 minimal-1 : (x : HOD ) → ( ne : ¬ (x =h= od∅ ) ) → (y : HOD ) → ¬ ( odef (minimal x ne) (& y)) ∧ (odef x (& y) )
|
|
|
179 minimal-1 x ne y = min-empty (Min2 (* (a-choice (cx ne) )) x ( oo∋ (is-in (cx ne)))) y
|
|
|
180
|
|
|
181
|
|
|
182
|
|
|
183
|
