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

comparison ODC.agda @ 288:4fcac1eebc74 release

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
axiom of choice clean up
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 07 Jun 2020 20:31:30 +0900
parents 197e0b3d39dc
children 5544f4921a44
comparison
equal deleted inserted replaced
256:6e1c60866788 288:4fcac1eebc74
1 open import Level
2 open import Ordinals
3 module ODC {n : Level } (O : Ordinals {n} ) where
4
5 open import zf
6 open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ; _⊔_ to _n⊔_ )
7 open import Relation.Binary.PropositionalEquality
8 open import Data.Nat.Properties
9 open import Data.Empty
10 open import Relation.Nullary
11 open import Relation.Binary
12 open import Relation.Binary.Core
13
14 open import logic
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
24 postulate
25 -- mimimul and x∋minimal is an Axiom of choice
26 minimal : (x : OD ) → ¬ (x == od∅ )→ OD
27 -- this should be ¬ (x == od∅ )→ ∃ ox → x ∋ Ord ox ( minimum of x )
28 x∋minimal : (x : OD ) → ( ne : ¬ (x == od∅ ) ) → def x ( od→ord ( minimal x ne ) )
29 -- 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) )
31
32
33 --
34 -- Axiom of choice in intutionistic logic implies the exclude middle
35 -- https://plato.stanford.edu/entries/axiom-choice/#AxiChoLog
36 --
37
38 ppp : { p : Set n } { a : OD } → record { def = λ x → p } ∋ a → p
39 ppp {p} {a} d = d
40
41 p∨¬p : ( p : Set n ) → p ∨ ( ¬ p ) -- assuming axiom of choice
42 p∨¬p p with is-o∅ ( od→ord ( record { def = λ x → p } ))
43 p∨¬p p | yes eq = case2 (¬p eq) where
44 ps = record { def = λ x → p }
45 lemma : ps == od∅ → p → ⊥
46 lemma eq p0 = ¬x<0 {od→ord ps} (eq→ eq p0 )
47 ¬p : (od→ord ps ≡ o∅) → p → ⊥
48 ¬p eq = lemma ( subst₂ (λ j k → j == k ) oiso o∅≡od∅ ( o≡→== eq ))
49 p∨¬p p | no ¬p = case1 (ppp {p} {minimal ps (λ eq → ¬p (eqo∅ eq))} lemma) where
50 ps = record { def = λ x → p }
51 eqo∅ : ps == od∅ → od→ord ps ≡ o∅
52 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))
54 lemma = x∋minimal ps (λ eq → ¬p (eqo∅ eq))
55
56 decp : ( p : Set n ) → Dec p -- assuming axiom of choice
57 decp p with p∨¬p p
58 decp p | case1 x = yes x
59 decp p | case2 x = no x
60
61 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
63 ... | yes p = p
64 ... | no ¬p = ⊥-elim ( notnot ¬p )
65
66 OrdP : ( x : Ordinal ) ( y : OD ) → Dec ( Ord x ∋ y )
67 OrdP x y with trio< x (od→ord y)
68 OrdP x y | tri< a ¬b ¬c = no ¬c
69 OrdP x y | tri≈ ¬a refl ¬c = no ( o<¬≡ refl )
70 OrdP x y | tri> ¬a ¬b c = yes c
71
72 open import zfc
73
74 OD→ZFC : ZFC
75 OD→ZFC = record {
76 ZFSet = OD
77 ; _∋_ = _∋_
78 ; _≈_ = _==_
79 ; ∅ = od∅
80 ; Select = Select
81 ; isZFC = isZFC
82 } where
83 -- infixr 200 _∈_
84 -- infixr 230 _∩_ _∪_
85 isZFC : IsZFC (OD ) _∋_ _==_ od∅ Select
86 isZFC = record {
87 choice-func = choice-func ;
88 choice = choice
89 } where
90 -- Axiom of choice ( is equivalent to the existence of minimal in our case )
91 -- ∀ X [ ∅ ∉ X → (∃ f : X → ⋃ X ) → ∀ A ∈ X ( f ( A ) ∈ A ) ]
92 choice-func : (X : OD ) → {x : OD } → ¬ ( x == od∅ ) → ( X ∋ x ) → OD
93 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
95 choice X {A} X∋A not = x∋minimal A not
96