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

comparison src/ODC.agda @ 1120:e086a266c6b7

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
FIP fix
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 03 Jan 2023 09:28:23 +0900
parents 55ab5de1ae02
children 45cd80181a29
comparison
equal deleted inserted replaced
1119:5b0525cb9a5d 1120:e086a266c6b7
2 open import Level 2 open import Level
3 open import Ordinals 3 open import Ordinals
4 module ODC {n : Level } (O : Ordinals {n} ) where 4 module ODC {n : Level } (O : Ordinals {n} ) where
5 5
6 open import zf 6 open import zf
7 open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ; _⊔_ to _n⊔_ ) 7 open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ; _⊔_ to _n⊔_ )
8 open import Relation.Binary.PropositionalEquality 8 open import Relation.Binary.PropositionalEquality
9 open import Data.Nat.Properties 9 open import Data.Nat.Properties
10 open import Data.Empty 10 open import Data.Empty
11 open import Relation.Nullary 11 open import Relation.Nullary
12 open import Relation.Binary 12 open import Relation.Binary
13 open import Relation.Binary.Core 13 open import Relation.Binary.Core
14 14
33 33
34 open HOD 34 open HOD
35 35
36 open _∧_ 36 open _∧_
37 37
38 postulate 38 postulate
39 -- mimimul and x∋minimal is an Axiom of choice 39 -- mimimul and x∋minimal is an Axiom of choice
40 minimal : (x : HOD ) → ¬ (x =h= od∅ )→ HOD 40 minimal : (x : HOD ) → ¬ (x =h= od∅ )→ HOD
41 -- this should be ¬ (x =h= od∅ )→ ∃ ox → x ∋ Ord ox ( minimum of x ) 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 ) ) 42 x∋minimal : (x : HOD ) → ( ne : ¬ (x =h= od∅ ) ) → odef x ( & ( minimal x ne ) )
43 -- minimality (proved by ε-induction with LEM) 43 -- minimality (proved by ε-induction with LEM)
44 minimal-1 : (x : HOD ) → ( ne : ¬ (x =h= od∅ ) ) → (y : HOD ) → ¬ ( odef (minimal x ne) (& y)) ∧ (odef x (& y) ) 44 minimal-1 : (x : HOD ) → ( ne : ¬ (x =h= od∅ ) ) → (y : HOD ) → ¬ ( odef (minimal x ne) (& y)) ∧ (odef x (& y) )
45 45
49 -- https://plato.stanford.edu/entries/axiom-choice/#AxiChoLog 49 -- https://plato.stanford.edu/entries/axiom-choice/#AxiChoLog
50 -- 50 --
51 51
52 pred-od : ( p : Set n ) → HOD 52 pred-od : ( p : Set n ) → HOD
53 pred-od p = record { od = record { def = λ x → (x ≡ o∅) ∧ p } ; 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 } 54 odmax = osuc o∅; <odmax = λ x → subst (λ k → k o< osuc o∅) (sym (proj1 x)) <-osuc }
55 55
56 ppp : { p : Set n } { a : HOD } → pred-od p ∋ a → p 56 ppp : { p : Set n } { a : HOD } → pred-od p ∋ a → p
57 ppp {p} {a} d = proj2 d 57 ppp {p} {a} d = proj2 d
58 58
59 p∨¬p : ( p : Set n ) → p ∨ ( ¬ p ) -- assuming axiom of choice 59 p∨¬p : ( p : Set n ) → p ∨ ( ¬ p ) -- assuming axiom of choice
60 p∨¬p p with is-o∅ ( & (pred-od p )) 60 p∨¬p p with is-o∅ ( & (pred-od p ))
61 p∨¬p p | yes eq = case2 (¬p eq) where 61 p∨¬p p | yes eq = case2 (¬p eq) where
62 ps = pred-od p 62 ps = pred-od p
63 eqo∅ : ps =h= od∅ → & ps ≡ o∅ 63 eqo∅ : ps =h= od∅ → & ps ≡ o∅
64 eqo∅ eq = subst (λ k → & ps ≡ k) ord-od∅ ( cong (λ k → & k ) (==→o≡ eq)) 64 eqo∅ eq = subst (λ k → & ps ≡ k) ord-od∅ ( cong (λ k → & k ) (==→o≡ eq))
65 lemma : ps =h= od∅ → p → ⊥ 65 lemma : ps =h= od∅ → p → ⊥
66 lemma eq p0 = ¬x<0 {& ps} (eq→ eq record { proj1 = eqo∅ eq ; proj2 = p0 } ) 66 lemma eq p0 = ¬x<0 {& ps} (eq→ eq record { proj1 = eqo∅ eq ; proj2 = p0 } )
67 ¬p : (& ps ≡ o∅) → p → ⊥ 67 ¬p : (& ps ≡ o∅) → p → ⊥
68 ¬p eq = lemma ( subst₂ (λ j k → j =h= k ) *iso o∅≡od∅ ( o≡→== eq )) 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 69 p∨¬p p | no ¬p = case1 (ppp {p} {minimal ps (λ eq → ¬p (eqo∅ eq))} lemma) where
70 ps = pred-od p 70 ps = pred-od p
71 eqo∅ : ps =h= od∅ → & ps ≡ o∅ 71 eqo∅ : ps =h= od∅ → & ps ≡ o∅
72 eqo∅ eq = subst (λ k → & ps ≡ k) ord-od∅ ( cong (λ k → & k ) (==→o≡ eq)) 72 eqo∅ eq = subst (λ k → & ps ≡ k) ord-od∅ ( cong (λ k → & k ) (==→o≡ eq))
73 lemma : ps ∋ minimal ps (λ eq → ¬p (eqo∅ eq)) 73 lemma : ps ∋ minimal ps (λ eq → ¬p (eqo∅ eq))
74 lemma = x∋minimal ps (λ eq → ¬p (eqo∅ eq)) 74 lemma = x∋minimal ps (λ eq → ¬p (eqo∅ eq))
75 75
76 decp : ( p : Set n ) → Dec p -- assuming axiom of choice 76 decp : ( p : Set n ) → Dec p -- assuming axiom of choice
77 decp p with p∨¬p p 77 decp p with p∨¬p p
78 decp p | case1 x = yes x 78 decp p | case1 x = yes x
79 decp p | case2 x = no x 79 decp p | case2 x = no x
80 80
81 ∋-p : (A x : HOD ) → Dec ( A ∋ x ) 81 ∋-p : (A x : HOD ) → Dec ( A ∋ x )
82 ∋-p A x with p∨¬p ( A ∋ x ) -- LEM 82 ∋-p A x with p∨¬p ( A ∋ x ) -- LEM
83 ∋-p A x | case1 t = yes t 83 ∋-p A x | case1 t = yes t
84 ∋-p A x | case2 t = no (λ x → t x) 84 ∋-p A x | case2 t = no (λ x → t x)
85 85
86 double-neg-eilm : {A : Set n} → ¬ ¬ A → A -- we don't have this in intutionistic logic 86 double-neg-elim : {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 87 double-neg-elim {A} notnot with decp A -- assuming axiom of choice
88 ... | yes p = p 88 ... | yes p = p
89 ... | no ¬p = ⊥-elim ( notnot ¬p ) 89 ... | no ¬p = ⊥-elim ( notnot ¬p )
90 90
91 or-exclude : {A B : Set n} → A ∨ B → A ∨ ( (¬ A) ∧ B ) 91 or-exclude : {A B : Set n} → A ∨ B → A ∨ ( (¬ A) ∧ B )
92 or-exclude {A} {B} ab with p∨¬p A 92 or-exclude {A} {B} ab with p∨¬p A
93 or-exclude {A} {B} (case1 a) | case1 a0 = case1 a 93 or-exclude {A} {B} (case1 a) | case1 a0 = case1 a
94 or-exclude {A} {B} (case1 a) | case2 ¬a = ⊥-elim ( ¬a a ) 94 or-exclude {A} {B} (case1 a) | case2 ¬a = ⊥-elim ( ¬a a )
95 or-exclude {A} {B} (case2 b) | case1 a = case1 a 95 or-exclude {A} {B} (case2 b) | case1 a = case1 a
96 or-exclude {A} {B} (case2 b) | case2 ¬a = case2 ⟪ ¬a , b ⟫ 96 or-exclude {A} {B} (case2 b) | case2 ¬a = case2 ⟪ ¬a , b ⟫
97 97
98 -- record By-contradiction (A : Set n) (B : A → Set n) : Set (suc n) where
99 -- field
100 -- a : A
101 -- b : B a
102 --
103 -- by-contradiction : {A : Set n} {B : A → Set n} → ¬ ( (a : A ) → ¬ B a ) → By-contradiction A B
104 -- by-contradiction {A} {B} not with p∨¬p A
105 -- ... | case2 ¬a = ⊥-elim (not (λ a → ⊥-elim (¬a a )))
106 -- ... | case1 a with p∨¬p (B a)
107 -- ... | case1 b = record { a = a ; b = b }
108 -- ... | case2 ¬b = ⊥-elim ( not ( λ a b → ⊥-elim ( ¬b ? )))
109 --
98 power→⊆ : ( A t : HOD) → Power A ∋ t → t ⊆ A 110 power→⊆ : ( A t : HOD) → Power A ∋ t → t ⊆ A
99 power→⊆ A t PA∋t tx = subst (λ k → odef A k ) &iso ( power→ A t PA∋t (subst (λ k → odef t k) (sym &iso) tx ) ) 111 power→⊆ A t PA∋t tx = subst (λ k → odef A k ) &iso ( power→ A t PA∋t (subst (λ k → odef t k) (sym &iso) tx ) )
100 112
101 power-∩ : { A x y : HOD } → Power A ∋ x → Power A ∋ y → Power A ∋ ( x ∩ y ) 113 power-∩ : { A x y : HOD } → Power A ∋ x → Power A ∋ y → Power A ∋ ( x ∩ y )
102 power-∩ {A} {x} {y} ax ay = power← A (x ∩ y) p01 where 114 power-∩ {A} {x} {y} ax ay = power← A (x ∩ y) p01 where
110 OrdP x y | tri> ¬a ¬b c = yes c 122 OrdP x y | tri> ¬a ¬b c = yes c
111 123
112 open import zfc 124 open import zfc
113 125
114 HOD→ZFC : ZFC 126 HOD→ZFC : ZFC
115 HOD→ZFC = record { 127 HOD→ZFC = record {
116 ZFSet = HOD 128 ZFSet = HOD
117 ; _∋_ = _∋_ 129 ; _∋_ = _∋_
118 ; _≈_ = _=h=_ 130 ; _≈_ = _=h=_
119 ; ∅ = od∅ 131 ; ∅ = od∅
120 ; Select = Select 132 ; Select = Select
121 ; isZFC = isZFC 133 ; isZFC = isZFC
122 } where 134 } where
123 -- infixr 200 _∈_ 135 -- infixr 200 _∈_
126 isZFC = record { 138 isZFC = record {
127 choice-func = choice-func ; 139 choice-func = choice-func ;
128 choice = choice 140 choice = choice
129 } where 141 } where
130 -- Axiom of choice ( is equivalent to the existence of minimal in our case ) 142 -- Axiom of choice ( is equivalent to the existence of minimal in our case )
131 -- ∀ X [ ∅ ∉ X → (∃ f : X → ⋃ X ) → ∀ A ∈ X ( f ( A ) ∈ A ) ] 143 -- ∀ X [ ∅ ∉ X → (∃ f : X → ⋃ X ) → ∀ A ∈ X ( f ( A ) ∈ A ) ]
132 choice-func : (X : HOD ) → {x : HOD } → ¬ ( x =h= od∅ ) → ( X ∋ x ) → HOD 144 choice-func : (X : HOD ) → {x : HOD } → ¬ ( x =h= od∅ ) → ( X ∋ x ) → HOD
133 choice-func X {x} not X∋x = minimal x not 145 choice-func X {x} not X∋x = minimal x not
134 choice : (X : HOD ) → {A : HOD } → ( X∋A : X ∋ A ) → (not : ¬ ( A =h= od∅ )) → A ∋ choice-func X not X∋A 146 choice : (X : HOD ) → {A : HOD } → ( X∋A : X ∋ A ) → (not : ¬ ( A =h= od∅ )) → A ∋ choice-func X not X∋A
135 choice X {A} X∋A not = x∋minimal A not 147 choice X {A} X∋A not = x∋minimal A not
136 148