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

comparison LEMC.agda @ 277:d9d3654baee1

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
seperate choice from LEM
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 09 May 2020 09:38:21 +0900
parents ODC.agda@6f10c47e4e7a
children 197e0b3d39dc
comparison
equal deleted inserted replaced
276:6f10c47e4e7a 277:d9d3654baee1
1 open import Level
2 open import Ordinals
3 open import logic
4 open import Relation.Nullary
5 module LEMC {n : Level } (O : Ordinals {n} ) (p∨¬p : ( p : Set (suc n)) → p ∨ ( ¬ p )) where
6
7 open import zf
8 open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ; _⊔_ to _n⊔_ )
9 open import Relation.Binary.PropositionalEquality
10 open import Data.Nat.Properties
11 open import Data.Empty
12 open import Relation.Binary
13 open import Relation.Binary.Core
14
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 open import zfc
25
26 --- With assuption of OD is ordered, p ∨ ( ¬ p ) <=> axiom of choice
27 ---
28 record choiced ( X : OD) : Set (suc n) where
29 field
30 a-choice : OD
31 is-in : X ∋ a-choice
32
33 open choiced
34
35 OD→ZFC : ZFC
36 OD→ZFC = record {
37 ZFSet = OD
38 ; _∋_ = _∋_
39 ; _≈_ = _==_
40 ; ∅ = od∅
41 ; Select = Select
42 ; isZFC = isZFC
43 } where
44 -- infixr 200 _∈_
45 -- infixr 230 _∩_ _∪_
46 isZFC : IsZFC (OD ) _∋_ _==_ od∅ Select
47 isZFC = record {
48 choice-func = λ A {X} not A∋X → a-choice (choice-func X not );
49 choice = λ A {X} A∋X not → is-in (choice-func X not)
50 } where
51 choice-func : (X : OD ) → ¬ ( X == od∅ ) → choiced X
52 choice-func X not = have_to_find where
53 ψ : ( ox : Ordinal ) → Set (suc n)
54 ψ ox = (( x : Ordinal ) → x o< ox → ( ¬ def X x )) ∨ choiced X
55 lemma-ord : ( ox : Ordinal ) → ψ ox
56 lemma-ord ox = TransFinite {ψ} induction ox where
57 ∋-p : (A x : OD ) → Dec ( A ∋ x )
58 ∋-p A x with p∨¬p (Lift (suc n) ( A ∋ x )) -- LEM
59 ∋-p A x | case1 (lift t) = yes t
60 ∋-p A x | case2 t = no (λ x → t (lift x ))
61 ∀-imply-or : {A : Ordinal → Set n } {B : Set (suc n) }
62 → ((x : Ordinal ) → A x ∨ B) → ((x : Ordinal ) → A x) ∨ B
63 ∀-imply-or {A} {B} ∀AB with p∨¬p (Lift ( suc n ) ((x : Ordinal ) → A x)) -- LEM
64 ∀-imply-or {A} {B} ∀AB | case1 (lift t) = case1 t
65 ∀-imply-or {A} {B} ∀AB | case2 x = case2 (lemma (λ not → x (lift not ))) where
66 lemma : ¬ ((x : Ordinal ) → A x) → B
67 lemma not with p∨¬p B
68 lemma not | case1 b = b
69 lemma not | case2 ¬b = ⊥-elim (not (λ x → dont-orb (∀AB x) ¬b ))
70 induction : (x : Ordinal) → ((y : Ordinal) → y o< x → ψ y) → ψ x
71 induction x prev with ∋-p X ( ord→od x)
72 ... | yes p = case2 ( record { a-choice = ord→od x ; is-in = p } )
73 ... | no ¬p = lemma where
74 lemma1 : (y : Ordinal) → (y o< x → def X y → ⊥) ∨ choiced X
75 lemma1 y with ∋-p X (ord→od y)
76 lemma1 y | yes y<X = case2 ( record { a-choice = ord→od y ; is-in = y<X } )
77 lemma1 y | no ¬y<X = case1 ( λ lt y<X → ¬y<X (subst (λ k → def X k ) (sym diso) y<X ) )
78 lemma : ((y : Ordinals.ord O) → (O Ordinals.o< y) x → def X y → ⊥) ∨ choiced X
79 lemma = ∀-imply-or lemma1
80 have_to_find : choiced X
81 have_to_find = dont-or (lemma-ord (od→ord X )) ¬¬X∋x where
82 ¬¬X∋x : ¬ ((x : Ordinal) → x o< (od→ord X) → def X x → ⊥)
83 ¬¬X∋x nn = not record {
84 eq→ = λ {x} lt → ⊥-elim (nn x (def→o< lt) lt)
85 ; eq← = λ {x} lt → ⊥-elim ( ¬x<0 lt )
86 }
87