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

comparison LEMC.agda @ 330:0faa7120e4b5

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 15:49:00 +0900
parents 5de8905a5a2b
children 12071f79f3cf
comparison
equal deleted inserted replaced
329:5544f4921a44 330:0faa7120e4b5
21 open OD._==_ 21 open OD._==_
22 open ODAxiom odAxiom 22 open ODAxiom odAxiom
23 23
24 open import zfc 24 open import zfc
25 25
26 --- With assuption of OD is ordered, p ∨ ( ¬ p ) <=> axiom of choice 26 --- With assuption of HOD is ordered, p ∨ ( ¬ p ) <=> axiom of choice
27 --- 27 ---
28 record choiced ( X : OD) : Set (suc n) where 28 record choiced ( X : HOD) : Set (suc n) where
29 field 29 field
30 a-choice : OD 30 a-choice : HOD
31 is-in : X ∋ a-choice 31 is-in : X ∋ a-choice
32
33 open HOD
34 _=h=_ : (x y : HOD) → Set n
35 x =h= y = od x == od y
32 36
33 open choiced 37 open choiced
34 38
35 OD→ZFC : ZFC 39 OD→ZFC : ZFC
36 OD→ZFC = record { 40 OD→ZFC = record {
37 ZFSet = OD 41 ZFSet = HOD
38 ; _∋_ = _∋_ 42 ; _∋_ = _∋_
39 ; _≈_ = _==_ 43 ; _≈_ = _=h=_
40 ; ∅ = od∅ 44 ; ∅ = od∅
41 ; Select = Select 45 ; Select = Select
42 ; isZFC = isZFC 46 ; isZFC = isZFC
43 } where 47 } where
44 -- infixr 200 _∈_ 48 -- infixr 200 _∈_
45 -- infixr 230 _∩_ _∪_ 49 -- infixr 230 _∩_ _∪_
46 isZFC : IsZFC (OD ) _∋_ _==_ od∅ Select 50 isZFC : IsZFC (HOD ) _∋_ _=h=_ od∅ Select
47 isZFC = record { 51 isZFC = record {
48 choice-func = λ A {X} not A∋X → a-choice (choice-func X not ); 52 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) 53 choice = λ A {X} A∋X not → is-in (choice-func X not)
50 } where 54 } where
51 choice-func : (X : OD ) → ¬ ( X == od∅ ) → choiced X 55 choice-func : (X : HOD ) → ¬ ( X =h= od∅ ) → choiced X
52 choice-func X not = have_to_find where 56 choice-func X not = have_to_find where
53 ψ : ( ox : Ordinal ) → Set (suc n) 57 ψ : ( ox : Ordinal ) → Set (suc n)
54 ψ ox = (( x : Ordinal ) → x o< ox → ( ¬ def X x )) ∨ choiced X 58 ψ ox = (( x : Ordinal ) → x o< ox → ( ¬ odef X x )) ∨ choiced X
55 lemma-ord : ( ox : Ordinal ) → ψ ox 59 lemma-ord : ( ox : Ordinal ) → ψ ox
56 lemma-ord ox = TransFinite {ψ} induction ox where 60 lemma-ord ox = TransFinite1 {ψ} induction ox where
57 ∋-p : (A x : OD ) → Dec ( A ∋ x ) 61 ∋-p : (A x : HOD ) → Dec ( A ∋ x )
58 ∋-p A x with p∨¬p (Lift (suc n) ( A ∋ x )) -- LEM 62 ∋-p A x with p∨¬p (Lift (suc n) ( A ∋ x )) -- LEM
59 ∋-p A x | case1 (lift t) = yes t 63 ∋-p A x | case1 (lift t) = yes t
60 ∋-p A x | case2 t = no (λ x → t (lift x )) 64 ∋-p A x | case2 t = no (λ x → t (lift x ))
61 ∀-imply-or : {A : Ordinal → Set n } {B : Set (suc n) } 65 ∀-imply-or : {A : Ordinal → Set n } {B : Set (suc n) }
62 → ((x : Ordinal ) → A x ∨ B) → ((x : Ordinal ) → A x) ∨ B 66 → ((x : Ordinal ) → A x ∨ B) → ((x : Ordinal ) → A x) ∨ B
69 lemma not | case2 ¬b = ⊥-elim (not (λ x → dont-orb (∀AB x) ¬b )) 73 lemma not | case2 ¬b = ⊥-elim (not (λ x → dont-orb (∀AB x) ¬b ))
70 induction : (x : Ordinal) → ((y : Ordinal) → y o< x → ψ y) → ψ x 74 induction : (x : Ordinal) → ((y : Ordinal) → y o< x → ψ y) → ψ x
71 induction x prev with ∋-p X ( ord→od x) 75 induction x prev with ∋-p X ( ord→od x)
72 ... | yes p = case2 ( record { a-choice = ord→od x ; is-in = p } ) 76 ... | yes p = case2 ( record { a-choice = ord→od x ; is-in = p } )
73 ... | no ¬p = lemma where 77 ... | no ¬p = lemma where
74 lemma1 : (y : Ordinal) → (y o< x → def X y → ⊥) ∨ choiced X 78 lemma1 : (y : Ordinal) → (y o< x → odef X y → ⊥) ∨ choiced X
75 lemma1 y with ∋-p X (ord→od y) 79 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 } ) 80 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 ) ) 81 lemma1 y | no ¬y<X = case1 ( λ lt y<X → ¬y<X (subst (λ k → odef X k ) (sym diso) y<X ) )
78 lemma : ((y : Ordinals.ord O) → (O Ordinals.o< y) x → def X y → ⊥) ∨ choiced X 82 lemma : ((y : Ordinals.ord O) → (O Ordinals.o< y) x → odef X y → ⊥) ∨ choiced X
79 lemma = ∀-imply-or lemma1 83 lemma = ∀-imply-or lemma1
80 have_to_find : choiced X 84 have_to_find : choiced X
81 have_to_find = dont-or (lemma-ord (od→ord X )) ¬¬X∋x where 85 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 → ⊥) 86 ¬¬X∋x : ¬ ((x : Ordinal) → x o< (od→ord X) → odef X x → ⊥)
83 ¬¬X∋x nn = not record { 87 ¬¬X∋x nn = not record {
84 eq→ = λ {x} lt → ⊥-elim (nn x (def→o< lt) lt) 88 eq→ = λ {x} lt → ⊥-elim (nn x (odef→o< lt) lt)
85 ; eq← = λ {x} lt → ⊥-elim ( ¬x<0 lt ) 89 ; eq← = λ {x} lt → ⊥-elim ( ¬x<0 lt )
86 } 90 }
87 record Minimal (x : OD) : Set (suc n) where 91 record Minimal (x : HOD) : Set (suc n) where
88 field 92 field
89 min : OD 93 min : HOD
90 x∋min : x ∋ min 94 x∋min : x ∋ min
91 min-empty : (y : OD ) → ¬ ( min ∋ y) ∧ (x ∋ y) 95 min-empty : (y : HOD ) → ¬ ( min ∋ y) ∧ (x ∋ y)
92 open Minimal 96 open Minimal
93 open _∧_ 97 open _∧_
94 -- 98 --
95 -- from https://math.stackexchange.com/questions/2973777/is-it-possible-to-prove-regularity-with-transfinite-induction-only 99 -- from https://math.stackexchange.com/questions/2973777/is-it-possible-to-prove-regularity-with-transfinite-induction-only
96 -- 100 --
97 induction : {x : OD} → ({y : OD} → x ∋ y → (u : OD ) → (u∋x : u ∋ y) → Minimal u ) 101 induction : {x : HOD} → ({y : HOD} → x ∋ y → (u : HOD ) → (u∋x : u ∋ y) → Minimal u )
98 → (u : OD ) → (u∋x : u ∋ x) → Minimal u 102 → (u : HOD ) → (u∋x : u ∋ x) → Minimal u
99 induction {x} prev u u∋x with p∨¬p ((y : OD) → ¬ (x ∋ y) ∧ (u ∋ y)) 103 induction {x} prev u u∋x with p∨¬p ((y : HOD) → ¬ (x ∋ y) ∧ (u ∋ y))
100 ... | case1 P = 104 ... | case1 P =
101 record { min = x 105 record { min = x
102 ; x∋min = u∋x 106 ; x∋min = u∋x
103 ; min-empty = P 107 ; min-empty = P
104 } 108 }
105 ... | case2 NP = min2 where 109 ... | case2 NP = min2 where
106 p : OD 110 p : HOD
107 p = record { def = λ y1 → def x y1 ∧ def u y1 } 111 p = record { od = record { def = λ y1 → odef x y1 ∧ odef u y1 } ; odmax = omin (odmax x) (odmax u) ; <odmax = lemma } where
108 np : ¬ (p == od∅) 112 lemma : {y : Ordinal} → OD.def (od x) y ∧ OD.def (od u) y → y o< omin (odmax x) (odmax u)
113 lemma {y} lt = min1 (<odmax x (proj1 lt)) (<odmax u (proj2 lt))
114 np : ¬ (p =h= od∅)
109 np p∅ = NP (λ y p∋y → ∅< p∋y p∅ ) 115 np p∅ = NP (λ y p∋y → ∅< p∋y p∅ )
110 y1choice : choiced p 116 y1choice : choiced p
111 y1choice = choice-func p np 117 y1choice = choice-func p np
112 y1 : OD 118 y1 : HOD
113 y1 = a-choice y1choice 119 y1 = a-choice y1choice
114 y1prop : (x ∋ y1) ∧ (u ∋ y1) 120 y1prop : (x ∋ y1) ∧ (u ∋ y1)
115 y1prop = is-in y1choice 121 y1prop = is-in y1choice
116 min2 : Minimal u 122 min2 : Minimal u
117 min2 = prev (proj1 y1prop) u (proj2 y1prop) 123 min2 = prev (proj1 y1prop) u (proj2 y1prop)
118 Min2 : (x : OD) → (u : OD ) → (u∋x : u ∋ x) → Minimal u 124 Min2 : (x : HOD) → (u : HOD ) → (u∋x : u ∋ x) → Minimal u
119 Min2 x u u∋x = (ε-induction {λ y → (u : OD ) → (u∋x : u ∋ y) → Minimal u } induction x u u∋x ) 125 Min2 x u u∋x = (ε-induction1 {λ y → (u : HOD ) → (u∋x : u ∋ y) → Minimal u } induction x u u∋x )
120 cx : {x : OD} → ¬ (x == od∅ ) → choiced x 126 cx : {x : HOD} → ¬ (x =h= od∅ ) → choiced x
121 cx {x} nx = choice-func x nx 127 cx {x} nx = choice-func x nx
122 minimal : (x : OD ) → ¬ (x == od∅ ) → OD 128 minimal : (x : HOD ) → ¬ (x =h= od∅ ) → HOD
123 minimal x not = min (Min2 (a-choice (cx not) ) x (is-in (cx not))) 129 minimal x not = min (Min2 (a-choice (cx not) ) x (is-in (cx not)))
124 x∋minimal : (x : OD ) → ( ne : ¬ (x == od∅ ) ) → def x ( od→ord ( minimal x ne ) ) 130 x∋minimal : (x : HOD ) → ( ne : ¬ (x =h= od∅ ) ) → odef x ( od→ord ( minimal x ne ) )
125 x∋minimal x ne = x∋min (Min2 (a-choice (cx ne) ) x (is-in (cx ne))) 131 x∋minimal x ne = x∋min (Min2 (a-choice (cx ne) ) x (is-in (cx ne)))
126 minimal-1 : (x : OD ) → ( ne : ¬ (x == od∅ ) ) → (y : OD ) → ¬ ( def (minimal x ne) (od→ord y)) ∧ (def x (od→ord y) ) 132 minimal-1 : (x : HOD ) → ( ne : ¬ (x =h= od∅ ) ) → (y : HOD ) → ¬ ( odef (minimal x ne) (od→ord y)) ∧ (odef x (od→ord y) )
127 minimal-1 x ne y = min-empty (Min2 (a-choice (cx ne) ) x (is-in (cx ne))) y 133 minimal-1 x ne y = min-empty (Min2 (a-choice (cx ne) ) x (is-in (cx ne))) y
128 134
129 135
130 136
131 137