Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison LEMC.agda @ 277:d9d3654baee1
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 |