Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 1466:e8c166541c86
fix for safe
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 18 Jun 2024 18:46:53 +0900 |
| parents | bd2b003e25ef |
| children | ca5bfb401ada |
| files | Todo src/BAlgebra.agda src/LEMC.agda |
| diffstat | 3 files changed, 85 insertions(+), 98 deletions(-) [+] |
line wrap: on
line diff
--- a/Todo Fri Jan 05 13:50:21 2024 +0900 +++ b/Todo Tue Jun 18 18:46:53 2024 +0900 @@ -1,3 +1,8 @@ +Tue Jun 18 18:43:10 JST 2024 + + make safe in all case + stop using functional extensionality + Sun Jul 9 09:42:20 JST 2023 Assume countable dense OD in Ordinal as L
--- a/src/BAlgebra.agda Fri Jan 05 13:50:21 2024 +0900 +++ b/src/BAlgebra.agda Tue Jun 18 18:46:53 2024 +0900 @@ -3,35 +3,24 @@ open import Ordinals import HODBase import OD +open import Relation.Nullary module BAlgebra {n : Level } (O : Ordinals {n} ) (HODAxiom : HODBase.ODAxiom O) (ho< : OD.ODAxiom-ho< O HODAxiom ) - (AC : OD.AxiomOfChoice O HODAxiom ) - where + (L : HODBase.HOD O) (∋-p : (P : HODBase.HOD O) → OD._⊆_ O HODAxiom P L → (x : HODBase.HOD O) → Dec ( OD._∈_ O HODAxiom x P )) where --- open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ; _⊔_ to _n⊔_ ) open import Relation.Binary.PropositionalEquality hiding ( [_] ) open import Data.Empty -open import Data.Unit -open import Relation.Nullary -open import Relation.Binary hiding (_⇔_) -open import Relation.Binary.Core hiding (_⇔_) -import Relation.Binary.Reasoning.Setoid as EqR -open import logic import OrdUtil -open import nat open Ordinals.Ordinals O open Ordinals.IsOrdinals isOrdinal --- open Ordinals.IsNext isNext +import ODUtil + +open import logic +open import nat + open OrdUtil O -import ODUtil -open ODUtil O HODAxiom ho< -import ODC - --- Ordinal Definable Set - -open HODBase.HOD -open HODBase.OD +open ODUtil O HODAxiom ho< open _∧_ open _∨_ @@ -39,56 +28,52 @@ open HODBase._==_ -open HODBase.ODAxiom HODAxiom +open HODBase.ODAxiom HODAxiom open OD O HODAxiom -open AxiomOfChoice AC -open _∧_ -open _∨_ -open Bool -L＼L=0 : { L : HOD } → (L ＼ L) =h= od∅ -L＼L=0 {L} = record { eq→ = lem0 ; eq← = lem1 } where +L＼L=0 : (L ＼ L) =h= od∅ +L＼L=0 = record { eq→ = lem0 ; eq← = lem1 } where lem0 : {x : Ordinal} → odef (L ＼ L) x → odef od∅ x lem0 {x} ⟪ lx , ¬lx ⟫ = ⊥-elim (¬lx lx) lem1 : {x : Ordinal} → odef od∅ x → odef (L ＼ L) x lem1 {x} lt = ⊥-elim ( ¬∅∋ (subst (λ k → odef od∅ k) (sym &iso) lt )) -L＼Lx=x : { L x : HOD } → x ⊆ L → (L ＼ ( L ＼ x )) =h= x -L＼Lx=x {L} {x} x⊆L = record { eq→ = lem03 ; eq← = lem04 } where +L＼Lx=x : {x : HOD} → x ⊆ L → (L ＼ ( L ＼ x )) =h= x +L＼Lx=x {x} x⊆L = record { eq→ = lem03 ; eq← = lem04 } where lem03 : {z : Ordinal} → odef (L ＼ (L ＼ x)) z → odef x z - lem03 {z} ⟪ Lz , Lxz ⟫ with ODC.∋-p O HODAxiom AC x (* z) + lem03 {z} ⟪ Lz , Lxz ⟫ with ∋-p x x⊆L (* z) ... | yes y = subst (λ k → odef x k ) &iso y ... | no n = ⊥-elim ( Lxz ⟪ Lz , ( subst (λ k → ¬ odef x k ) &iso n ) ⟫ ) lem04 : {z : Ordinal} → odef x z → odef (L ＼ (L ＼ x)) z - lem04 {z} xz with ODC.∋-p O HODAxiom AC L (* z) + lem04 {z} xz with ∋-p L (λ x → x) (* z) ... | yes y = ⟪ subst (λ k → odef L k ) &iso y , ( λ p → proj2 p xz ) ⟫ ... | no n = ⊥-elim ( n (subst (λ k → odef L k ) (sym &iso) ( x⊆L xz) )) -L＼0=L : { L : HOD } → (L ＼ od∅) =h= L -L＼0=L {L} = record { eq→ = lem05 ; eq← = lem06 } where +L＼0=L : (L ＼ od∅) =h= L +L＼0=L = record { eq→ = lem05 ; eq← = lem06 } where lem05 : {x : Ordinal} → odef (L ＼ od∅) x → odef L x lem05 {x} ⟪ Lx , _ ⟫ = Lx lem06 : {x : Ordinal} → odef L x → odef (L ＼ od∅) x lem06 {x} Lx = ⟪ Lx , (λ lt → ¬x<0 lt) ⟫ -∨L＼X : { L X : HOD } → {x : Ordinal } → odef L x → odef X x ∨ odef (L ＼ X) x -∨L＼X {L} {X} {x} Lx with ODC.∋-p O HODAxiom AC X (* x) -... | yes y = case1 ( subst (λ k → odef X k ) &iso y ) -... | no n = case2 ⟪ Lx , subst (λ k → ¬ odef X k) &iso n ⟫ +∨L＼X : { X : HOD } → {x : Ordinal } → odef L x → odef X x ∨ odef (L ＼ X) x +∨L＼X {X} {x} Lx with ∋-p (X ∩ L) (λ lt → proj2 lt ) (* x) +... | yes y = case1 ( subst (λ k → odef X k ) &iso (proj1 y) ) +... | no n = case2 ⟪ Lx , subst (λ k → ¬ odef X k) &iso (λ lt → ⊥-elim ( n ⟪ lt , subst (λ k → odef L k) (sym &iso) Lx ⟫ ) ) ⟫ -＼-⊆ : { P A B : HOD } → A ⊆ P → ( A ⊆ B → ( P ＼ B ) ⊆ ( P ＼ A )) ∧ (( P ＼ B ) ⊆ ( P ＼ A ) → A ⊆ B ) -＼-⊆ {P} {A} {B} A⊆P = ⟪ ( λ a<b {x} pbx → ⟪ proj1 pbx , (λ ax → proj2 pbx (a<b ax)) ⟫ ) , lem07 ⟫ where - lem07 : (P ＼ B) ⊆ (P ＼ A) → A ⊆ B - lem07 pba {x} ax with ODC.p∨¬p O HODAxiom AC (odef B x) - ... | case1 bx = bx - ... | case2 ¬bx = ⊥-elim ( proj2 ( pba ⟪ A⊆P ax , ¬bx ⟫ ) ax ) +＼-⊆ : { A B : HOD } → A ⊆ L → ( A ⊆ B → ( L ＼ B ) ⊆ ( L ＼ A )) ∧ (( L ＼ B ) ⊆ ( L ＼ A ) → A ⊆ B ) +＼-⊆ {A} {B} A⊆L = ⟪ ( λ a<b {x} pbx → ⟪ proj1 pbx , (λ ax → proj2 pbx (a<b ax)) ⟫ ) , lem07 ⟫ where + lem07 : (L ＼ B) ⊆ (L ＼ A) → A ⊆ B + lem07 pba {x} ax with ∋-p (B ∩ L) proj2 (* x) + ... | yes bx = subst (λ k → odef B k ) &iso (proj1 bx) + ... | no ¬bx = ⊥-elim ( proj2 ( pba ⟪ A⊆L ax , (λ bx → ¬bx ⟪ d→∋ B bx , subst (λ k → odef L k) (sym &iso) ( A⊆L ax) ⟫) ⟫ ) ax ) -RC＼ : {L : HOD} → RCod (Power (Union L)) (λ z → L ＼ z ) -RC＼ {L} = record { ≤COD = λ {x} lt z xz → lemm {x} lt z xz ; ψ-eq = λ {x} {y} → wdf {x} {y} } where +RC＼ : RCod (Power (Union L)) (λ z → L ＼ z ) +RC＼ = record { ≤COD = λ {x} lt z xz → lemm {x} lt z xz ; ψ-eq = λ {x} {y} → wdf {x} {y} } where lemm : {x : HOD} → (L ＼ x) ⊆ Power (Union L ) lemm {x} ⟪ Ly , nxy ⟫ z xz = record { owner = _ ; ao = Ly ; ox = xz } - wdf : {x y : HOD} → od x == od y → (L ＼ x) =h= (L ＼ y) + wdf : {x y : HOD} → x =h= y → (L ＼ x) =h= (L ＼ y) wdf {x} {y} x=y = record { eq→ = λ {p} lxp → ⟪ proj1 lxp , (λ yp → proj2 lxp (eq← x=y yp) ) ⟫ ; eq← = λ {p} lxp → ⟪ proj1 lxp , (λ yp → proj2 lxp (eq→ x=y yp) ) ⟫ } @@ -97,10 +82,10 @@ [a-b]∩b=0 {A} {B} = record { eq← = λ lt → ⊥-elim ( ¬∅∋ (subst (λ k → odef od∅ k) (sym &iso) lt )) ; eq→ = λ {x} lt → ⊥-elim (proj2 (proj1 lt ) (proj2 lt)) } -U-F=∅→F⊆U : {F U : HOD} → ((x : Ordinal) → ¬ ( odef F x ∧ ( ¬ odef U x ))) → F ⊆ U -U-F=∅→F⊆U {F} {U} not = gt02 where +U-F=∅→F⊆U : {F U : HOD} → U ⊆ L → ((x : Ordinal) → ¬ ( odef F x ∧ ( ¬ odef U x ))) → F ⊆ U +U-F=∅→F⊆U {F} {U} U⊆L not = gt02 where gt02 : { x : Ordinal } → odef F x → odef U x - gt02 {x} fx with ODC.∋-p O HODAxiom AC U (* x) + gt02 {x} fx with ∋-p U U⊆L (* x) ... | yes y = subst (λ k → odef U k ) &iso y ... | no n = ⊥-elim ( not x ⟪ fx , subst (λ k → ¬ odef U k ) &iso n ⟫ ) @@ -153,6 +138,12 @@ lemma2 {x} lt | case1 cp | _ = case1 cp lemma2 {x} lt | _ | case1 cp = case1 cp lemma2 {x} lt | case2 cq | case2 cr = case2 ⟪ cq , cr ⟫ +record PowerP (P : HOD) : Set (suc n) where + constructor ⟦_,_⟧ + field + hod : HOD + x⊆P : hod ⊆ P + record IsBooleanAlgebra {n m : Level} ( L : Set n) ( _≈_ : L → L → Set m ) @@ -185,16 +176,10 @@ _x_ : L → L → L isBooleanAlgebra : IsBooleanAlgebra L _≈_ b1 b0 -_ _+_ _x_ -record PowerP (P : HOD) : Set (suc n) where - constructor ⟦_,_⟧ - field - hod : HOD - x⊆P : hod ⊆ P -open PowerP - -HODBA : (P : HOD) → BooleanAlgebra {suc n} {n} (PowerP P) -HODBA P = record { _≈_ = λ x y → hod x =h= hod y ; b1 = ⟦ P , (λ x → x) ⟧ ; b0 = ⟦ od∅ , (λ x → ⊥-elim (¬x<0 x)) ⟧ +HODBA : (P : HODBase.HOD O) (∋-p : (Q : HODBase.HOD O) → OD._⊆_ O HODAxiom Q P → ( x : HODBase.HOD O ) → Dec ( OD._∈_ O HODAxiom x Q )) + → BooleanAlgebra (PowerP P) +HODBA P ∋-p = record { _≈_ = λ x y → hod x =h= hod y ; b1 = ⟦ P , (λ x → x) ⟧ ; b0 = ⟦ od∅ , (λ x → ⊥-elim (¬x<0 x)) ⟧ ; -_ = λ x → ⟦ P ＼ hod x , proj1 ⟧ ; _+_ = λ x y → ⟦ hod x ∪ hod y , ba00 x y ⟧ ; _x_ = λ x y → ⟦ hod x ∩ hod y , (λ lt → x⊆P x (proj1 lt)) ⟧ ; isBooleanAlgebra = record { @@ -213,6 +198,7 @@ ; a+-a1 = λ {a} → record { eq→ = ba06 a ; eq← = ba07 a } ; ax-a0 = λ {a} → record { eq→ = ba08 a ; eq← = λ lt → ⊥-elim (¬x<0 lt) } } } where + open PowerP ba00 : (x y : PowerP P ) → (hod x ∪ hod y) ⊆ P ba00 x y (case1 px) = x⊆P x px ba00 x y (case2 py) = x⊆P y py @@ -227,7 +213,7 @@ ba02 a b c {x} (case1 (case2 bx)) = case2 (case1 bx) ba02 a b c {x} (case2 cx) = case2 (case2 cx) ba03 : (a b : PowerP P) → {x : Ordinal} → - odef (hod a) x ∨ odef (hod a ∩ hod b) x → def (od (hod a)) x + odef (hod a) x ∨ odef (hod a ∩ hod b) x → odef (hod a) x ba03 a b (case1 ax) = ax ba03 a b (case2 ab) = proj1 ab ba04 : (a : HOD) → {x : Ordinal} → odef a x ∨ odef od∅ x → odef a x @@ -236,13 +222,13 @@ ba05 : {a b : HOD} {x : Ordinal} → odef a x ∨ odef b x → odef b x ∨ odef a x ba05 (case1 x) = case2 x ba05 (case2 x) = case1 x - ba06 : (a : PowerP P ) → { x : Ordinal} → odef (hod a) x ∨ odef (P ＼ hod a) x → def (od P) x + ba06 : (a : PowerP P ) → { x : Ordinal} → odef (hod a) x ∨ odef (P ＼ hod a) x → odef P x ba06 a {x} (case1 ax) = x⊆P a ax ba06 a {x} (case2 nax) = proj1 nax - ba07 : (a : PowerP P ) → { x : Ordinal} → def (od P) x → odef (hod a) x ∨ odef (P ＼ hod a) x - ba07 a {x} px with ODC.∋-p O HODAxiom AC (hod a) (* x) + ba07 : (a : PowerP P ) → { x : Ordinal} → odef P x → odef (hod a) x ∨ odef (P ＼ hod a) x + ba07 a {x} px with ∋-p (hod a) (x⊆P a) (* x) ... | yes y = case1 (subst (λ k → odef (hod a) k) &iso y) ... | no n = case2 ⟪ px , subst (λ k → ¬ odef (hod a) k) &iso n ⟫ - ba08 : (a : PowerP P) → {x : Ordinal} → def (od (hod a ∩ (P ＼ hod a))) x → def (od od∅) x + ba08 : (a : PowerP P) → {x : Ordinal} → odef (hod a ∩ (P ＼ hod a)) x → odef od∅ x ba08 a {x} ⟪ ax , ⟪ px , nax ⟫ ⟫ = ⊥-elim ( nax ax )
--- a/src/LEMC.agda Fri Jan 05 13:50:21 2024 +0900 +++ b/src/LEMC.agda Tue Jun 18 18:46:53 2024 +0900 @@ -1,38 +1,41 @@ +{-# OPTIONS --cubical-compatible --safe #-} open import Level open import Ordinals open import logic open import Relation.Nullary -module LEMC {n : Level } (O : Ordinals {n} ) where - -open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ; _⊔_ to _n⊔_ ) -open import Relation.Binary.PropositionalEquality -open import Data.Nat.Properties -open import Data.Empty -open import Relation.Binary -open import Relation.Binary.Core -open import nat +open import Level +open import Ordinals +import HODBase import OD +open import Relation.Nullary +module LEMC {n : Level } (O : Ordinals {n} ) (HODAxiom : HODBase.ODAxiom O) (ho< : OD.ODAxiom-ho< O HODAxiom )( p∨¬p : ( p : Set n) → p ∨ ( ¬ p ) ) where -open inOrdinal O -open OD O -open OD.OD -open OD._==_ -open ODAxiom odAxiom +open import Relation.Binary.PropositionalEquality hiding ( [_] ) +open import Data.Empty + import OrdUtil -import ODUtil + open Ordinals.Ordinals O open Ordinals.IsOrdinals isOrdinal --- open Ordinals.IsNext isNext +import ODUtil + +open import logic +open import nat + open OrdUtil O -open ODUtil O +open ODUtil O HODAxiom ho< -open import zfc +open _∧_ +open _∨_ +open Bool -open HOD +open HODBase._==_ -postulate - p∨¬p : ( p : Set n) → p ∨ ( ¬ p ) +open HODBase.ODAxiom HODAxiom +open OD O HODAxiom + +open HODBase.HOD decp : ( p : Set n ) → Dec p -- assuming axiom of choice decp p with p∨¬p p @@ -49,11 +52,6 @@ ... | yes p = p ... | no ¬p = ⊥-elim ( notnot ¬p ) --- by-contradiction : {A : Set n} {B : A → Set n} → ¬ ( (a : A ) → ¬ B a ) → A --- by-contradiction {A} {B} not with p∨¬p A --- ... | case2 ¬a = ⊥-elim (not (λ a → ⊥-elim (¬a a ))) --- ... | case1 a = a - power→⊆ : ( A t : HOD) → Power A ∋ t → t ⊆ A power→⊆ A t PA∋t t∋x = subst (λ k → odef A k ) &iso ( t1 (subst (λ k → odef t k ) (sym &iso) t∋x)) where t1 : {x : HOD } → t ∋ x → A ∋ x @@ -68,14 +66,13 @@ open choiced --- ∋→d : ( a : HOD ) { x : HOD } → * (& a) ∋ x → X ∋ * (a-choice (choice-func X not)) --- ∋→d a lt = subst₂ (λ j k → odef j k) *iso (sym &iso) lt - oo∋ : { a : HOD} { x : Ordinal } → odef (* (& a)) x → a ∋ * x -oo∋ lt = subst₂ (λ j k → odef j k) *iso (sym &iso) lt +oo∋ {a} {x} lt = eq→ *iso (subst (λ k → odef (* (& a)) k ) (sym &iso) lt ) ∋oo : { a : HOD} { x : Ordinal } → a ∋ * x → odef (* (& a)) x -∋oo lt = subst₂ (λ j k → odef j k ) (sym *iso) &iso lt +∋oo {a} {x} lt = eq← *iso (subst (λ k → odef a k ) &iso lt ) + +open import zfc OD→ZFC : ZFC OD→ZFC = record { @@ -83,12 +80,11 @@ ; _∋_ = _∋_ ; _≈_ = _=h=_ ; ∅ = od∅ - ; Select = Select ; isZFC = isZFC } where -- infixr 200 _∈_ -- infixr 230 _∩_ _∪_ - isZFC : IsZFC (HOD ) _∋_ _=h=_ od∅ Select + isZFC : IsZFC (HOD ) _∋_ _=h=_ od∅ isZFC = record { choice-func = λ A {X} not A∋X → * (a-choice (choice-func X not) ); choice = λ A {X} A∋X not → oo∋ (is-in (choice-func X not)) @@ -101,7 +97,7 @@ ψ : ( ox : Ordinal ) → Set n ψ ox = (( x : Ordinal ) → x o< ox → ( ¬ odef X x )) ∨ choiced (& X) lemma-ord : ( ox : Ordinal ) → ψ ox - lemma-ord ox = TransFinite0 {ψ} induction ox where + lemma-ord ox = inOrdinal.TransFinite0 O {ψ} induction ox where ∀-imply-or : {A : Ordinal → Set n } {B : Set n } → ((x : Ordinal ) → A x ∨ B) → ((x : Ordinal ) → A x) ∨ B ∀-imply-or {A} {B} ∀AB with p∨¬p ((x : Ordinal ) → A x) -- LEM @@ -122,7 +118,7 @@ lemma : ((y : Ordinal) → y o< x → odef X y → ⊥) ∨ choiced (& X) lemma = ∀-imply-or lemma1 odef→o< : {X : HOD } → {x : Ordinal } → odef X x → x o< & X - odef→o< {X} {x} lt = o<-subst {_} {_} {x} {& X} ( c<→o< ( subst₂ (λ j k → odef j k ) (sym *iso) (sym &iso) lt )) &iso &iso + odef→o< {X} {x} lt = o<-subst {_} {_} {x} {& X} ( c<→o< (eq← *iso (subst (λ k → odef X k) (sym &iso) lt ))) &iso &iso have_to_find : choiced (& X) have_to_find = dont-or (lemma-ord (& X )) ¬¬X∋x where ¬¬X∋x : ¬ ((x : Ordinal) → x o< (& X) → odef X x → ⊥) @@ -154,7 +150,7 @@ ... | case2 NP = min2 where p : HOD p = record { od = record { def = λ y1 → odef x y1 ∧ odef u y1 } ; odmax = omin (odmax x) (odmax u) ; <odmax = lemma } where - lemma : {y : Ordinal} → OD.def (od x) y ∧ OD.def (od u) y → y o< omin (odmax x) (odmax u) + lemma : {y : Ordinal} → odef x y ∧ odef u y → y o< omin (odmax x) (odmax u) lemma {y} lt = min1 (<odmax x (proj1 lt)) (<odmax u (proj2 lt)) np : ¬ (p =h= od∅) np p∅ = NP (λ y p∋y → ∅< {p} {_} (d→∋ p p∋y) p∅ )