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

comparison src/ODC.agda @ 431:a5f8084b8368

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
reorganiztion for apkg
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 21 Dec 2020 10:23:37 +0900
parents
children 364d738f871d
comparison
equal deleted inserted replaced
430:28c7be8f252c 431:a5f8084b8368
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 ) )
43 -- minimality (may proved by ε-induction with LEM)
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
98 OrdP : ( x : Ordinal ) ( y : HOD ) → Dec ( Ord x ∋ y )
99 OrdP x y with trio< x (& y)
100 OrdP x y | tri< a ¬b ¬c = no ¬c
101 OrdP x y | tri≈ ¬a refl ¬c = no ( o<¬≡ refl )
102 OrdP x y | tri> ¬a ¬b c = yes c
103
104 open import zfc
105
106 HOD→ZFC : ZFC
107 HOD→ZFC = record {
108 ZFSet = HOD
109 ; _∋_ = _∋_
110 ; _≈_ = _=h=_
111 ; ∅ = od∅
112 ; Select = Select
113 ; isZFC = isZFC
114 } where
115 -- infixr 200 _∈_
116 -- infixr 230 _∩_ _∪_
117 isZFC : IsZFC (HOD ) _∋_ _=h=_ od∅ Select
118 isZFC = record {
119 choice-func = choice-func ;
120 choice = choice
121 } where
122 -- Axiom of choice ( is equivalent to the existence of minimal in our case )
123 -- ∀ X [ ∅ ∉ X → (∃ f : X → ⋃ X ) → ∀ A ∈ X ( f ( A ) ∈ A ) ]
124 choice-func : (X : HOD ) → {x : HOD } → ¬ ( x =h= od∅ ) → ( X ∋ x ) → HOD
125 choice-func X {x} not X∋x = minimal x not
126 choice : (X : HOD ) → {A : HOD } → ( X∋A : X ∋ A ) → (not : ¬ ( A =h= od∅ )) → A ∋ choice-func X not X∋A
127 choice X {A} X∋A not = x∋minimal A not
128