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

comparison LEMC.agda @ 424:cc7909f86841

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
remvoe TransFinifte1
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 01 Aug 2020 23:37:10 +0900
parents 44a484f17f26
children
comparison
equal deleted inserted replaced
423:9984cdd88da3 424:cc7909f86841
18 open inOrdinal O 18 open inOrdinal O
19 open OD O 19 open OD O
20 open OD.OD 20 open OD.OD
21 open OD._==_ 21 open OD._==_
22 open ODAxiom odAxiom 22 open ODAxiom odAxiom
23 import OrdUtil
24 import ODUtil
25 open Ordinals.Ordinals O
26 open Ordinals.IsOrdinals isOrdinal
27 open Ordinals.IsNext isNext
28 open OrdUtil O
29 open ODUtil O
23 30
24 open import zfc 31 open import zfc
25 32
26 open HOD 33 open HOD
27 34
87 choice-func : (X : HOD ) → ¬ ( X =h= od∅ ) → choiced (& X) 94 choice-func : (X : HOD ) → ¬ ( X =h= od∅ ) → choiced (& X)
88 choice-func X not = have_to_find where 95 choice-func X not = have_to_find where
89 ψ : ( ox : Ordinal ) → Set n 96 ψ : ( ox : Ordinal ) → Set n
90 ψ ox = (( x : Ordinal ) → x o< ox → ( ¬ odef X x )) ∨ choiced (& X) 97 ψ ox = (( x : Ordinal ) → x o< ox → ( ¬ odef X x )) ∨ choiced (& X)
91 lemma-ord : ( ox : Ordinal ) → ψ ox 98 lemma-ord : ( ox : Ordinal ) → ψ ox
92 lemma-ord ox = TransFinite {ψ} induction ox where 99 lemma-ord ox = TransFinite0 {ψ} induction ox where
93 ∀-imply-or : {A : Ordinal → Set n } {B : Set n } 100 ∀-imply-or : {A : Ordinal → Set n } {B : Set n }
94 → ((x : Ordinal ) → A x ∨ B) → ((x : Ordinal ) → A x) ∨ B 101 → ((x : Ordinal ) → A x ∨ B) → ((x : Ordinal ) → A x) ∨ B
95 ∀-imply-or {A} {B} ∀AB with p∨¬p ((x : Ordinal ) → A x) -- LEM 102 ∀-imply-or {A} {B} ∀AB with p∨¬p ((x : Ordinal ) → A x) -- LEM
96 ∀-imply-or {A} {B} ∀AB | case1 t = case1 t 103 ∀-imply-or {A} {B} ∀AB | case1 t = case1 t
97 ∀-imply-or {A} {B} ∀AB | case2 x = case2 (lemma (λ not → x not )) where 104 ∀-imply-or {A} {B} ∀AB | case2 x = case2 (lemma (λ not → x not )) where
105 ... | no ¬p = lemma where 112 ... | no ¬p = lemma where
106 lemma1 : (y : Ordinal) → (y o< x → odef X y → ⊥) ∨ choiced (& X) 113 lemma1 : (y : Ordinal) → (y o< x → odef X y → ⊥) ∨ choiced (& X)
107 lemma1 y with ∋-p X (* y) 114 lemma1 y with ∋-p X (* y)
108 lemma1 y | yes y<X = case2 ( record { a-choice = y ; is-in = ∋oo y<X } ) 115 lemma1 y | yes y<X = case2 ( record { a-choice = y ; is-in = ∋oo y<X } )
109 lemma1 y | no ¬y<X = case1 ( λ lt y<X → ¬y<X (d→∋ X y<X) ) 116 lemma1 y | no ¬y<X = case1 ( λ lt y<X → ¬y<X (d→∋ X y<X) )
110 lemma : ((y : Ordinals.ord O) → (O Ordinals.o< y) x → odef X y → ⊥) ∨ choiced (& X) 117 lemma : ((y : Ordinal) → y o< x → odef X y → ⊥) ∨ choiced (& X)
111 lemma = ∀-imply-or lemma1 118 lemma = ∀-imply-or lemma1
119 odef→o< : {X : HOD } → {x : Ordinal } → odef X x → x o< & X
120 odef→o< {X} {x} lt = o<-subst {_} {_} {x} {& X} ( c<→o< ( subst₂ (λ j k → odef j k ) (sym *iso) (sym &iso) lt )) &iso &iso
112 have_to_find : choiced (& X) 121 have_to_find : choiced (& X)
113 have_to_find = dont-or (lemma-ord (& X )) ¬¬X∋x where 122 have_to_find = dont-or (lemma-ord (& X )) ¬¬X∋x where
114 ¬¬X∋x : ¬ ((x : Ordinal) → x o< (& X) → odef X x → ⊥) 123 ¬¬X∋x : ¬ ((x : Ordinal) → x o< (& X) → odef X x → ⊥)
115 ¬¬X∋x nn = not record { 124 ¬¬X∋x nn = not record {
116 eq→ = λ {x} lt → ⊥-elim (nn x (odef→o< lt) lt) 125 eq→ = λ {x} lt → ⊥-elim (nn x (odef→o< lt) lt)
117 ; eq← = λ {x} lt → ⊥-elim ( ¬x<0 lt ) 126 ; eq← = λ {x} lt → ⊥-elim ( ¬x<0 lt )
118 } 127 }
119 128
120 -- 129 --
121 -- axiom regurality from ε-induction (using axiom of choice above) 130 -- axiom regurality from ε-induction (using axiom of choice above)
152 y1prop : (x ∋ y1) ∧ (u ∋ y1) 161 y1prop : (x ∋ y1) ∧ (u ∋ y1)
153 y1prop = oo∋ (is-in y1choice) 162 y1prop = oo∋ (is-in y1choice)
154 min2 : Minimal u 163 min2 : Minimal u
155 min2 = prev (proj1 y1prop) u (proj2 y1prop) 164 min2 = prev (proj1 y1prop) u (proj2 y1prop)
156 Min2 : (x : HOD) → (u : HOD ) → (u∋x : u ∋ x) → Minimal u 165 Min2 : (x : HOD) → (u : HOD ) → (u∋x : u ∋ x) → Minimal u
157 Min2 x u u∋x = (ε-induction1 {λ y → (u : HOD ) → (u∋x : u ∋ y) → Minimal u } induction x u u∋x ) 166 Min2 x u u∋x = (ε-induction {λ y → (u : HOD ) → (u∋x : u ∋ y) → Minimal u } induction x u u∋x )
158 cx : {x : HOD} → ¬ (x =h= od∅ ) → choiced (& x ) 167 cx : {x : HOD} → ¬ (x =h= od∅ ) → choiced (& x )
159 cx {x} nx = choice-func x nx 168 cx {x} nx = choice-func x nx
160 minimal : (x : HOD ) → ¬ (x =h= od∅ ) → HOD 169 minimal : (x : HOD ) → ¬ (x =h= od∅ ) → HOD
161 minimal x ne = min (Min2 (* (a-choice (cx {x} ne) )) x ( oo∋ (is-in (cx ne))) ) 170 minimal x ne = min (Min2 (* (a-choice (cx {x} ne) )) x ( oo∋ (is-in (cx ne))) )
162 x∋minimal : (x : HOD ) → ( ne : ¬ (x =h= od∅ ) ) → odef x ( & ( minimal x ne ) ) 171 x∋minimal : (x : HOD ) → ( ne : ¬ (x =h= od∅ ) ) → odef x ( & ( minimal x ne ) )