Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 284:a8f9c8a27e8d
minimal from LEM
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 10 May 2020 09:19:32 +0900 |
| parents | 2d77b6d12a22 |
| children | 313140ae5e3d |
| files | LEMC.agda |
| diffstat | 1 files changed, 42 insertions(+), 59 deletions(-) [+] |
line wrap: on
line diff
--- a/LEMC.agda Sun May 10 00:18:59 2020 +0900 +++ b/LEMC.agda Sun May 10 09:19:32 2020 +0900 @@ -32,6 +32,12 @@ open choiced +double-neg-eilm : {A : Set (suc n)} → ¬ ¬ A → A -- we don't have this in intutionistic logic +double-neg-eilm {A} notnot with p∨¬p A -- assuming axiom of choice +... | case1 p = p +... | case2 ¬p = ⊥-elim ( notnot ¬p ) + + OD→ZFC : ZFC OD→ZFC = record { ZFSet = OD @@ -91,68 +97,45 @@ min-empty : (y : OD ) → ¬ ( min ∋ y) ∧ (x ∋ y) open Minimal open _∧_ - induction : {x : OD} → ({y : OD} → x ∋ y → (ne : ¬ (y == od∅ )) → Minimal y ne ) → (ne : ¬ (x == od∅ )) → Minimal x ne - induction {x} prev ne = c2 - where - ch : choiced x - ch = choice-func x ne - c1 : OD - c1 = a-choice ch -- x ∋ c1 - c2 : Minimal x ne - c2 with p∨¬p ( (y : OD ) → ¬ ( def c1 (od→ord y) ∧ (def x (od→ord y))) ) - c2 | case1 Yes = record { - min = c1 - ; x∋min = is-in ch - ; min-empty = Yes - } - c2 | case2 No = c3 where - y1 : OD - y1 = record { def = λ y → ( def c1 y ∧ def x y) } - noty1 : ¬ (y1 == od∅ ) - noty1 not = ⊥-elim ( No (λ z n → ∅< n not ) ) - ch1 : choiced y1 -- a-choice ch1 ∈ c1 , a-choice ch1 ∈ x - ch1 = choice-func y1 noty1 - c3 : Minimal x ne - c3 with is-o∅ (od→ord (a-choice ch1)) - ... | yes eq = record { - min = od∅ - ; x∋min = def-subst {x} {od→ord (a-choice ch1)} {x} (proj2 (is-in ch1)) refl (trans eq (sym ord-od∅) ) - ; min-empty = λ z p → ⊥-elim ( ¬x<0 (proj1 p) ) - } - ... | no n = record { - min = min min3 - ; x∋min = x∋min3 (x∋min min3) - ; min-empty = min3-empty -- λ y p → min3-empty min3 y p -- p : (min min3 ∋ y) ∧ (x ∋ y) - } where - lemma : (a-choice ch1 == od∅ ) → od→ord (a-choice ch1) ≡ o∅ - lemma eq = begin - od→ord (a-choice ch1) - ≡⟨ cong (λ k → od→ord k ) (==→o≡ eq ) ⟩ - od→ord od∅ - ≡⟨ ord-od∅ ⟩ - o∅ - ∎ where open ≡-Reasoning - -- Minimal (a-choice ch1) ch1not - -- min ∈ a-choice ch1 , min ∩ a-choice ch1 ≡ ∅ - ch1not : ¬ (a-choice ch1 == od∅) - ch1not ch1=0 = n (lemma ch1=0) - min3 : Minimal (a-choice ch1) ch1not - min3 = prev (proj2 (is-in ch1)) (λ ch1=0 → n (lemma ch1=0)) - x∋min3 : a-choice ch1 ∋ min min3 → x ∋ min min3 - x∋min3 lt = {!!} - min3-empty : (y : OD ) → ¬ ((min min3 ∋ y) ∧ (x ∋ y)) - min3-empty y p = min-empty min3 y record { proj1 = proj1 p ; proj2 = ? } -- (min min3 ∋ y) ∧ (a-choice ch1 ∋ y) - -- p : (min min3 ∋ y) ∧ (x ∋ y) - - - Min1 : (x : OD) → (ne : ¬ (x == od∅ )) → Minimal x ne - Min1 x ne = (ε-induction {λ y → (ne : ¬ (y == od∅ ) ) → Minimal y ne } induction x ne ) + -- + -- from https://math.stackexchange.com/questions/2973777/is-it-possible-to-prove-regularity-with-transfinite-induction-only + -- + induction : {x : OD} → ({y : OD} → x ∋ y → (u : OD ) → (u∋x : u ∋ y) → Minimal u (∅< u∋x)) + → (u : OD ) → (u∋x : u ∋ x) → Minimal u (∅< u∋x) + induction {x} prev u u∋x with p∨¬p ((y : OD) → ¬ (x ∋ y) ∧ (u ∋ y)) + ... | case1 P = + record { min = x + ; x∋min = u∋x + ; min-empty = P + } + ... | case2 NP = + record { min = min min2 + ; x∋min = x∋min min2 + ; min-empty = min-empty min2 + + } where + p : OD + p = record { def = λ y1 → def x y1 ∧ def u y1 } + np : ¬ (p == od∅) + np p∅ = NP (λ y p∋y → ∅< p∋y p∅ ) + y1choice : choiced p + y1choice = choice-func p np + y1 : OD + y1 = a-choice y1choice + y1prop : (x ∋ y1) ∧ (u ∋ y1) + y1prop = is-in y1choice + min2 : Minimal u (∅< (proj2 y1prop)) + min2 = prev (proj1 y1prop) u (proj2 y1prop) + Min2 : (x : OD) → (u : OD ) → (u∋x : u ∋ x) → Minimal u (∅< u∋x) + Min2 x u u∋x = (ε-induction {λ y → (u : OD ) → (u∋x : u ∋ y) → Minimal u (∅< u∋x) } induction x u u∋x ) + cx : {x : OD} → ¬ (x == od∅ ) → choiced x + cx {x} nx = choice-func x nx minimal : (x : OD ) → ¬ (x == od∅ ) → OD - minimal x not = min (Min1 x not ) + minimal x not = min (Min2 (a-choice (cx not) ) x (is-in (cx not))) x∋minimal : (x : OD ) → ( ne : ¬ (x == od∅ ) ) → def x ( od→ord ( minimal x ne ) ) - x∋minimal x ne = x∋min (Min1 x ne) + x∋minimal x ne = x∋min (Min2 (a-choice (cx ne) ) x (is-in (cx ne))) minimal-1 : (x : OD ) → ( ne : ¬ (x == od∅ ) ) → (y : OD ) → ¬ ( def (minimal x ne) (od→ord y)) ∧ (def x (od→ord y) ) - minimal-1 x ne y = min-empty (Min1 x ne ) y + minimal-1 x ne y = min-empty (Min2 (a-choice (cx ne) ) x (is-in (cx ne))) y