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

comparison ODC.agda @ 329:5544f4921a44

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 Sun, 05 Jul 2020 12:32:09 +0900
parents 197e0b3d39dc
children 0faa7120e4b5
comparison
equal deleted inserted replaced
328:72f3e3b44c27 329:5544f4921a44
19 open OD O 19 open OD O
20 open OD.OD 20 open OD.OD
21 open OD._==_ 21 open OD._==_
22 open ODAxiom odAxiom 22 open ODAxiom odAxiom
23 23
24 open HOD
25
26 _=h=_ : (x y : HOD) → Set n
27 x =h= y = od x == od y
28
24 postulate 29 postulate
25 -- mimimul and x∋minimal is an Axiom of choice 30 -- mimimul and x∋minimal is an Axiom of choice
26 minimal : (x : OD ) → ¬ (x == od∅ )→ OD 31 minimal : (x : HOD ) → ¬ (x =h= od∅ )→ HOD
27 -- this should be ¬ (x == od∅ )→ ∃ ox → x ∋ Ord ox ( minimum of x ) 32 -- this should be ¬ (x =h= od∅ )→ ∃ ox → x ∋ Ord ox ( minimum of x )
28 x∋minimal : (x : OD ) → ( ne : ¬ (x == od∅ ) ) → def x ( od→ord ( minimal x ne ) ) 33 x∋minimal : (x : HOD ) → ( ne : ¬ (x =h= od∅ ) ) → odef x ( od→ord ( minimal x ne ) )
29 -- minimality (may proved by ε-induction ) 34 -- minimality (may proved by ε-induction )
30 minimal-1 : (x : OD ) → ( ne : ¬ (x == od∅ ) ) → (y : OD ) → ¬ ( def (minimal x ne) (od→ord y)) ∧ (def x (od→ord y) ) 35 minimal-1 : (x : HOD ) → ( ne : ¬ (x =h= od∅ ) ) → (y : HOD ) → ¬ ( odef (minimal x ne) (od→ord y)) ∧ (odef x (od→ord y) )
31 36
32 37
33 -- 38 --
34 -- Axiom of choice in intutionistic logic implies the exclude middle 39 -- Axiom of choice in intutionistic logic implies the exclude middle
35 -- https://plato.stanford.edu/entries/axiom-choice/#AxiChoLog 40 -- https://plato.stanford.edu/entries/axiom-choice/#AxiChoLog
36 -- 41 --
37 42
38 ppp : { p : Set n } { a : OD } → record { def = λ x → p } ∋ a → p 43 -- ppp : { p : Set n } { a : HOD } → record { def = λ x → p } ∋ a → p
39 ppp {p} {a} d = d 44 -- ppp {p} {a} d = d
40 45
41 p∨¬p : ( p : Set n ) → p ∨ ( ¬ p ) -- assuming axiom of choice 46 -- p∨¬p : ( p : Set n ) → p ∨ ( ¬ p ) -- assuming axiom of choice
42 p∨¬p p with is-o∅ ( od→ord ( record { def = λ x → p } )) 47 -- p∨¬p p with is-o∅ ( od→ord ( record { odef = λ x → p } ))
43 p∨¬p p | yes eq = case2 (¬p eq) where 48 -- p∨¬p p | yes eq = case2 (¬p eq) where
44 ps = record { def = λ x → p } 49 -- ps = record { odef = λ x → p }
45 lemma : ps == od∅ → p → ⊥ 50 -- lemma : ps =h= od∅ → p → ⊥
46 lemma eq p0 = ¬x<0 {od→ord ps} (eq→ eq p0 ) 51 -- lemma eq p0 = ¬x<0 {od→ord ps} (eq→ eq p0 )
47 ¬p : (od→ord ps ≡ o∅) → p → ⊥ 52 -- ¬p : (od→ord ps ≡ o∅) → p → ⊥
48 ¬p eq = lemma ( subst₂ (λ j k → j == k ) oiso o∅≡od∅ ( o≡→== eq )) 53 -- ¬p eq = lemma ( subst₂ (λ j k → j =h= k ) oiso o∅≡od∅ ( o≡→== eq ))
49 p∨¬p p | no ¬p = case1 (ppp {p} {minimal ps (λ eq → ¬p (eqo∅ eq))} lemma) where 54 -- p∨¬p p | no ¬p = case1 (ppp {p} {minimal ps (λ eq → ¬p (eqo∅ eq))} lemma) where
50 ps = record { def = λ x → p } 55 -- ps = record { odef = λ x → p }
51 eqo∅ : ps == od∅ → od→ord ps ≡ o∅ 56 -- eqo∅ : ps =h= od∅ → od→ord ps ≡ o∅
52 eqo∅ eq = subst (λ k → od→ord ps ≡ k) ord-od∅ ( cong (λ k → od→ord k ) (==→o≡ eq)) 57 -- eqo∅ eq = subst (λ k → od→ord ps ≡ k) ord-od∅ ( cong (λ k → od→ord k ) (==→o≡ eq))
53 lemma : ps ∋ minimal ps (λ eq → ¬p (eqo∅ eq)) 58 -- lemma : ps ∋ minimal ps (λ eq → ¬p (eqo∅ eq))
54 lemma = x∋minimal ps (λ eq → ¬p (eqo∅ eq)) 59 -- lemma = x∋minimal ps (λ eq → ¬p (eqo∅ eq))
60
61 postulate
62 p∨¬p : ( p : Set n ) → p ∨ ( ¬ p ) -- assuming axiom of choice
55 63
56 decp : ( p : Set n ) → Dec p -- assuming axiom of choice 64 decp : ( p : Set n ) → Dec p -- assuming axiom of choice
57 decp p with p∨¬p p 65 decp p with p∨¬p p
58 decp p | case1 x = yes x 66 decp p | case1 x = yes x
59 decp p | case2 x = no x 67 decp p | case2 x = no x
61 double-neg-eilm : {A : Set n} → ¬ ¬ A → A -- we don't have this in intutionistic logic 69 double-neg-eilm : {A : Set n} → ¬ ¬ A → A -- we don't have this in intutionistic logic
62 double-neg-eilm {A} notnot with decp A -- assuming axiom of choice 70 double-neg-eilm {A} notnot with decp A -- assuming axiom of choice
63 ... | yes p = p 71 ... | yes p = p
64 ... | no ¬p = ⊥-elim ( notnot ¬p ) 72 ... | no ¬p = ⊥-elim ( notnot ¬p )
65 73
66 OrdP : ( x : Ordinal ) ( y : OD ) → Dec ( Ord x ∋ y ) 74 OrdP : ( x : Ordinal ) ( y : HOD ) → Dec ( Ord x ∋ y )
67 OrdP x y with trio< x (od→ord y) 75 OrdP x y with trio< x (od→ord y)
68 OrdP x y | tri< a ¬b ¬c = no ¬c 76 OrdP x y | tri< a ¬b ¬c = no ¬c
69 OrdP x y | tri≈ ¬a refl ¬c = no ( o<¬≡ refl ) 77 OrdP x y | tri≈ ¬a refl ¬c = no ( o<¬≡ refl )
70 OrdP x y | tri> ¬a ¬b c = yes c 78 OrdP x y | tri> ¬a ¬b c = yes c
71 79
72 open import zfc 80 open import zfc
73 81
74 OD→ZFC : ZFC 82 HOD→ZFC : ZFC
75 OD→ZFC = record { 83 HOD→ZFC = record {
76 ZFSet = OD 84 ZFSet = HOD
77 ; _∋_ = _∋_ 85 ; _∋_ = _∋_
78 ; _≈_ = _==_ 86 ; _≈_ = _=h=_
79 ; ∅ = od∅ 87 ; ∅ = od∅
80 ; Select = Select 88 ; Select = Select
81 ; isZFC = isZFC 89 ; isZFC = isZFC
82 } where 90 } where
83 -- infixr 200 _∈_ 91 -- infixr 200 _∈_
84 -- infixr 230 _∩_ _∪_ 92 -- infixr 230 _∩_ _∪_
85 isZFC : IsZFC (OD ) _∋_ _==_ od∅ Select 93 isZFC : IsZFC (HOD ) _∋_ _=h=_ od∅ Select
86 isZFC = record { 94 isZFC = record {
87 choice-func = choice-func ; 95 choice-func = choice-func ;
88 choice = choice 96 choice = choice
89 } where 97 } where
90 -- Axiom of choice ( is equivalent to the existence of minimal in our case ) 98 -- Axiom of choice ( is equivalent to the existence of minimal in our case )
91 -- ∀ X [ ∅ ∉ X → (∃ f : X → ⋃ X ) → ∀ A ∈ X ( f ( A ) ∈ A ) ] 99 -- ∀ X [ ∅ ∉ X → (∃ f : X → ⋃ X ) → ∀ A ∈ X ( f ( A ) ∈ A ) ]
92 choice-func : (X : OD ) → {x : OD } → ¬ ( x == od∅ ) → ( X ∋ x ) → OD 100 choice-func : (X : HOD ) → {x : HOD } → ¬ ( x =h= od∅ ) → ( X ∋ x ) → HOD
93 choice-func X {x} not X∋x = minimal x not 101 choice-func X {x} not X∋x = minimal x not
94 choice : (X : OD ) → {A : OD } → ( X∋A : X ∋ A ) → (not : ¬ ( A == od∅ )) → A ∋ choice-func X not X∋A 102 choice : (X : HOD ) → {A : HOD } → ( X∋A : X ∋ A ) → (not : ¬ ( A =h= od∅ )) → A ∋ choice-func X not X∋A
95 choice X {A} X∋A not = x∋minimal A not 103 choice X {A} X∋A not = x∋minimal A not
96 104