|
431
|
1 {-# OPTIONS --allow-unsolved-metas #-}
|
|
|
2 open import Level
|
|
|
3 open import Ordinals
|
|
|
4 module ODC {n : Level } (O : Ordinals {n} ) where
|
|
|
5
|
|
|
6 open import zf
|
|
|
7 open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ; _⊔_ to _n⊔_ )
|
|
|
8 open import Relation.Binary.PropositionalEquality
|
|
|
9 open import Data.Nat.Properties
|
|
|
10 open import Data.Empty
|
|
|
11 open import Relation.Nullary
|
|
|
12 open import Relation.Binary
|
|
|
13 open import Relation.Binary.Core
|
|
|
14
|
|
|
15 import OrdUtil
|
|
|
16 open import logic
|
|
|
17 open import nat
|
|
|
18 import OD
|
|
|
19 import ODUtil
|
|
|
20
|
|
|
21 open inOrdinal O
|
|
|
22 open OD O
|
|
|
23 open OD.OD
|
|
|
24 open OD._==_
|
|
|
25 open ODAxiom odAxiom
|
|
|
26 open ODUtil O
|
|
|
27
|
|
|
28 open Ordinals.Ordinals O
|
|
|
29 open Ordinals.IsOrdinals isOrdinal
|
|
|
30 open Ordinals.IsNext isNext
|
|
|
31 open OrdUtil O
|
|
|
32
|
|
|
33
|
|
|
34 open HOD
|
|
|
35
|
|
|
36 open _∧_
|
|
|
37
|
|
|
38 postulate
|
|
|
39 -- mimimul and x∋minimal is an Axiom of choice
|
|
|
40 minimal : (x : HOD ) → ¬ (x =h= od∅ )→ HOD
|
|
|
41 -- this should be ¬ (x =h= od∅ )→ ∃ ox → x ∋ Ord ox ( minimum of x )
|
|
|
42 x∋minimal : (x : HOD ) → ( ne : ¬ (x =h= od∅ ) ) → odef x ( & ( minimal x ne ) )
|
|
467
|
43 -- minimality (proved by ε-induction with LEM)
|
|
431
|
44 minimal-1 : (x : HOD ) → ( ne : ¬ (x =h= od∅ ) ) → (y : HOD ) → ¬ ( odef (minimal x ne) (& y)) ∧ (odef x (& y) )
|
|
|
45
|
|
|
46
|
|
|
47 --
|
|
|
48 -- Axiom of choice in intutionistic logic implies the exclude middle
|
|
|
49 -- https://plato.stanford.edu/entries/axiom-choice/#AxiChoLog
|
|
|
50 --
|
|
|
51
|
|
|
52 pred-od : ( p : Set n ) → HOD
|
|
|
53 pred-od p = record { od = record { def = λ x → (x ≡ o∅) ∧ p } ;
|
|
|
54 odmax = osuc o∅; <odmax = λ x → subst (λ k → k o< osuc o∅) (sym (proj1 x)) <-osuc }
|
|
|
55
|
|
|
56 ppp : { p : Set n } { a : HOD } → pred-od p ∋ a → p
|
|
|
57 ppp {p} {a} d = proj2 d
|
|
|
58
|
|
|
59 p∨¬p : ( p : Set n ) → p ∨ ( ¬ p ) -- assuming axiom of choice
|
|
|
60 p∨¬p p with is-o∅ ( & (pred-od p ))
|
|
|
61 p∨¬p p | yes eq = case2 (¬p eq) where
|
|
|
62 ps = pred-od p
|
|
|
63 eqo∅ : ps =h= od∅ → & ps ≡ o∅
|
|
|
64 eqo∅ eq = subst (λ k → & ps ≡ k) ord-od∅ ( cong (λ k → & k ) (==→o≡ eq))
|
|
|
65 lemma : ps =h= od∅ → p → ⊥
|
|
|
66 lemma eq p0 = ¬x<0 {& ps} (eq→ eq record { proj1 = eqo∅ eq ; proj2 = p0 } )
|
|
|
67 ¬p : (& ps ≡ o∅) → p → ⊥
|
|
|
68 ¬p eq = lemma ( subst₂ (λ j k → j =h= k ) *iso o∅≡od∅ ( o≡→== eq ))
|
|
|
69 p∨¬p p | no ¬p = case1 (ppp {p} {minimal ps (λ eq → ¬p (eqo∅ eq))} lemma) where
|
|
|
70 ps = pred-od p
|
|
|
71 eqo∅ : ps =h= od∅ → & ps ≡ o∅
|
|
|
72 eqo∅ eq = subst (λ k → & ps ≡ k) ord-od∅ ( cong (λ k → & k ) (==→o≡ eq))
|
|
|
73 lemma : ps ∋ minimal ps (λ eq → ¬p (eqo∅ eq))
|
|
|
74 lemma = x∋minimal ps (λ eq → ¬p (eqo∅ eq))
|
|
|
75
|
|
|
76 decp : ( p : Set n ) → Dec p -- assuming axiom of choice
|
|
|
77 decp p with p∨¬p p
|
|
|
78 decp p | case1 x = yes x
|
|
|
79 decp p | case2 x = no x
|
|
|
80
|
|
|
81 ∋-p : (A x : HOD ) → Dec ( A ∋ x )
|
|
|
82 ∋-p A x with p∨¬p ( A ∋ x ) -- LEM
|
|
|
83 ∋-p A x | case1 t = yes t
|
|
|
84 ∋-p A x | case2 t = no (λ x → t x)
|
|
|
85
|
|
|
86 double-neg-eilm : {A : Set n} → ¬ ¬ A → A -- we don't have this in intutionistic logic
|
|
|
87 double-neg-eilm {A} notnot with decp A -- assuming axiom of choice
|
|
|
88 ... | yes p = p
|
|
|
89 ... | no ¬p = ⊥-elim ( notnot ¬p )
|
|
|
90
|
|
|
91 open _⊆_
|
|
|
92
|
|
|
93 power→⊆ : ( A t : HOD) → Power A ∋ t → t ⊆ A
|
|
|
94 power→⊆ A t PA∋t = record { incl = λ {x} t∋x → double-neg-eilm (t1 t∋x) } where
|
|
|
95 t1 : {x : HOD } → t ∋ x → ¬ ¬ (A ∋ x)
|
|
|
96 t1 = power→ A t PA∋t
|
|
|
97
|
|
447
|
98 power-∩ : { A x y : HOD } → Power A ∋ x → Power A ∋ y → Power A ∋ ( x ∩ y )
|
|
|
99 power-∩ {A} {x} {y} ax ay = power← A (x ∩ y) p01 where
|
|
|
100 p01 : {z : HOD} → (x ∩ y) ∋ z → A ∋ z
|
|
|
101 p01 {z} xyz = double-neg-eilm ( power→ A x ax (proj1 xyz ))
|
|
|
102
|
|
431
|
103 OrdP : ( x : Ordinal ) ( y : HOD ) → Dec ( Ord x ∋ y )
|
|
|
104 OrdP x y with trio< x (& y)
|
|
|
105 OrdP x y | tri< a ¬b ¬c = no ¬c
|
|
|
106 OrdP x y | tri≈ ¬a refl ¬c = no ( o<¬≡ refl )
|
|
|
107 OrdP x y | tri> ¬a ¬b c = yes c
|
|
|
108
|
|
|
109 open import zfc
|
|
|
110
|
|
|
111 HOD→ZFC : ZFC
|
|
|
112 HOD→ZFC = record {
|
|
|
113 ZFSet = HOD
|
|
|
114 ; _∋_ = _∋_
|
|
|
115 ; _≈_ = _=h=_
|
|
|
116 ; ∅ = od∅
|
|
|
117 ; Select = Select
|
|
|
118 ; isZFC = isZFC
|
|
|
119 } where
|
|
|
120 -- infixr 200 _∈_
|
|
|
121 -- infixr 230 _∩_ _∪_
|
|
|
122 isZFC : IsZFC (HOD ) _∋_ _=h=_ od∅ Select
|
|
|
123 isZFC = record {
|
|
|
124 choice-func = choice-func ;
|
|
|
125 choice = choice
|
|
|
126 } where
|
|
|
127 -- Axiom of choice ( is equivalent to the existence of minimal in our case )
|
|
|
128 -- ∀ X [ ∅ ∉ X → (∃ f : X → ⋃ X ) → ∀ A ∈ X ( f ( A ) ∈ A ) ]
|
|
|
129 choice-func : (X : HOD ) → {x : HOD } → ¬ ( x =h= od∅ ) → ( X ∋ x ) → HOD
|
|
|
130 choice-func X {x} not X∋x = minimal x not
|
|
|
131 choice : (X : HOD ) → {A : HOD } → ( X∋A : X ∋ A ) → (not : ¬ ( A =h= od∅ )) → A ∋ choice-func X not X∋A
|
|
|
132 choice X {A} X∋A not = x∋minimal A not
|
|
|
133
|
