Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 288:4fcac1eebc74 release
axiom of choice clean up
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 07 Jun 2020 20:31:30 +0900 |
| parents | 6e1c60866788 (current diff) 5de8905a5a2b (diff) |
| children | 9f926b2210bc |
| files | |
| diffstat | 27 files changed, 4260 insertions(+), 450 deletions(-) [+] |
line wrap: on
line diff
--- a/.hgtags Thu Aug 29 16:18:37 2019 +0900 +++ b/.hgtags Sun Jun 07 20:31:30 2020 +0900 @@ -15,3 +15,9 @@ 1b1620e2053cfc340a4df0d63de65b9059b19b6f current 1b1620e2053cfc340a4df0d63de65b9059b19b6f current 2ea2a19f9cd638b29af51a47fa3dabdaea381d5c current +2ea2a19f9cd638b29af51a47fa3dabdaea381d5c current +29a85a427ed21beb9be068728f7c55a7070a0a9f current +29a85a427ed21beb9be068728f7c55a7070a0a9f current +d9d3654baee12c1b93a25a3994146bc001877b2b current +d9d3654baee12c1b93a25a3994146bc001877b2b current +313140ae5e3d1793f8b2dc9055159658d63874e4 current
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/BAlgbra.agda Sun Jun 07 20:31:30 2020 +0900 @@ -0,0 +1,109 @@ +open import Level +open import Ordinals +module BAlgbra {n : Level } (O : Ordinals {n}) where + +open import zf +open import logic +import OD +import ODC + +open import Relation.Nullary +open import Relation.Binary +open import Data.Empty +open import Relation.Binary +open import Relation.Binary.Core +open import Relation.Binary.PropositionalEquality +open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ; _⊔_ to _n⊔_ ) + +open inOrdinal O +open OD O +open OD.OD +open ODAxiom odAxiom + +open _∧_ +open _∨_ +open Bool + +_∩_ : ( A B : OD ) → OD +A ∩ B = record { def = λ x → def A x ∧ def B x } + +_∪_ : ( A B : OD ) → OD +A ∪ B = record { def = λ x → def A x ∨ def B x } + +_＼_ : ( A B : OD ) → OD +A ＼ B = record { def = λ x → def A x ∧ ( ¬ ( def B x ) ) } + +∪-Union : { A B : OD } → Union (A , B) ≡ ( A ∪ B ) +∪-Union {A} {B} = ==→o≡ ( record { eq→ = lemma1 ; eq← = lemma2 } ) where + lemma1 : {x : Ordinal} → def (Union (A , B)) x → def (A ∪ B) x + lemma1 {x} lt = lemma3 lt where + lemma4 : {y : Ordinal} → def (A , B) y ∧ def (ord→od y) x → ¬ (¬ ( def A x ∨ def B x) ) + lemma4 {y} z with proj1 z + lemma4 {y} z | case1 refl = double-neg (case1 ( subst (λ k → def k x ) oiso (proj2 z)) ) + lemma4 {y} z | case2 refl = double-neg (case2 ( subst (λ k → def k x ) oiso (proj2 z)) ) + lemma3 : (((u : Ordinals.ord O) → ¬ def (A , B) u ∧ def (ord→od u) x) → ⊥) → def (A ∪ B) x + lemma3 not = ODC.double-neg-eilm O (FExists _ lemma4 not) -- choice + lemma2 : {x : Ordinal} → def (A ∪ B) x → def (Union (A , B)) x + lemma2 {x} (case1 A∋x) = subst (λ k → def (Union (A , B)) k) diso ( IsZF.union→ isZF (A , B) (ord→od x) A + (record { proj1 = case1 refl ; proj2 = subst (λ k → def A k) (sym diso) A∋x})) + lemma2 {x} (case2 B∋x) = subst (λ k → def (Union (A , B)) k) diso ( IsZF.union→ isZF (A , B) (ord→od x) B + (record { proj1 = case2 refl ; proj2 = subst (λ k → def B k) (sym diso) B∋x})) + +∩-Select : { A B : OD } → Select A ( λ x → ( A ∋ x ) ∧ ( B ∋ x ) ) ≡ ( A ∩ B ) +∩-Select {A} {B} = ==→o≡ ( record { eq→ = lemma1 ; eq← = lemma2 } ) where + lemma1 : {x : Ordinal} → def (Select A (λ x₁ → (A ∋ x₁) ∧ (B ∋ x₁))) x → def (A ∩ B) x + lemma1 {x} lt = record { proj1 = proj1 lt ; proj2 = subst (λ k → def B k ) diso (proj2 (proj2 lt)) } + lemma2 : {x : Ordinal} → def (A ∩ B) x → def (Select A (λ x₁ → (A ∋ x₁) ∧ (B ∋ x₁))) x + lemma2 {x} lt = record { proj1 = proj1 lt ; proj2 = + record { proj1 = subst (λ k → def A k) (sym diso) (proj1 lt) ; proj2 = subst (λ k → def B k ) (sym diso) (proj2 lt) } } + +dist-ord : {p q r : OD } → p ∩ ( q ∪ r ) ≡ ( p ∩ q ) ∪ ( p ∩ r ) +dist-ord {p} {q} {r} = ==→o≡ ( record { eq→ = lemma1 ; eq← = lemma2 } ) where + lemma1 : {x : Ordinal} → def (p ∩ (q ∪ r)) x → def ((p ∩ q) ∪ (p ∩ r)) x + lemma1 {x} lt with proj2 lt + lemma1 {x} lt | case1 q∋x = case1 ( record { proj1 = proj1 lt ; proj2 = q∋x } ) + lemma1 {x} lt | case2 r∋x = case2 ( record { proj1 = proj1 lt ; proj2 = r∋x } ) + lemma2 : {x : Ordinal} → def ((p ∩ q) ∪ (p ∩ r)) x → def (p ∩ (q ∪ r)) x + lemma2 {x} (case1 p∩q) = record { proj1 = proj1 p∩q ; proj2 = case1 (proj2 p∩q ) } + lemma2 {x} (case2 p∩r) = record { proj1 = proj1 p∩r ; proj2 = case2 (proj2 p∩r ) } + +dist-ord2 : {p q r : OD } → p ∪ ( q ∩ r ) ≡ ( p ∪ q ) ∩ ( p ∪ r ) +dist-ord2 {p} {q} {r} = ==→o≡ ( record { eq→ = lemma1 ; eq← = lemma2 } ) where + lemma1 : {x : Ordinal} → def (p ∪ (q ∩ r)) x → def ((p ∪ q) ∩ (p ∪ r)) x + lemma1 {x} (case1 cp) = record { proj1 = case1 cp ; proj2 = case1 cp } + lemma1 {x} (case2 cqr) = record { proj1 = case2 (proj1 cqr) ; proj2 = case2 (proj2 cqr) } + lemma2 : {x : Ordinal} → def ((p ∪ q) ∩ (p ∪ r)) x → def (p ∪ (q ∩ r)) x + lemma2 {x} lt with proj1 lt | proj2 lt + lemma2 {x} lt | case1 cp | _ = case1 cp + lemma2 {x} lt | _ | case1 cp = case1 cp + lemma2 {x} lt | case2 cq | case2 cr = case2 ( record { proj1 = cq ; proj2 = cr } ) + +record IsBooleanAlgebra ( L : Set n) + ( b1 : L ) + ( b0 : L ) + ( -_ : L → L ) + ( _+_ : L → L → L ) + ( _*_ : L → L → L ) : Set (suc n) where + field + +-assoc : {a b c : L } → a + ( b + c ) ≡ (a + b) + c + *-assoc : {a b c : L } → a * ( b * c ) ≡ (a * b) * c + +-sym : {a b : L } → a + b ≡ b + a + -sym : {a b : L } → a * b ≡ b * a + -aab : {a b : L } → a + ( a * b ) ≡ a + *-aab : {a b : L } → a * ( a + b ) ≡ a + -dist : {a b c : L } → a + ( b * c ) ≡ ( a * b ) + ( a * c ) + *-dist : {a b c : L } → a * ( b + c ) ≡ ( a + b ) * ( a + c ) + a+0 : {a : L } → a + b0 ≡ a + a*1 : {a : L } → a * b1 ≡ a + a+-a1 : {a : L } → a + ( - a ) ≡ b1 + a*-a0 : {a : L } → a * ( - a ) ≡ b0 + +record BooleanAlgebra ( L : Set n) : Set (suc n) where + field + b1 : L + b0 : L + -_ : L → L + _++_ : L → L → L + _**_ : L → L → L + isBooleanAlgebra : IsBooleanAlgebra L b1 b0 -_ _++_ _**_ +
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/LEMC.agda Sun Jun 07 20:31:30 2020 +0900 @@ -0,0 +1,131 @@ +open import Level +open import Ordinals +open import logic +open import Relation.Nullary +module LEMC {n : Level } (O : Ordinals {n} ) (p∨¬p : ( p : Set (suc n)) → p ∨ ( ¬ p )) where + +open import zf +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 +import OD + +open inOrdinal O +open OD O +open OD.OD +open OD._==_ +open ODAxiom odAxiom + +open import zfc + +--- With assuption of OD is ordered, p ∨ ( ¬ p ) <=> axiom of choice +--- +record choiced ( X : OD) : Set (suc n) where + field + a-choice : OD + is-in : X ∋ a-choice + +open choiced + +OD→ZFC : ZFC +OD→ZFC = record { + ZFSet = OD + ; _∋_ = _∋_ + ; _≈_ = _==_ + ; ∅ = od∅ + ; Select = Select + ; isZFC = isZFC + } where + -- infixr 200 _∈_ + -- infixr 230 _∩_ _∪_ + isZFC : IsZFC (OD ) _∋_ _==_ od∅ Select + isZFC = record { + choice-func = λ A {X} not A∋X → a-choice (choice-func X not ); + choice = λ A {X} A∋X not → is-in (choice-func X not) + } where + choice-func : (X : OD ) → ¬ ( X == od∅ ) → choiced X + choice-func X not = have_to_find where + ψ : ( ox : Ordinal ) → Set (suc n) + ψ ox = (( x : Ordinal ) → x o< ox → ( ¬ def X x )) ∨ choiced X + lemma-ord : ( ox : Ordinal ) → ψ ox + lemma-ord ox = TransFinite {ψ} induction ox where + ∋-p : (A x : OD ) → Dec ( A ∋ x ) + ∋-p A x with p∨¬p (Lift (suc n) ( A ∋ x )) -- LEM + ∋-p A x | case1 (lift t) = yes t + ∋-p A x | case2 t = no (λ x → t (lift x )) + ∀-imply-or : {A : Ordinal → Set n } {B : Set (suc n) } + → ((x : Ordinal ) → A x ∨ B) → ((x : Ordinal ) → A x) ∨ B + ∀-imply-or {A} {B} ∀AB with p∨¬p (Lift ( suc n ) ((x : Ordinal ) → A x)) -- LEM + ∀-imply-or {A} {B} ∀AB | case1 (lift t) = case1 t + ∀-imply-or {A} {B} ∀AB | case2 x = case2 (lemma (λ not → x (lift not ))) where + lemma : ¬ ((x : Ordinal ) → A x) → B + lemma not with p∨¬p B + lemma not | case1 b = b + lemma not | case2 ¬b = ⊥-elim (not (λ x → dont-orb (∀AB x) ¬b )) + induction : (x : Ordinal) → ((y : Ordinal) → y o< x → ψ y) → ψ x + induction x prev with ∋-p X ( ord→od x) + ... | yes p = case2 ( record { a-choice = ord→od x ; is-in = p } ) + ... | no ¬p = lemma where + lemma1 : (y : Ordinal) → (y o< x → def X y → ⊥) ∨ choiced X + lemma1 y with ∋-p X (ord→od y) + lemma1 y | yes y<X = case2 ( record { a-choice = ord→od y ; is-in = y<X } ) + lemma1 y | no ¬y<X = case1 ( λ lt y<X → ¬y<X (subst (λ k → def X k ) (sym diso) y<X ) ) + lemma : ((y : Ordinals.ord O) → (O Ordinals.o< y) x → def X y → ⊥) ∨ choiced X + lemma = ∀-imply-or lemma1 + have_to_find : choiced X + have_to_find = dont-or (lemma-ord (od→ord X )) ¬¬X∋x where + ¬¬X∋x : ¬ ((x : Ordinal) → x o< (od→ord X) → def X x → ⊥) + ¬¬X∋x nn = not record { + eq→ = λ {x} lt → ⊥-elim (nn x (def→o< lt) lt) + ; eq← = λ {x} lt → ⊥-elim ( ¬x<0 lt ) + } + record Minimal (x : OD) : Set (suc n) where + field + min : OD + x∋min : x ∋ min + min-empty : (y : OD ) → ¬ ( min ∋ y) ∧ (x ∋ y) + open Minimal + open _∧_ + -- + -- 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 : OD ) → (u∋x : u ∋ x) → Minimal u + 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 = 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 + min2 = prev (proj1 y1prop) u (proj2 y1prop) + Min2 : (x : OD) → (u : OD ) → (u∋x : u ∋ x) → Minimal u + Min2 x u u∋x = (ε-induction {λ y → (u : OD ) → (u∋x : u ∋ y) → Minimal u } 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 (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 (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 (Min2 (a-choice (cx ne) ) x (is-in (cx ne))) y + + + +
--- a/OD.agda Thu Aug 29 16:18:37 2019 +0900 +++ b/OD.agda Sun Jun 07 20:31:30 2020 +0900 @@ -36,21 +36,56 @@ id : {A : Set n} → A → A id x = x -eq-refl : { x : OD } → x == x -eq-refl {x} = record { eq→ = id ; eq← = id } +==-refl : { x : OD } → x == x +==-refl {x} = record { eq→ = id ; eq← = id } open _==_ -eq-sym : { x y : OD } → x == y → y == x -eq-sym eq = record { eq→ = eq← eq ; eq← = eq→ eq } +==-trans : { x y z : OD } → x == y → y == z → x == z +==-trans x=y y=z = record { eq→ = λ {m} t → eq→ y=z (eq→ x=y t) ; eq← = λ {m} t → eq← x=y (eq← y=z t) } -eq-trans : { x y z : OD } → x == y → y == z → x == z -eq-trans x=y y=z = record { eq→ = λ t → eq→ y=z ( eq→ x=y t) ; eq← = λ t → eq← x=y ( eq← y=z t) } +==-sym : { x y : OD } → x == y → y == x +==-sym x=y = record { eq→ = λ {m} t → eq← x=y t ; eq← = λ {m} t → eq→ x=y t } + ⇔→== : { x y : OD } → ( {z : Ordinal } → def x z ⇔ def y z) → x == y eq→ ( ⇔→== {x} {y} eq ) {z} m = proj1 eq m eq← ( ⇔→== {x} {y} eq ) {z} m = proj2 eq m +-- next assumptions are our axiom +-- it defines a subset of OD, which is called HOD, usually defined as +-- HOD = { x | TC x ⊆ OD } +-- where TC x is a transitive clusure of x, i.e. Union of all elemnts of all subset of x + +record ODAxiom : Set (suc n) where + -- OD can be iso to a subset of Ordinal ( by means of Godel Set ) + field + od→ord : OD → Ordinal + ord→od : Ordinal → OD + c<→o< : {x y : OD } → def y ( od→ord x ) → od→ord x o< od→ord y + oiso : {x : OD } → ord→od ( od→ord x ) ≡ x + diso : {x : Ordinal } → od→ord ( ord→od x ) ≡ x + ==→o≡ : { x y : OD } → (x == y) → x ≡ y + -- supermum as Replacement Axiom ( corresponding Ordinal of OD has maximum ) + sup-o : ( OD → Ordinal ) → Ordinal + sup-o< : { ψ : OD → Ordinal } → ∀ {x : OD } → ψ x o< sup-o ψ + -- contra-position of mimimulity of supermum required in Power Set Axiom which we don't use + -- sup-x : {n : Level } → ( OD → Ordinal ) → Ordinal + -- sup-lb : {n : Level } → { ψ : OD → Ordinal } → {z : Ordinal } → z o< sup-o ψ → z o< osuc (ψ (sup-x ψ)) + +postulate odAxiom : ODAxiom +open ODAxiom odAxiom + +data One : Set n where + OneObj : One + +-- Ordinals in OD , the maximum +Ords : OD +Ords = record { def = λ x → One } + +maxod : {x : OD} → od→ord x o< od→ord Ords +maxod {x} = c<→o< OneObj + -- Ordinal in OD ( and ZFSet ) Transitive Set Ord : ( a : Ordinal ) → OD Ord a = record { def = λ y → y o< a } @@ -58,30 +93,13 @@ od∅ : OD od∅ = Ord o∅ -postulate - -- OD can be iso to a subset of Ordinal ( by means of Godel Set ) - od→ord : OD → Ordinal - ord→od : Ordinal → OD - c<→o< : {x y : OD } → def y ( od→ord x ) → od→ord x o< od→ord y - oiso : {x : OD } → ord→od ( od→ord x ) ≡ x - diso : {x : Ordinal } → od→ord ( ord→od x ) ≡ x - -- we should prove this in agda, but simply put here - ==→o≡ : { x y : OD } → (x == y) → x ≡ y - -- next assumption causes ∀ x ∋ ∅ . It menas only an ordinal becomes a set - -- o<→c< : {n : Level} {x y : Ordinal } → x o< y → def (ord→od y) x - -- ord→od x ≡ Ord x results the same - -- supermum as Replacement Axiom - sup-o : ( Ordinal → Ordinal ) → Ordinal - sup-o< : { ψ : Ordinal → Ordinal } → ∀ {x : Ordinal } → ψ x o< sup-o ψ - -- contra-position of mimimulity of supermum required in Power Set Axiom - -- sup-x : {n : Level } → ( Ordinal → Ordinal ) → Ordinal - -- sup-lb : {n : Level } → { ψ : Ordinal → Ordinal } → {z : Ordinal } → z o< sup-o ψ → z o< osuc (ψ (sup-x ψ)) - -- mimimul and x∋minimul is an Axiom of choice - minimul : (x : OD ) → ¬ (x == od∅ )→ OD - -- this should be ¬ (x == od∅ )→ ∃ ox → x ∋ Ord ox ( minimum of x ) - x∋minimul : (x : OD ) → ( ne : ¬ (x == od∅ ) ) → def x ( od→ord ( minimul x ne ) ) - -- minimulity (may proved by ε-induction ) - minimul-1 : (x : OD ) → ( ne : ¬ (x == od∅ ) ) → (y : OD ) → ¬ ( def (minimul x ne) (od→ord y)) ∧ (def x (od→ord y) ) + +o<→c<→OD=Ord : ( {x y : Ordinal } → x o< y → def (ord→od y) x ) → {x : OD } → x ≡ Ord (od→ord x) +o<→c<→OD=Ord o<→c< {x} = ==→o≡ ( record { eq→ = lemma1 ; eq← = lemma2 } ) where + lemma1 : {y : Ordinal} → def x y → def (Ord (od→ord x)) y + lemma1 {y} lt = subst ( λ k → k o< od→ord x ) diso (c<→o< {ord→od y} {x} (subst (λ k → def x k ) (sym diso) lt)) + lemma2 : {y : Ordinal} → def (Ord (od→ord x)) y → def x y + lemma2 {y} lt = subst (λ k → def k y ) oiso (o<→c< {y} {od→ord x} lt ) _∋_ : ( a x : OD ) → Set n _∋_ a x = def a ( od→ord x ) @@ -89,9 +107,6 @@ _c<_ : ( x a : OD ) → Set n x c< a = a ∋ x -_c≤_ : OD → OD → Set (suc n) -a c≤ b = (a ≡ b) ∨ ( b ∋ a ) - cseq : {n : Level} → OD → OD cseq x = record { def = λ y → def x (osuc y) } where @@ -99,13 +114,13 @@ def-subst df refl refl = df sup-od : ( OD → OD ) → OD -sup-od ψ = Ord ( sup-o ( λ x → od→ord (ψ (ord→od x ))) ) +sup-od ψ = Ord ( sup-o ( λ x → od→ord (ψ x)) ) -sup-c< : ( ψ : OD → OD ) → ∀ {x : OD } → def ( sup-od ψ ) (od→ord ( ψ x )) -sup-c< ψ {x} = def-subst {_} {_} {Ord ( sup-o ( λ x → od→ord (ψ (ord→od x ))) )} {od→ord ( ψ x )} +sup-c< : ( ψ : OD → OD ) → ∀ {x : OD } → def ( sup-od ψ ) (od→ord ( ψ x )) +sup-c< ψ {x} = def-subst {_} {_} {Ord ( sup-o ( λ x → od→ord (ψ x)) )} {od→ord ( ψ x )} lemma refl (cong ( λ k → od→ord (ψ k) ) oiso) where - lemma : od→ord (ψ (ord→od (od→ord x))) o< sup-o (λ x → od→ord (ψ (ord→od x))) - lemma = subst₂ (λ j k → j o< k ) refl diso (o<-subst sup-o< refl (sym diso) ) + lemma : od→ord (ψ (ord→od (od→ord x))) o< sup-o (λ x → od→ord (ψ x)) + lemma = subst₂ (λ j k → j o< k ) refl diso (o<-subst (sup-o< ) refl (sym diso) ) otrans : {n : Level} {a x y : Ordinal } → def (Ord a) x → def (Ord x) y → def (Ord a) y otrans x<a y<x = ordtrans y<x x<a @@ -113,6 +128,7 @@ def→o< : {X : OD } → {x : Ordinal } → def X x → x o< od→ord X def→o< {X} {x} lt = o<-subst {_} {_} {x} {od→ord X} ( c<→o< ( def-subst {X} {x} lt (sym oiso) (sym diso) )) diso diso + -- avoiding lv != Zero error orefl : { x : OD } → { y : Ordinal } → od→ord x ≡ y → od→ord x ≡ y orefl refl = refl @@ -131,13 +147,10 @@ ord→== : { x y : OD } → od→ord x ≡ od→ord y → x == y ord→== {x} {y} eq = ==-iso (lemma (od→ord x) (od→ord y) (orefl eq)) where lemma : ( ox oy : Ordinal ) → ox ≡ oy → (ord→od ox) == (ord→od oy) - lemma ox ox refl = eq-refl + lemma ox ox refl = ==-refl o≡→== : { x y : Ordinal } → x ≡ y → ord→od x == ord→od y -o≡→== {x} {.x} refl = eq-refl - -c≤-refl : {n : Level} → ( x : OD ) → x c≤ x -c≤-refl x = case1 refl +o≡→== {x} {.x} refl = ==-refl o∅≡od∅ : ord→od (o∅ ) ≡ od∅ o∅≡od∅ = ==→o≡ lemma where @@ -156,7 +169,7 @@ eq← ∅0 {w} lt = lift (¬x<0 lt) ∅< : { x y : OD } → def x (od→ord y ) → ¬ ( x == od∅ ) -∅< {x} {y} d eq with eq→ (eq-trans eq (eq-sym ∅0) ) d +∅< {x} {y} d eq with eq→ (==-trans eq (==-sym ∅0) ) d ∅< {x} {y} d eq | lift () ∅6 : { x : OD } → ¬ ( x ∋ x ) -- no Russel paradox @@ -173,105 +186,6 @@ _,_ : OD → OD → OD x , y = record { def = λ t → (t ≡ od→ord x ) ∨ ( t ≡ od→ord y ) } -- Ord (omax (od→ord x) (od→ord y)) -<_,_> : (x y : OD) → OD -< x , y > = (x , x ) , (x , y ) - -exg-pair : { x y : OD } → (x , y ) == ( y , x ) -exg-pair {x} {y} = record { eq→ = left ; eq← = right } where - left : {z : Ordinal} → def (x , y) z → def (y , x) z - left (case1 t) = case2 t - left (case2 t) = case1 t - right : {z : Ordinal} → def (y , x) z → def (x , y) z - right (case1 t) = case2 t - right (case2 t) = case1 t - -==-trans : { x y z : OD } → x == y → y == z → x == z -==-trans x=y y=z = record { eq→ = λ {m} t → eq→ y=z (eq→ x=y t) ; eq← = λ {m} t → eq← x=y (eq← y=z t) } - -==-sym : { x y : OD } → x == y → y == x -==-sym x=y = record { eq→ = λ {m} t → eq← x=y t ; eq← = λ {m} t → eq→ x=y t } - -ord≡→≡ : { x y : OD } → od→ord x ≡ od→ord y → x ≡ y -ord≡→≡ eq = subst₂ (λ j k → j ≡ k ) oiso oiso ( cong ( λ k → ord→od k ) eq ) - -od≡→≡ : { x y : Ordinal } → ord→od x ≡ ord→od y → x ≡ y -od≡→≡ eq = subst₂ (λ j k → j ≡ k ) diso diso ( cong ( λ k → od→ord k ) eq ) - -eq-prod : { x x' y y' : OD } → x ≡ x' → y ≡ y' → < x , y > ≡ < x' , y' > -eq-prod refl refl = refl - -prod-eq : { x x' y y' : OD } → < x , y > == < x' , y' > → (x ≡ x' ) ∧ ( y ≡ y' ) -prod-eq {x} {x'} {y} {y'} eq = record { proj1 = lemmax ; proj2 = lemmay } where - lemma0 : {x y z : OD } → ( x , x ) == ( z , y ) → x ≡ y - lemma0 {x} {y} eq with trio< (od→ord x) (od→ord y) - lemma0 {x} {y} eq | tri< a ¬b ¬c with eq← eq {od→ord y} (case2 refl) - lemma0 {x} {y} eq | tri< a ¬b ¬c | case1 s = ⊥-elim ( o<¬≡ (sym s) a ) - lemma0 {x} {y} eq | tri< a ¬b ¬c | case2 s = ⊥-elim ( o<¬≡ (sym s) a ) - lemma0 {x} {y} eq | tri≈ ¬a b ¬c = ord≡→≡ b - lemma0 {x} {y} eq | tri> ¬a ¬b c with eq← eq {od→ord y} (case2 refl) - lemma0 {x} {y} eq | tri> ¬a ¬b c | case1 s = ⊥-elim ( o<¬≡ s c ) - lemma0 {x} {y} eq | tri> ¬a ¬b c | case2 s = ⊥-elim ( o<¬≡ s c ) - lemma2 : {x y z : OD } → ( x , x ) == ( z , y ) → z ≡ y - lemma2 {x} {y} {z} eq = trans (sym (lemma0 lemma3 )) ( lemma0 eq ) where - lemma3 : ( x , x ) == ( y , z ) - lemma3 = ==-trans eq exg-pair - lemma1 : {x y : OD } → ( x , x ) == ( y , y ) → x ≡ y - lemma1 {x} {y} eq with eq← eq {od→ord y} (case2 refl) - lemma1 {x} {y} eq | case1 s = ord≡→≡ (sym s) - lemma1 {x} {y} eq | case2 s = ord≡→≡ (sym s) - lemma4 : {x y z : OD } → ( x , y ) == ( x , z ) → y ≡ z - lemma4 {x} {y} {z} eq with eq← eq {od→ord z} (case2 refl) - lemma4 {x} {y} {z} eq | case1 s with ord≡→≡ s -- x ≡ z - ... | refl with lemma2 (==-sym eq ) - ... | refl = refl - lemma4 {x} {y} {z} eq | case2 s = ord≡→≡ (sym s) -- y ≡ z - lemmax : x ≡ x' - lemmax with eq→ eq {od→ord (x , x)} (case1 refl) - lemmax | case1 s = lemma1 (ord→== s ) -- (x,x)≡(x',x') - lemmax | case2 s with lemma2 (ord→== s ) -- (x,x)≡(x',y') with x'≡y' - ... | refl = lemma1 (ord→== s ) - lemmay : y ≡ y' - lemmay with lemmax - ... | refl with lemma4 eq -- with (x,y)≡(x,y') - ... | eq1 = lemma4 (ord→== (cong (λ k → od→ord k ) eq1 )) - -ppp : { p : Set n } { a : OD } → record { def = λ x → p } ∋ a → p -ppp {p} {a} d = d - --- --- Axiom of choice in intutionistic logic implies the exclude middle --- https://plato.stanford.edu/entries/axiom-choice/#AxiChoLog --- -p∨¬p : ( p : Set n ) → p ∨ ( ¬ p ) -- assuming axiom of choice -p∨¬p p with is-o∅ ( od→ord ( record { def = λ x → p } )) -p∨¬p p | yes eq = case2 (¬p eq) where - ps = record { def = λ x → p } - lemma : ps == od∅ → p → ⊥ - lemma eq p0 = ¬x<0 {od→ord ps} (eq→ eq p0 ) - ¬p : (od→ord ps ≡ o∅) → p → ⊥ - ¬p eq = lemma ( subst₂ (λ j k → j == k ) oiso o∅≡od∅ ( o≡→== eq )) -p∨¬p p | no ¬p = case1 (ppp {p} {minimul ps (λ eq → ¬p (eqo∅ eq))} lemma) where - ps = record { def = λ x → p } - eqo∅ : ps == od∅ → od→ord ps ≡ o∅ - eqo∅ eq = subst (λ k → od→ord ps ≡ k) ord-od∅ ( cong (λ k → od→ord k ) (==→o≡ eq)) - lemma : ps ∋ minimul ps (λ eq → ¬p (eqo∅ eq)) - lemma = x∋minimul ps (λ eq → ¬p (eqo∅ eq)) - -decp : ( p : Set n ) → Dec p -- assuming axiom of choice -decp p with p∨¬p p -decp p | case1 x = yes x -decp p | case2 x = no x - -double-neg-eilm : {A : Set n} → ¬ ¬ A → A -- we don't have this in intutionistic logic -double-neg-eilm {A} notnot with decp A -- assuming axiom of choice -... | yes p = p -... | no ¬p = ⊥-elim ( notnot ¬p ) - -OrdP : ( x : Ordinal ) ( y : OD ) → Dec ( Ord x ∋ y ) -OrdP x y with trio< x (od→ord y) -OrdP x y | tri< a ¬b ¬c = no ¬c -OrdP x y | tri≈ ¬a refl ¬c = no ( o<¬≡ refl ) -OrdP x y | tri> ¬a ¬b c = yes c -- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) -- postulate f-extensionality : { n : Level} → Relation.Binary.PropositionalEquality.Extensionality n (suc n) @@ -285,33 +199,38 @@ ZFSubset A x = record { def = λ y → def A y ∧ def x y } -- roughly x = A → Set Def : (A : OD ) → OD -Def A = Ord ( sup-o ( λ x → od→ord ( ZFSubset A (ord→od x )) ) ) +Def A = Ord ( sup-o ( λ x → od→ord ( ZFSubset A x) ) ) +-- _⊆_ : ( A B : OD ) → ∀{ x : OD } → Set n +-- _⊆_ A B {x} = A ∋ x → B ∋ x -_⊆_ : ( A B : OD ) → ∀{ x : OD } → Set n -_⊆_ A B {x} = A ∋ x → B ∋ x +record _⊆_ ( A B : OD ) : Set (suc n) where + field + incl : { x : OD } → A ∋ x → B ∋ x + +open _⊆_ infixr 220 _⊆_ -subset-lemma : {A x y : OD } → ( x ∋ y → ZFSubset A x ∋ y ) ⇔ ( _⊆_ x A {y} ) -subset-lemma {A} {x} {y} = record { - proj1 = λ z lt → proj1 (z lt) - ; proj2 = λ x⊆A lt → record { proj1 = x⊆A lt ; proj2 = lt } +subset-lemma : {A x : OD } → ( {y : OD } → x ∋ y → ZFSubset A x ∋ y ) ⇔ ( x ⊆ A ) +subset-lemma {A} {x} = record { + proj1 = λ lt → record { incl = λ x∋z → proj1 (lt x∋z) } + ; proj2 = λ x⊆A lt → record { proj1 = incl x⊆A lt ; proj2 = lt } } --- Constructible Set on α --- Def X = record { def = λ y → ∀ (x : OD ) → y < X ∧ y < od→ord x } --- L (Φ 0) = Φ --- L (OSuc lv n) = { Def ( L n ) } --- L (Φ (Suc n)) = Union (L α) (α < Φ (Suc n) ) --- L : {n : Level} → (α : Ordinal ) → OD --- L record { lv = Zero ; ord = (Φ .0) } = od∅ --- L record { lv = lx ; ord = (OSuc lv ox) } = Def ( L ( record { lv = lx ; ord = ox } ) ) --- L record { lv = (Suc lx) ; ord = (Φ (Suc lx)) } = -- Union ( L α ) --- cseq ( Ord (od→ord (L (record { lv = lx ; ord = Φ lx })))) +open import Data.Unit --- L0 : {n : Level} → (α : Ordinal ) → L (osuc α) ∋ L α --- L1 : {n : Level} → (α β : Ordinal ) → α o< β → ∀ (x : OD ) → L α ∋ x → L β ∋ x +ε-induction : { ψ : OD → Set (suc n)} + → ( {x : OD } → ({ y : OD } → x ∋ y → ψ y ) → ψ x ) + → (x : OD ) → ψ x +ε-induction {ψ} ind x = subst (λ k → ψ k ) oiso (ε-induction-ord (osuc (od→ord x)) <-osuc ) where + induction : (ox : Ordinal) → ((oy : Ordinal) → oy o< ox → ψ (ord→od oy)) → ψ (ord→od ox) + induction ox prev = ind ( λ {y} lt → subst (λ k → ψ k ) oiso (prev (od→ord y) (o<-subst (c<→o< lt) refl diso ))) + ε-induction-ord : (ox : Ordinal) { oy : Ordinal } → oy o< ox → ψ (ord→od oy) + ε-induction-ord ox {oy} lt = TransFinite {λ oy → ψ (ord→od oy)} induction oy + +-- minimal-2 : (x : OD ) → ( ne : ¬ (x == od∅ ) ) → (y : OD ) → ¬ ( def (minimal x ne) (od→ord y)) ∧ (def x (od→ord y) ) +-- minimal-2 x ne y = contra-position ( ε-induction (λ {z} ind → {!!} ) x ) ( λ p → {!!} ) OD→ZF : ZF OD→ZF = record { @@ -327,11 +246,11 @@ ; infinite = infinite ; isZF = isZF } where - ZFSet = OD + ZFSet = OD -- is less than Ords because of maxod Select : (X : OD ) → ((x : OD ) → Set n ) → OD Select X ψ = record { def = λ x → ( def X x ∧ ψ ( ord→od x )) } Replace : OD → (OD → OD ) → OD - Replace X ψ = record { def = λ x → (x o< sup-o ( λ x → od→ord (ψ (ord→od x )))) ∧ def (in-codomain X ψ) x } + Replace X ψ = record { def = λ x → (x o< sup-o ( λ x → od→ord (ψ x))) ∧ def (in-codomain X ψ) x } _∩_ : ( A B : ZFSet ) → ZFSet A ∩ B = record { def = λ x → def A x ∧ def B x } Union : OD → OD @@ -340,8 +259,8 @@ A ∈ B = B ∋ A Power : OD → OD Power A = Replace (Def (Ord (od→ord A))) ( λ x → A ∩ x ) - ｛_｝ : ZFSet → ZFSet - ｛ x ｝ = ( x , x ) + -- ｛_｝ : ZFSet → ZFSet + -- ｛ x ｝ = ( x , x ) -- it works but we don't use data infinite-d : ( x : Ordinal ) → Set n where iφ : infinite-d o∅ @@ -355,7 +274,7 @@ -- infixr 230 _∩_ _∪_ isZF : IsZF (OD ) _∋_ _==_ od∅ _,_ Union Power Select Replace infinite isZF = record { - isEquivalence = record { refl = eq-refl ; sym = eq-sym; trans = eq-trans } + isEquivalence = record { refl = ==-refl ; sym = ==-sym; trans = ==-trans } ; pair→ = pair→ ; pair← = pair← ; union→ = union→ @@ -364,14 +283,14 @@ ; power→ = power→ ; power← = power← ; extensionality = λ {A} {B} {w} → extensionality {A} {B} {w} - -- ; ε-induction = {!!} + ; ε-induction = ε-induction ; infinity∅ = infinity∅ ; infinity = infinity ; selection = λ {X} {ψ} {y} → selection {X} {ψ} {y} ; replacement← = replacement← ; replacement→ = replacement→ - ; choice-func = choice-func - ; choice = choice + -- ; choice-func = choice-func + -- ; choice = choice } where pair→ : ( x y t : ZFSet ) → (x , y) ∋ t → ( t == x ) ∨ ( t == y ) @@ -382,28 +301,24 @@ pair← x y t (case1 t==x) = case1 (cong (λ k → od→ord k ) (==→o≡ t==x)) pair← x y t (case2 t==y) = case2 (cong (λ k → od→ord k ) (==→o≡ t==y)) - -- pair0 : (A B : OD ) → ((A , B) ∋ A) ∧ ((A , B) ∋ B) - -- proj1 (pair A B ) = omax-x (od→ord A) (od→ord B) - -- proj2 (pair A B ) = omax-y (od→ord A) (od→ord B) - empty : (x : OD ) → ¬ (od∅ ∋ x) empty x = ¬x<0 - o<→c< : {x y : Ordinal } {z : OD }→ x o< y → _⊆_ (Ord x) (Ord y) {z} - o<→c< lt lt1 = ordtrans lt1 lt + o<→c< : {x y : Ordinal } → x o< y → (Ord x) ⊆ (Ord y) + o<→c< lt = record { incl = λ z → ordtrans z lt } - ⊆→o< : {x y : Ordinal } → (∀ (z : OD) → _⊆_ (Ord x) (Ord y) {z} ) → x o< osuc y + ⊆→o< : {x y : Ordinal } → (Ord x) ⊆ (Ord y) → x o< osuc y ⊆→o< {x} {y} lt with trio< x y ⊆→o< {x} {y} lt | tri< a ¬b ¬c = ordtrans a <-osuc ⊆→o< {x} {y} lt | tri≈ ¬a b ¬c = subst ( λ k → k o< osuc y) (sym b) <-osuc - ⊆→o< {x} {y} lt | tri> ¬a ¬b c with lt (ord→od y) (o<-subst c (sym diso) refl ) + ⊆→o< {x} {y} lt | tri> ¬a ¬b c with (incl lt) (o<-subst c (sym diso) refl ) ... | ttt = ⊥-elim ( o<¬≡ refl (o<-subst ttt diso refl )) union→ : (X z u : OD) → (X ∋ u) ∧ (u ∋ z) → Union X ∋ z union→ X z u xx not = ⊥-elim ( not (od→ord u) ( record { proj1 = proj1 xx ; proj2 = subst ( λ k → def k (od→ord z)) (sym oiso) (proj2 xx) } )) union← : (X z : OD) (X∋z : Union X ∋ z) → ¬ ( (u : OD ) → ¬ ((X ∋ u) ∧ (u ∋ z ))) - union← X z UX∋z = TransFiniteExists _ lemma UX∋z where + union← X z UX∋z = FExists _ lemma UX∋z where lemma : {y : Ordinal} → def X y ∧ def (ord→od y) (od→ord z) → ¬ ((u : OD) → ¬ (X ∋ u) ∧ (u ∋ z)) lemma {y} xx not = not (ord→od y) record { proj1 = subst ( λ k → def X k ) (sym diso) (proj1 xx ) ; proj2 = proj2 xx } @@ -434,7 +349,6 @@ --- First consider ordinals in OD --- --- ZFSubset A x = record { def = λ y → def A y ∧ def x y } subset of A - --- Power X = ord→od ( sup-o ( λ x → od→ord ( ZFSubset A (ord→od x )) ) ) Power X is a sup of all subset of A -- -- ∩-≡ : { a b : OD } → ({x : OD } → (a ∋ x → b ∋ x)) → a == ( b ∩ a ) @@ -443,8 +357,10 @@ proj1 = def-subst {_} {_} {b} {x} (inc (def-subst {_} {_} {a} {_} x<a refl (sym diso) )) refl diso } ; eq← = λ {x} x<a∩b → proj2 x<a∩b } -- - -- we have t ∋ x → A ∋ x means t is a subset of A, that is ZFSubset A t == t - -- Power A is a sup of ZFSubset A t, so Power A ∋ t + -- Transitive Set case + -- we have t ∋ x → Ord a ∋ x means t is a subset of Ord a, that is ZFSubset (Ord a) t == t + -- Def (Ord a) is a sup of ZFSubset (Ord a) t, so Def (Ord a) ∋ t + -- Def A = Ord ( sup-o ( λ x → od→ord ( ZFSubset A (ord→od x )) ) ) -- ord-power← : (a : Ordinal ) (t : OD) → ({x : OD} → (t ∋ x → (Ord a) ∋ x)) → Def (Ord a) ∋ t ord-power← a t t→A = def-subst {_} {_} {Def (Ord a)} {od→ord t} @@ -457,18 +373,19 @@ lemma1 : {a : Ordinal } { t : OD } → (eq : ZFSubset (Ord a) t == t) → od→ord (ZFSubset (Ord a) (ord→od (od→ord t))) ≡ od→ord t lemma1 {a} {t} eq = subst (λ k → od→ord (ZFSubset (Ord a) k) ≡ od→ord t ) (sym oiso) (cong (λ k → od→ord k ) (==→o≡ eq )) - lemma : od→ord (ZFSubset (Ord a) (ord→od (od→ord t)) ) o< sup-o (λ x → od→ord (ZFSubset (Ord a) (ord→od x))) - lemma = sup-o< + lemma : od→ord (ZFSubset (Ord a) (ord→od (od→ord t)) ) o< sup-o (λ x → od→ord (ZFSubset (Ord a) x)) + lemma = sup-o< -- - -- Every set in OD is a subset of Ordinals + -- Every set in OD is a subset of Ordinals, so make Def (Ord (od→ord A)) first + -- then replace of all elements of the Power set by A ∩ y -- -- Power A = Replace (Def (Ord (od→ord A))) ( λ y → A ∩ y ) -- we have oly double negation form because of the replacement axiom -- power→ : ( A t : OD) → Power A ∋ t → {x : OD} → t ∋ x → ¬ ¬ (A ∋ x) - power→ A t P∋t {x} t∋x = TransFiniteExists _ lemma5 lemma4 where + power→ A t P∋t {x} t∋x = FExists _ lemma5 lemma4 where a = od→ord A lemma2 : ¬ ( (y : OD) → ¬ (t == (A ∩ y))) lemma2 = replacement→ (Def (Ord (od→ord A))) t P∋t @@ -486,8 +403,6 @@ lemma0 {x} t∋x = c<→o< (t→A t∋x) lemma3 : Def (Ord a) ∋ t lemma3 = ord-power← a t lemma0 - lt1 : od→ord (A ∩ ord→od (od→ord t)) o< sup-o (λ x → od→ord (A ∩ ord→od x)) - lt1 = sup-o< {λ x → od→ord (A ∩ ord→od x)} {od→ord t} lemma4 : (A ∩ ord→od (od→ord t)) ≡ t lemma4 = let open ≡-Reasoning in begin A ∩ ord→od (od→ord t) @@ -496,26 +411,23 @@ ≡⟨ sym (==→o≡ ( ∩-≡ t→A )) ⟩ t ∎ - lemma1 : od→ord t o< sup-o (λ x → od→ord (A ∩ ord→od x)) - lemma1 = subst (λ k → od→ord k o< sup-o (λ x → od→ord (A ∩ ord→od x))) - lemma4 (sup-o< {λ x → od→ord (A ∩ ord→od x)} {od→ord t}) + lemma1 : od→ord t o< sup-o (λ x → od→ord (A ∩ x)) + lemma1 = subst (λ k → od→ord k o< sup-o (λ x → od→ord (A ∩ x))) + lemma4 (sup-o< {λ x → od→ord (A ∩ x)} ) lemma2 : def (in-codomain (Def (Ord (od→ord A))) (_∩_ A)) (od→ord t) lemma2 not = ⊥-elim ( not (od→ord t) (record { proj1 = lemma3 ; proj2 = lemma6 }) ) where lemma6 : od→ord t ≡ od→ord (A ∩ ord→od (od→ord t)) lemma6 = cong ( λ k → od→ord k ) (==→o≡ (subst (λ k → t == (A ∩ k)) (sym oiso) ( ∩-≡ t→A ))) - -- assuming axiom of choice - regularity : (x : OD) (not : ¬ (x == od∅)) → - (x ∋ minimul x not) ∧ (Select (minimul x not) (λ x₁ → (minimul x not ∋ x₁) ∧ (x ∋ x₁)) == od∅) - proj1 (regularity x not ) = x∋minimul x not - proj2 (regularity x not ) = record { eq→ = lemma1 ; eq← = λ {y} d → lemma2 {y} d } where - lemma1 : {x₁ : Ordinal} → def (Select (minimul x not) (λ x₂ → (minimul x not ∋ x₂) ∧ (x ∋ x₂))) x₁ → def od∅ x₁ - lemma1 {x₁} s = ⊥-elim ( minimul-1 x not (ord→od x₁) lemma3 ) where - lemma3 : def (minimul x not) (od→ord (ord→od x₁)) ∧ def x (od→ord (ord→od x₁)) - lemma3 = record { proj1 = def-subst {_} {_} {minimul x not} {_} (proj1 s) refl (sym diso) - ; proj2 = proj2 (proj2 s) } - lemma2 : {x₁ : Ordinal} → def od∅ x₁ → def (Select (minimul x not) (λ x₂ → (minimul x not ∋ x₂) ∧ (x ∋ x₂))) x₁ - lemma2 {y} d = ⊥-elim (empty (ord→od y) (def-subst {_} {_} {od∅} {od→ord (ord→od y)} d refl (sym diso) )) + ord⊆power : (a : Ordinal) → (Ord (osuc a)) ⊆ (Power (Ord a)) + ord⊆power a = record { incl = λ {x} lt → power← (Ord a) x (lemma lt) } where + lemma : {x y : OD} → od→ord x o< osuc a → x ∋ y → Ord a ∋ y + lemma lt y<x with osuc-≡< lt + lemma lt y<x | case1 refl = c<→o< y<x + lemma lt y<x | case2 x<a = ordtrans (c<→o< y<x) x<a + + continuum-hyphotheis : (a : Ordinal) → Set (suc n) + continuum-hyphotheis a = Power (Ord a) ⊆ Ord (osuc a) extensionality0 : {A B : OD } → ((z : OD) → (A ∋ z) ⇔ (B ∋ z)) → A == B eq→ (extensionality0 {A} {B} eq ) {x} d = def-iso {A} {B} (sym diso) (proj1 (eq (ord→od x))) d @@ -541,59 +453,6 @@ ≡ od→ord (Union (x , (x , x))) lemma = cong (λ k → od→ord (Union ( k , ( k , k ) ))) oiso - -- Axiom of choice ( is equivalent to the existence of minimul in our case ) - -- ∀ X [ ∅ ∉ X → (∃ f : X → ⋃ X ) → ∀ A ∈ X ( f ( A ) ∈ A ) ] - choice-func : (X : OD ) → {x : OD } → ¬ ( x == od∅ ) → ( X ∋ x ) → OD - choice-func X {x} not X∋x = minimul x not - choice : (X : OD ) → {A : OD } → ( X∋A : X ∋ A ) → (not : ¬ ( A == od∅ )) → A ∋ choice-func X not X∋A - choice X {A} X∋A not = x∋minimul A not - - --- - --- With assuption of OD is ordered, p ∨ ( ¬ p ) <=> axiom of choice - --- - record choiced ( X : OD) : Set (suc n) where - field - a-choice : OD - is-in : X ∋ a-choice - - choice-func' : (X : OD ) → (p∨¬p : ( p : Set (suc n)) → p ∨ ( ¬ p )) → ¬ ( X == od∅ ) → choiced X - choice-func' X p∨¬p not = have_to_find where - ψ : ( ox : Ordinal ) → Set (suc n) - ψ ox = (( x : Ordinal ) → x o< ox → ( ¬ def X x )) ∨ choiced X - lemma-ord : ( ox : Ordinal ) → ψ ox - lemma-ord ox = TransFinite {ψ} induction ox where - ∋-p : (A x : OD ) → Dec ( A ∋ x ) - ∋-p A x with p∨¬p (Lift (suc n) ( A ∋ x )) - ∋-p A x | case1 (lift t) = yes t - ∋-p A x | case2 t = no (λ x → t (lift x )) - ∀-imply-or : {A : Ordinal → Set n } {B : Set (suc n) } - → ((x : Ordinal ) → A x ∨ B) → ((x : Ordinal ) → A x) ∨ B - ∀-imply-or {A} {B} ∀AB with p∨¬p (Lift ( suc n ) ((x : Ordinal ) → A x)) - ∀-imply-or {A} {B} ∀AB | case1 (lift t) = case1 t - ∀-imply-or {A} {B} ∀AB | case2 x = case2 (lemma (λ not → x (lift not ))) where - lemma : ¬ ((x : Ordinal ) → A x) → B - lemma not with p∨¬p B - lemma not | case1 b = b - lemma not | case2 ¬b = ⊥-elim (not (λ x → dont-orb (∀AB x) ¬b )) - induction : (x : Ordinal) → ((y : Ordinal) → y o< x → ψ y) → ψ x - induction x prev with ∋-p X ( ord→od x) - ... | yes p = case2 ( record { a-choice = ord→od x ; is-in = p } ) - ... | no ¬p = lemma where - lemma1 : (y : Ordinal) → (y o< x → def X y → ⊥) ∨ choiced X - lemma1 y with ∋-p X (ord→od y) - lemma1 y | yes y<X = case2 ( record { a-choice = ord→od y ; is-in = y<X } ) - lemma1 y | no ¬y<X = case1 ( λ lt y<X → ¬y<X (subst (λ k → def X k ) (sym diso) y<X ) ) - lemma : ((y : Ordinals.ord O) → (O Ordinals.o< y) x → def X y → ⊥) ∨ choiced X - lemma = ∀-imply-or lemma1 - have_to_find : choiced X - have_to_find with lemma-ord (od→ord X ) - have_to_find | t = dont-or t ¬¬X∋x where - ¬¬X∋x : ¬ ((x : Ordinal) → x o< (od→ord X) → def X x → ⊥) - ¬¬X∋x nn = not record { - eq→ = λ {x} lt → ⊥-elim (nn x (def→o< lt) lt) - ; eq← = λ {x} lt → ⊥-elim ( ¬x<0 lt ) - } - Union = ZF.Union OD→ZF Power = ZF.Power OD→ZF
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/ODC.agda Sun Jun 07 20:31:30 2020 +0900 @@ -0,0 +1,96 @@ +open import Level +open import Ordinals +module ODC {n : Level } (O : Ordinals {n} ) where + +open import zf +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.Nullary +open import Relation.Binary +open import Relation.Binary.Core + +open import logic +open import nat +import OD + +open inOrdinal O +open OD O +open OD.OD +open OD._==_ +open ODAxiom odAxiom + +postulate + -- mimimul and x∋minimal is an Axiom of choice + minimal : (x : OD ) → ¬ (x == od∅ )→ OD + -- this should be ¬ (x == od∅ )→ ∃ ox → x ∋ Ord ox ( minimum of x ) + x∋minimal : (x : OD ) → ( ne : ¬ (x == od∅ ) ) → def x ( od→ord ( minimal x ne ) ) + -- minimality (may proved by ε-induction ) + minimal-1 : (x : OD ) → ( ne : ¬ (x == od∅ ) ) → (y : OD ) → ¬ ( def (minimal x ne) (od→ord y)) ∧ (def x (od→ord y) ) + + +-- +-- Axiom of choice in intutionistic logic implies the exclude middle +-- https://plato.stanford.edu/entries/axiom-choice/#AxiChoLog +-- + +ppp : { p : Set n } { a : OD } → record { def = λ x → p } ∋ a → p +ppp {p} {a} d = d + +p∨¬p : ( p : Set n ) → p ∨ ( ¬ p ) -- assuming axiom of choice +p∨¬p p with is-o∅ ( od→ord ( record { def = λ x → p } )) +p∨¬p p | yes eq = case2 (¬p eq) where + ps = record { def = λ x → p } + lemma : ps == od∅ → p → ⊥ + lemma eq p0 = ¬x<0 {od→ord ps} (eq→ eq p0 ) + ¬p : (od→ord ps ≡ o∅) → p → ⊥ + ¬p eq = lemma ( subst₂ (λ j k → j == k ) oiso o∅≡od∅ ( o≡→== eq )) +p∨¬p p | no ¬p = case1 (ppp {p} {minimal ps (λ eq → ¬p (eqo∅ eq))} lemma) where + ps = record { def = λ x → p } + eqo∅ : ps == od∅ → od→ord ps ≡ o∅ + eqo∅ eq = subst (λ k → od→ord ps ≡ k) ord-od∅ ( cong (λ k → od→ord k ) (==→o≡ eq)) + lemma : ps ∋ minimal ps (λ eq → ¬p (eqo∅ eq)) + lemma = x∋minimal ps (λ eq → ¬p (eqo∅ eq)) + +decp : ( p : Set n ) → Dec p -- assuming axiom of choice +decp p with p∨¬p p +decp p | case1 x = yes x +decp p | case2 x = no x + +double-neg-eilm : {A : Set n} → ¬ ¬ A → A -- we don't have this in intutionistic logic +double-neg-eilm {A} notnot with decp A -- assuming axiom of choice +... | yes p = p +... | no ¬p = ⊥-elim ( notnot ¬p ) + +OrdP : ( x : Ordinal ) ( y : OD ) → Dec ( Ord x ∋ y ) +OrdP x y with trio< x (od→ord y) +OrdP x y | tri< a ¬b ¬c = no ¬c +OrdP x y | tri≈ ¬a refl ¬c = no ( o<¬≡ refl ) +OrdP x y | tri> ¬a ¬b c = yes c + +open import zfc + +OD→ZFC : ZFC +OD→ZFC = record { + ZFSet = OD + ; _∋_ = _∋_ + ; _≈_ = _==_ + ; ∅ = od∅ + ; Select = Select + ; isZFC = isZFC + } where + -- infixr 200 _∈_ + -- infixr 230 _∩_ _∪_ + isZFC : IsZFC (OD ) _∋_ _==_ od∅ Select + isZFC = record { + choice-func = choice-func ; + choice = choice + } where + -- Axiom of choice ( is equivalent to the existence of minimal in our case ) + -- ∀ X [ ∅ ∉ X → (∃ f : X → ⋃ X ) → ∀ A ∈ X ( f ( A ) ∈ A ) ] + choice-func : (X : OD ) → {x : OD } → ¬ ( x == od∅ ) → ( X ∋ x ) → OD + choice-func X {x} not X∋x = minimal x not + choice : (X : OD ) → {A : OD } → ( X∋A : X ∋ A ) → (not : ¬ ( A == od∅ )) → A ∋ choice-func X not X∋A + choice X {A} X∋A not = x∋minimal A not +
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/OPair.agda Sun Jun 07 20:31:30 2020 +0900 @@ -0,0 +1,128 @@ +open import Level +open import Ordinals +module OPair {n : Level } (O : Ordinals {n}) where + +open import zf +open import logic +import OD + +open import Relation.Nullary +open import Relation.Binary +open import Data.Empty +open import Relation.Binary +open import Relation.Binary.Core +open import Relation.Binary.PropositionalEquality +open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ; _⊔_ to _n⊔_ ) + +open inOrdinal O +open OD O +open OD.OD +open ODAxiom odAxiom + +open _∧_ +open _∨_ +open Bool + +open _==_ + +<_,_> : (x y : OD) → OD +< x , y > = (x , x ) , (x , y ) + +exg-pair : { x y : OD } → (x , y ) == ( y , x ) +exg-pair {x} {y} = record { eq→ = left ; eq← = right } where + left : {z : Ordinal} → def (x , y) z → def (y , x) z + left (case1 t) = case2 t + left (case2 t) = case1 t + right : {z : Ordinal} → def (y , x) z → def (x , y) z + right (case1 t) = case2 t + right (case2 t) = case1 t + +ord≡→≡ : { x y : OD } → od→ord x ≡ od→ord y → x ≡ y +ord≡→≡ eq = subst₂ (λ j k → j ≡ k ) oiso oiso ( cong ( λ k → ord→od k ) eq ) + +od≡→≡ : { x y : Ordinal } → ord→od x ≡ ord→od y → x ≡ y +od≡→≡ eq = subst₂ (λ j k → j ≡ k ) diso diso ( cong ( λ k → od→ord k ) eq ) + +eq-prod : { x x' y y' : OD } → x ≡ x' → y ≡ y' → < x , y > ≡ < x' , y' > +eq-prod refl refl = refl + +prod-eq : { x x' y y' : OD } → < x , y > == < x' , y' > → (x ≡ x' ) ∧ ( y ≡ y' ) +prod-eq {x} {x'} {y} {y'} eq = record { proj1 = lemmax ; proj2 = lemmay } where + lemma0 : {x y z : OD } → ( x , x ) == ( z , y ) → x ≡ y + lemma0 {x} {y} eq with trio< (od→ord x) (od→ord y) + lemma0 {x} {y} eq | tri< a ¬b ¬c with eq← eq {od→ord y} (case2 refl) + lemma0 {x} {y} eq | tri< a ¬b ¬c | case1 s = ⊥-elim ( o<¬≡ (sym s) a ) + lemma0 {x} {y} eq | tri< a ¬b ¬c | case2 s = ⊥-elim ( o<¬≡ (sym s) a ) + lemma0 {x} {y} eq | tri≈ ¬a b ¬c = ord≡→≡ b + lemma0 {x} {y} eq | tri> ¬a ¬b c with eq← eq {od→ord y} (case2 refl) + lemma0 {x} {y} eq | tri> ¬a ¬b c | case1 s = ⊥-elim ( o<¬≡ s c ) + lemma0 {x} {y} eq | tri> ¬a ¬b c | case2 s = ⊥-elim ( o<¬≡ s c ) + lemma2 : {x y z : OD } → ( x , x ) == ( z , y ) → z ≡ y + lemma2 {x} {y} {z} eq = trans (sym (lemma0 lemma3 )) ( lemma0 eq ) where + lemma3 : ( x , x ) == ( y , z ) + lemma3 = ==-trans eq exg-pair + lemma1 : {x y : OD } → ( x , x ) == ( y , y ) → x ≡ y + lemma1 {x} {y} eq with eq← eq {od→ord y} (case2 refl) + lemma1 {x} {y} eq | case1 s = ord≡→≡ (sym s) + lemma1 {x} {y} eq | case2 s = ord≡→≡ (sym s) + lemma4 : {x y z : OD } → ( x , y ) == ( x , z ) → y ≡ z + lemma4 {x} {y} {z} eq with eq← eq {od→ord z} (case2 refl) + lemma4 {x} {y} {z} eq | case1 s with ord≡→≡ s -- x ≡ z + ... | refl with lemma2 (==-sym eq ) + ... | refl = refl + lemma4 {x} {y} {z} eq | case2 s = ord≡→≡ (sym s) -- y ≡ z + lemmax : x ≡ x' + lemmax with eq→ eq {od→ord (x , x)} (case1 refl) + lemmax | case1 s = lemma1 (ord→== s ) -- (x,x)≡(x',x') + lemmax | case2 s with lemma2 (ord→== s ) -- (x,x)≡(x',y') with x'≡y' + ... | refl = lemma1 (ord→== s ) + lemmay : y ≡ y' + lemmay with lemmax + ... | refl with lemma4 eq -- with (x,y)≡(x,y') + ... | eq1 = lemma4 (ord→== (cong (λ k → od→ord k ) eq1 )) + +data ord-pair : (p : Ordinal) → Set n where + pair : (x y : Ordinal ) → ord-pair ( od→ord ( < ord→od x , ord→od y > ) ) + +ZFProduct : OD +ZFProduct = record { def = λ x → ord-pair x } + +-- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) +-- eq-pair : { x x' y y' : Ordinal } → x ≡ x' → y ≡ y' → pair x y ≅ pair x' y' +-- eq-pair refl refl = HE.refl + +pi1 : { p : Ordinal } → ord-pair p → Ordinal +pi1 ( pair x y) = x + +π1 : { p : OD } → ZFProduct ∋ p → OD +π1 lt = ord→od (pi1 lt ) + +pi2 : { p : Ordinal } → ord-pair p → Ordinal +pi2 ( pair x y ) = y + +π2 : { p : OD } → ZFProduct ∋ p → OD +π2 lt = ord→od (pi2 lt ) + +op-cons : { ox oy : Ordinal } → ZFProduct ∋ < ord→od ox , ord→od oy > +op-cons {ox} {oy} = pair ox oy + +p-cons : ( x y : OD ) → ZFProduct ∋ < x , y > +p-cons x y = def-subst {_} {_} {ZFProduct} {od→ord (< x , y >)} (pair (od→ord x) ( od→ord y )) refl ( + let open ≡-Reasoning in begin + od→ord < ord→od (od→ord x) , ord→od (od→ord y) > + ≡⟨ cong₂ (λ j k → od→ord < j , k >) oiso oiso ⟩ + od→ord < x , y > + ∎ ) + +op-iso : { op : Ordinal } → (q : ord-pair op ) → od→ord < ord→od (pi1 q) , ord→od (pi2 q) > ≡ op +op-iso (pair ox oy) = refl + +p-iso : { x : OD } → (p : ZFProduct ∋ x ) → < π1 p , π2 p > ≡ x +p-iso {x} p = ord≡→≡ (op-iso p) + +p-pi1 : { x y : OD } → (p : ZFProduct ∋ < x , y > ) → π1 p ≡ x +p-pi1 {x} {y} p = proj1 ( prod-eq ( ord→== (op-iso p) )) + +p-pi2 : { x y : OD } → (p : ZFProduct ∋ < x , y > ) → π2 p ≡ y +p-pi2 {x} {y} p = proj2 ( prod-eq ( ord→== (op-iso p))) +
--- a/Ordinals.agda Thu Aug 29 16:18:37 2019 +0900 +++ b/Ordinals.agda Sun Jun 07 20:31:30 2020 +0900 @@ -193,9 +193,9 @@ } } - TransFiniteExists : {m l : Level} → ( ψ : Ordinal → Set m ) + FExists : {m l : Level} → ( ψ : Ordinal → Set m ) → {p : Set l} ( P : { y : Ordinal } → ψ y → ¬ p ) → (exists : ¬ (∀ y → ¬ ( ψ y ) )) → ¬ p - TransFiniteExists {m} {l} ψ {p} P = contra-position ( λ p y ψy → P {y} ψy p ) + FExists {m} {l} ψ {p} P = contra-position ( λ p y ψy → P {y} ψy p )
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/README.md Sun Jun 07 20:31:30 2020 +0900 @@ -0,0 +1,1 @@ +zf-in-agda.ind \ No newline at end of file
--- a/cardinal.agda Thu Aug 29 16:18:37 2019 +0900 +++ b/cardinal.agda Sun Jun 07 20:31:30 2020 +0900 @@ -5,6 +5,8 @@ open import zf open import logic import OD +import ODC +import OPair 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 @@ -16,6 +18,8 @@ open inOrdinal O open OD O open OD.OD +open OPair O +open ODAxiom odAxiom open _∧_ open _∨_ @@ -24,50 +28,10 @@ -- we have to work on Ordinal to keep OD Level n -- since we use p∨¬p which works only on Level n --- < x , y > = (x , x) , (x , y) - -data ord-pair : (p : Ordinal) → Set n where - pair : (x y : Ordinal ) → ord-pair ( od→ord ( < ord→od x , ord→od y > ) ) - -ZFProduct : OD -ZFProduct = record { def = λ x → ord-pair x } - --- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) --- eq-pair : { x x' y y' : Ordinal } → x ≡ x' → y ≡ y' → pair x y ≅ pair x' y' --- eq-pair refl refl = HE.refl - -pi1 : { p : Ordinal } → ord-pair p → Ordinal -pi1 ( pair x y) = x - -π1 : { p : OD } → ZFProduct ∋ p → Ordinal -π1 lt = pi1 lt - -pi2 : { p : Ordinal } → ord-pair p → Ordinal -pi2 ( pair x y ) = y - -π2 : { p : OD } → ZFProduct ∋ p → Ordinal -π2 lt = pi2 lt - -p-cons : ( x y : OD ) → ZFProduct ∋ < x , y > -p-cons x y = def-subst {_} {_} {ZFProduct} {od→ord (< x , y >)} (pair (od→ord x) ( od→ord y )) refl ( - let open ≡-Reasoning in begin - od→ord < ord→od (od→ord x) , ord→od (od→ord y) > - ≡⟨ cong₂ (λ j k → od→ord < j , k >) oiso oiso ⟩ - od→ord < x , y > - ∎ ) - - -p-iso1 : { ox oy : Ordinal } → ZFProduct ∋ < ord→od ox , ord→od oy > -p-iso1 {ox} {oy} = pair ox oy - -p-iso : { x : OD } → (p : ZFProduct ∋ x ) → < ord→od (π1 p) , ord→od (π2 p) > ≡ x -p-iso {x} p = ord≡→≡ (lemma p) where - lemma : { op : Ordinal } → (q : ord-pair op ) → od→ord < ord→od (pi1 q) , ord→od (pi2 q) > ≡ op - lemma (pair ox oy) = refl ∋-p : (A x : OD ) → Dec ( A ∋ x ) -∋-p A x with p∨¬p ( A ∋ x ) +∋-p A x with ODC.p∨¬p O ( A ∋ x ) ∋-p A x | case1 t = yes t ∋-p A x | case2 t = no t @@ -88,7 +52,6 @@ -- power→ : ( A t : OD) → Power A ∋ t → {x : OD} → t ∋ x → ¬ ¬ (A ∋ x) - func→od : (f : Ordinal → Ordinal ) → ( dom : OD ) → OD func→od f dom = Replace dom ( λ x → < x , ord→od (f (od→ord x)) > ) @@ -98,17 +61,17 @@ func→od∈Func-1 : Func dom cod ∋ func→od func-1 dom od→func : { dom cod : OD } → {f : Ordinal } → def (Func dom cod ) f → Func←cd {dom} {cod} {f} -od→func {dom} {cod} {f} lt = record { func-1 = λ x → sup-o ( λ y → lemma x y ) ; func→od∈Func-1 = record { proj1 = {!!} ; proj2 = {!!} } } where +od→func {dom} {cod} {f} lt = record { func-1 = λ x → sup-o ( λ y → lemma x {!!} ) ; func→od∈Func-1 = record { proj1 = {!!} ; proj2 = {!!} } } where lemma : Ordinal → Ordinal → Ordinal lemma x y with IsZF.power→ isZF (dom ⊗ cod) (ord→od f) (subst (λ k → def (Power (dom ⊗ cod)) k ) (sym diso) lt ) | ∋-p (ord→od f) (ord→od y) lemma x y | p | no n = o∅ - lemma x y | p | yes f∋y = lemma2 (proj1 (double-neg-eilm ( p {ord→od y} f∋y ))) where -- p : {y : OD} → f ∋ y → ¬ ¬ (dom ⊗ cod ∋ y) + lemma x y | p | yes f∋y = lemma2 (proj1 (ODC.double-neg-eilm O ( p {ord→od y} f∋y ))) where -- p : {y : OD} → f ∋ y → ¬ ¬ (dom ⊗ cod ∋ y) lemma2 : {p : Ordinal} → ord-pair p → Ordinal - lemma2 (pair x1 y1) with decp ( x1 ≡ x) + lemma2 (pair x1 y1) with ODC.decp O ( x1 ≡ x) lemma2 (pair x1 y1) | yes p = y1 lemma2 (pair x1 y1) | no ¬p = o∅ fod : OD - fod = Replace dom ( λ x → < x , ord→od (sup-o ( λ y → lemma (od→ord x) y )) > ) + fod = Replace dom ( λ x → < x , ord→od (sup-o ( λ y → lemma (od→ord x) {!!} )) > ) open Func←cd @@ -139,7 +102,7 @@ open Onto -onto-restrict : {X Y Z : OD} → Onto X Y → ({x : OD} → _⊆_ Z Y {x}) → Onto X Z +onto-restrict : {X Y Z : OD} → Onto X Y → Z ⊆ Y → Onto X Z onto-restrict {X} {Y} {Z} onto Z⊆Y = record { xmap = xmap1 ; ymap = zmap @@ -167,15 +130,15 @@ cardinal : (X : OD ) → Cardinal X cardinal X = record { - cardinal = sup-o ( λ x → proj1 ( cardinal-p x) ) + cardinal = sup-o ( λ x → proj1 ( cardinal-p {!!}) ) ; conto = onto ; cmax = cmax } where cardinal-p : (x : Ordinal ) → ( Ordinal ∧ Dec (Onto X (Ord x) ) ) - cardinal-p x with p∨¬p ( Onto X (Ord x) ) + cardinal-p x with ODC.p∨¬p O ( Onto X (Ord x) ) cardinal-p x | case1 True = record { proj1 = x ; proj2 = yes True } cardinal-p x | case2 False = record { proj1 = o∅ ; proj2 = no False } - S = sup-o (λ x → proj1 (cardinal-p x)) + S = sup-o (λ x → proj1 (cardinal-p {!!})) lemma1 : (x : Ordinal) → ((y : Ordinal) → y o< x → Lift (suc n) (y o< (osuc S) → Onto X (Ord y))) → Lift (suc n) (x o< (osuc S) → Onto X (Ord x) ) lemma1 x prev with trio< x (osuc S) @@ -192,9 +155,9 @@ ... | lift t = t <-osuc cmax : (y : Ordinal) → S o< y → ¬ Onto X (Ord y) cmax y lt ontoy = o<> lt (o<-subst {_} {_} {y} {S} - (sup-o< {λ x → proj1 ( cardinal-p x)}{y} ) lemma refl ) where + (sup-o< {λ x → proj1 ( cardinal-p {!!})}{{!!}} ) lemma refl ) where lemma : proj1 (cardinal-p y) ≡ y - lemma with p∨¬p ( Onto X (Ord y) ) + lemma with ODC.p∨¬p O ( Onto X (Ord y) ) lemma | case1 x = refl lemma | case2 not = ⊥-elim ( not ontoy )
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/fig/ODandOrdinals.svg Sun Jun 07 20:31:30 2020 +0900 @@ -0,0 +1,192 @@ +<?xml version="1.0" encoding="UTF-8" standalone="no"?> +<!DOCTYPE svg PUBLIC "-//W3C//DTD SVG 1.1//EN" "http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd"> +<svg version="1.1" xmlns="http://www.w3.org/2000/svg" xmlns:xl="http://www.w3.org/1999/xlink" xmlns:dc="http://purl.org/dc/elements/1.1/" viewBox="68 87 578 643" width="578" height="643"> + <defs> + <marker orient="auto" overflow="visible" markerUnits="strokeWidth" id="FilledArrow_Marker" stroke-linejoin="miter" stroke-miterlimit="10" viewBox="-5 -3 6 6" markerWidth="6" markerHeight="6" color="black"> + <g> + <path d="M -3.7333333 0 L 0 1.4 L 0 -1.4 Z" fill="currentColor" stroke="currentColor" stroke-width="1"/> + </g> + </marker> + <font-face font-family="Helvetica Neue" font-size="22" panose-1="2 0 5 3 0 0 0 2 0 4" units-per-em="1000" underline-position="-100" underline-thickness="50" slope="0" x-height="517" cap-height="714" ascent="951.9958" descent="-212.99744" font-weight="400"> + <font-face-src> + <font-face-name name="HelveticaNeue"/> + </font-face-src> + </font-face> + <marker orient="auto" overflow="visible" markerUnits="strokeWidth" id="FilledArrow_Marker_2" stroke-linejoin="miter" stroke-miterlimit="10" viewBox="-1 -3 6 6" markerWidth="6" markerHeight="6" color="black"> + <g> + <path d="M 3.7333333 0 L 0 -1.4 L 0 1.4 Z" fill="currentColor" stroke="currentColor" stroke-width="1"/> + </g> + </marker> + </defs> + <metadata> Produced by OmniGraffle 7.12.1 + <dc:date>2019-11-28 04:44:00 +0000</dc:date> + </metadata> + <g id="Canvas_1" stroke-dasharray="none" stroke="none" fill="none" stroke-opacity="1" fill-opacity="1"> + <title>Canvas 1</title> + <rect fill="white" x="68" y="87" width="578" height="643"/> + <g id="Canvas_1: Layer 1"> + <title>Layer 1</title> + <g id="Graphic_6"> + <path d="M 123 129 L 150.21835 251 L 177.4367 129 Z" fill="white"/> + <path d="M 123 129 L 150.21835 251 L 177.4367 129 Z" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/> + </g> + <g id="Graphic_7"> + <path d="M 123 251 L 150.21835 373 L 177.4367 251 Z" fill="white"/> + <path d="M 123 251 L 150.21835 373 L 177.4367 251 Z" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/> + </g> + <g id="Graphic_8"> + <path d="M 123 373 L 150.21835 495 L 177.4367 373 Z" fill="white"/> + <path d="M 123 373 L 150.21835 495 L 177.4367 373 Z" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/> + </g> + <g id="Graphic_9"> + <path d="M 123 495 L 150.21835 617 L 177.4367 495 Z" fill="white"/> + <path d="M 123 495 L 150.21835 617 L 177.4367 495 Z" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/> + </g> + <g id="Graphic_10"> + <ellipse cx="270.5" cy="478.5" rx="14.5000231695775" ry="82.5001318269064" fill="white"/> + <ellipse cx="270.5" cy="478.5" rx="14.5000231695775" ry="82.5001318269064" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/> + </g> + <g id="Graphic_12"> + <ellipse cx="293.5" cy="280.5" rx="14.5000231695775" ry="82.5001318269065" fill="white"/> + <ellipse cx="293.5" cy="280.5" rx="14.5000231695775" ry="82.5001318269065" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/> + </g> + <g id="Graphic_13"> + <circle cx="154.5" cy="181.5" r="6.50001038636232" fill="black"/> + <circle cx="154.5" cy="181.5" r="6.50001038636232" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/> + </g> + <g id="Graphic_14"> + <circle cx="154.5" cy="272.5" r="6.50001038636234" fill="black"/> + <circle cx="154.5" cy="272.5" r="6.50001038636234" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/> + </g> + <g id="Graphic_15"> + <circle cx="154.5" cy="304.5" r="6.50001038636234" fill="black"/> + <circle cx="154.5" cy="304.5" r="6.50001038636234" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/> + </g> + <g id="Graphic_16"> + <circle cx="154.5" cy="395.5" r="6.50001038636233" fill="black"/> + <circle cx="154.5" cy="395.5" r="6.50001038636233" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/> + </g> + <g id="Graphic_18"> + <circle cx="154.5" cy="424.5" r="6.50001038636234" fill="black"/> + <circle cx="154.5" cy="424.5" r="6.50001038636234" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/> + </g> + <g id="Line_19"> + <line x1="173.9379" y1="409.40815" x2="254.63666" y2="467.1495" marker-start="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/> + </g> + <g id="Line_20"> + <line x1="176.16929" y1="434.5874" x2="254.55825" y2="471.07884" marker-start="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/> + </g> + <g id="Line_21"> + <line x1="173.96816" y1="195.3658" x2="277.63543" y2="269.20077" marker-start="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/> + </g> + <g id="Line_22"> + <line x1="178.3606" y1="273.87327" x2="277.5009" y2="279.5792" marker-start="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/> + </g> + <g id="Line_23"> + <line x1="178.05217" y1="300.43344" x2="277.50804" y2="283.2612" marker-start="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/> + </g> + <g id="Graphic_24"> + <circle cx="150.21835" cy="525.5" r="6.50001038636231" fill="black"/> + <circle cx="150.21835" cy="525.5" r="6.50001038636231" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/> + </g> + <g id="Line_25"> + <line x1="162.28478" y1="504.8674" x2="278.23874" y2="306.5955" marker-start="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/> + </g> + <g id="Graphic_26"> + <text transform="translate(119.245 633)" fill="black"> + <tspan font-family="Helvetica Neue" font-size="22" font-weight="400" fill="black" x="0" y="21">Ordinal</tspan> + </text> + </g> + <g id="Graphic_27"> + <text transform="translate(224.256 584)" fill="black"> + <tspan font-family="Helvetica Neue" font-size="22" font-weight="400" fill="black" x="10.989" y="21">Ordinal</tspan> + <tspan font-family="Helvetica Neue" font-size="22" font-weight="400" fill="black" x="5968559e-19" y="47.616">Definable</tspan> + </text> + </g> + <g id="Graphic_47"> + <path d="M 426 129 L 453.21835 251 L 480.4367 129 Z" fill="white"/> + <path d="M 426 129 L 453.21835 251 L 480.4367 129 Z" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/> + </g> + <g id="Graphic_46"> + <path d="M 426 251 L 453.21835 373 L 480.4367 251 Z" fill="white"/> + <path d="M 426 251 L 453.21835 373 L 480.4367 251 Z" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/> + </g> + <g id="Graphic_45"> + <path d="M 426 373 L 453.21835 495 L 480.4367 373 Z" fill="white"/> + <path d="M 426 373 L 453.21835 495 L 480.4367 373 Z" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/> + </g> + <g id="Graphic_44"> + <path d="M 426 495 L 453.21835 617 L 480.4367 495 Z" fill="white"/> + <path d="M 426 495 L 453.21835 617 L 480.4367 495 Z" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/> + </g> + <g id="Graphic_43"> + <ellipse cx="573.5" cy="478.5" rx="14.5000231695775" ry="82.5001318269064" fill="white"/> + <ellipse cx="573.5" cy="478.5" rx="14.5000231695775" ry="82.5001318269064" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/> + </g> + <g id="Graphic_42"> + <ellipse cx="596.5" cy="280.5" rx="14.5000231695775" ry="82.5001318269065" fill="white"/> + <ellipse cx="596.5" cy="280.5" rx="14.5000231695775" ry="82.5001318269065" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/> + </g> + <g id="Graphic_41"> + <circle cx="457.5" cy="181.5" r="6.50001038636232" fill="black"/> + <circle cx="457.5" cy="181.5" r="6.50001038636232" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/> + </g> + <g id="Graphic_40"> + <circle cx="457.5" cy="272.5" r="6.50001038636234" fill="black"/> + <circle cx="457.5" cy="272.5" r="6.50001038636234" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/> + </g> + <g id="Graphic_39"> + <circle cx="457.5" cy="304.5" r="6.50001038636234" fill="black"/> + <circle cx="457.5" cy="304.5" r="6.50001038636234" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/> + </g> + <g id="Graphic_38"> + <circle cx="457.5" cy="395.5" r="6.50001038636232" fill="black"/> + <circle cx="457.5" cy="395.5" r="6.50001038636232" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/> + </g> + <g id="Graphic_37"> + <circle cx="457.5" cy="424.5" r="6.50001038636234" fill="black"/> + <circle cx="457.5" cy="424.5" r="6.50001038636234" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/> + </g> + <g id="Graphic_31"> + <circle cx="453.21835" cy="525.5" r="6.50001038636233" fill="black"/> + <circle cx="453.21835" cy="525.5" r="6.50001038636233" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/> + </g> + <g id="Graphic_29"> + <text transform="translate(422.245 633)" fill="black"> + <tspan font-family="Helvetica Neue" font-size="22" font-weight="400" fill="black" x="0" y="21">Ordinal</tspan> + </text> + </g> + <g id="Graphic_28"> + <text transform="translate(527.256 584)" fill="black"> + <tspan font-family="Helvetica Neue" font-size="22" font-weight="400" fill="black" x="10.989" y="21">Ordinal</tspan> + <tspan font-family="Helvetica Neue" font-size="22" font-weight="400" fill="black" x="5968559e-19" y="47.616">Definable</tspan> + </text> + </g> + <g id="Line_48"> + <path d="M 604.7609 469.93216 C 612.0671 467.7524 618.9377 465.6045 624.34375 463.84375 C 637.5514 459.5421 639.2045 425.7619 633.77734 414.5703 C 628.35015 403.3787 602 397 574 385 C 546 373 545 374 507 358 C 469 342 416.78393 326.70416 398 311 C 379.21607 295.29584 381.79114 286.83255 383 279 C 384.20886 271.16745 393.904 266.09114 404 266 C 410.17797 265.94423 421.8459 265.70735 434.2442 267.17386" marker-end="url(#FilledArrow_Marker_2)" marker-start="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/> + </g> + <g id="Graphic_49"> + <circle cx="453.21835" cy="149.5" r="6.50001038636234" fill="black"/> + <circle cx="453.21835" cy="149.5" r="6.50001038636234" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/> + </g> + <g id="Line_50"> + <path d="M 623.554 268.5201 C 625.4985 267.62867 627.6082 266.779 630 266 C 643.2077 261.69835 643.4272 246.1916 638 235 C 632.5728 223.8084 607 201 559 210 C 511 219 518.4367 243 480.4367 227 C 442.4367 211 413.62724 203.75242 394.8433 188.04826 C 376.0594 172.3441 378.63445 163.88081 379.8433 156.04826 C 381.05217 148.21571 390.7473 143.1394 400.8433 143.04826 C 408.3246 142.98073 423.85655 142.6476 438.987 145.39538" marker-end="url(#FilledArrow_Marker_2)" marker-start="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/> + </g> + <g id="Graphic_52"> + <text transform="translate(73.912 92.608)" fill="black"> + <tspan font-family="Helvetica Neue" font-size="22" font-weight="400" fill="black" x="18474111e-20" y="21">OD contains Ordinals</tspan> + </text> + </g> + <g id="Graphic_53"> + <text transform="translate(377.204 92.608)" fill="black"> + <tspan font-family="Helvetica Neue" font-size="22" font-weight="400" fill="black" x="7105427e-19" y="21">OD has a name in Ordinals</tspan> + </text> + </g> + <g id="Graphic_54"> + <text transform="translate(220 698)" fill="black"> + <tspan font-family="Helvetica Neue" font-size="22" font-weight="400" fill="black" x="0" y="21">all arrows have to be acyclic</tspan> + </text> + </g> + </g> + </g> +</svg>
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/fig/Sets.svg Sun Jun 07 20:31:30 2020 +0900 @@ -0,0 +1,84 @@ +<?xml version="1.0" encoding="UTF-8" standalone="no"?> +<!DOCTYPE svg PUBLIC "-//W3C//DTD SVG 1.1//EN" "http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd"> +<svg version="1.1" xmlns="http://www.w3.org/2000/svg" xmlns:xl="http://www.w3.org/1999/xlink" xmlns:dc="http://purl.org/dc/elements/1.1/" viewBox="26 93 572 303" width="572" height="303"> + <defs> + <font-face font-family="Hiragino Sans" font-size="18" panose-1="2 11 3 0 0 0 0 0 0 0" units-per-em="1000" underline-position="-75" underline-thickness="50" slope="0" x-height="545" cap-height="766" ascent="880.0018" descent="-120.00024" font-weight="300"> + <font-face-src> + <font-face-name name="HiraginoSans-W3"/> + </font-face-src> + </font-face> + <font-face font-family="Helvetica Neue" font-size="18" panose-1="2 0 5 3 0 0 0 2 0 4" units-per-em="1000" underline-position="-100" underline-thickness="50" slope="0" x-height="517" cap-height="714" ascent="951.9958" descent="-212.99744" font-weight="400"> + <font-face-src> + <font-face-name name="HelveticaNeue"/> + </font-face-src> + </font-face> + </defs> + <metadata> Produced by OmniGraffle 7.12.1 + <dc:date>2019-11-27 13:34:32 +0000</dc:date> + </metadata> + <g id="Canvas_1" stroke-dasharray="none" stroke="none" fill="none" stroke-opacity="1" fill-opacity="1"> + <title>Canvas 1</title> + <rect fill="white" x="26" y="93" width="572" height="303"/> + <g id="Canvas_1: Layer 1"> + <title>Layer 1</title> + <g id="Graphic_2"> + <text transform="translate(133 98.00003)" fill="black"> + <tspan font-family="Hiragino Sans" font-size="18" font-weight="300" fill="black" x="0" y="16">様々な集合</tspan> + </text> + </g> + <g id="Graphic_4"> + <text transform="translate(108 137.00001)" fill="black"> + <tspan font-family="Hiragino Sans" font-size="18" font-weight="300" fill="black" x="0" y="16">順序数の公理を満たすもの。自然数の延長</tspan> + </text> + </g> + <g id="Graphic_5"> + <text transform="translate(108 176)" fill="black"> + <tspan font-family="Hiragino Sans" font-size="18" font-weight="300" fill="black" x="0" y="16">一つ一つ増やす。無限回繰り返して、それを全部。</tspan> + <tspan font-family="Hiragino Sans" font-size="18" font-weight="300" fill="black" x="0" y="43.00002">また一つ一つ増やすを繰り返して得られるもの</tspan> + </text> + </g> + <g id="Graphic_6"> + <text transform="translate(108 233.696)" fill="black"> + <tspan font-family="Hiragino Sans" font-size="18" font-weight="300" fill="black" x="0" y="16">述語で定義されるものを集めるのを繰り返して作られるもの</tspan> + </text> + </g> + <g id="Graphic_7"> + <text transform="translate(108 281.99994)" fill="black"> + <tspan font-family="Hiragino Sans" font-size="18" font-weight="300" fill="black" x="0" y="16">順序数上の方程式を満たす順序数の集合</tspan> + <tspan font-family="Hiragino Sans" font-size="18" font-weight="300" fill="black" x="0" y="43.00002">階層化されていない</tspan> + </text> + </g> + <g id="Graphic_8"> + <text transform="translate(31.59 137.00001)" fill="black"> + <tspan font-family="Helvetica Neue" font-size="18" font-weight="400" fill="black" x="0" y="17">Ordinal</tspan> + </text> + </g> + <g id="Graphic_9"> + <text transform="translate(54.936 176)" fill="black"> + <tspan font-family="Helvetica Neue" font-size="18" font-weight="400" fill="black" x="0" y="17">V</tspan> + </text> + </g> + <g id="Graphic_10"> + <text transform="translate(53.23 281.99994)" fill="black"> + <tspan font-family="Helvetica Neue" font-size="18" font-weight="400" fill="black" x="0" y="17">OD</tspan> + </text> + </g> + <g id="Graphic_11"> + <text transform="translate(55.816 233.696)" fill="black"> + <tspan font-family="Helvetica Neue" font-size="18" font-weight="400" fill="black" x="8144596e-19" y="17">L</tspan> + </text> + </g> + <g id="Graphic_12"> + <text transform="translate(51.174 336)" fill="black"> + <tspan font-family="Helvetica Neue" font-size="18" font-weight="400" fill="black" x="2.502" y="17">Set </tspan> + </text> + </g> + <g id="Graphic_13"> + <text transform="translate(108 336)" fill="black"> + <tspan font-family="Hiragino Sans" font-size="18" font-weight="300" fill="black" x="0" y="16">型。集まりではなく、値の種類を区別する記号。’</tspan> + <tspan font-family="Hiragino Sans" font-size="18" font-weight="300" fill="black" x="0" y="43.00002">自身が値になると、一つLevelの高い型を持つ</tspan> + </text> + </g> + </g> + </g> +</svg>
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/fig/axiom-dependency.svg Sun Jun 07 20:31:30 2020 +0900 @@ -0,0 +1,87 @@ +<?xml version="1.0" encoding="UTF-8" standalone="no"?> +<!DOCTYPE svg PUBLIC "-//W3C//DTD SVG 1.1//EN" "http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd"> +<svg xmlns="http://www.w3.org/2000/svg" xmlns:dc="http://purl.org/dc/elements/1.1/" xmlns:xl="http://www.w3.org/1999/xlink" version="1.1" viewBox="28 101 424 224" width="424" height="224"> + <defs> + <font-face font-family="Hiragino Sans" font-size="22" panose-1="2 11 3 0 0 0 0 0 0 0" units-per-em="1000" underline-position="-75" underline-thickness="50" slope="0" x-height="545" cap-height="766" ascent="880.0018" descent="-120.00024" font-weight="300"> + <font-face-src> + <font-face-name name="HiraginoSans-W3"/> + </font-face-src> + </font-face> + <marker orient="auto" overflow="visible" markerUnits="strokeWidth" id="FilledArrow_Marker" stroke-linejoin="miter" stroke-miterlimit="10" viewBox="-1 -4 10 8" markerWidth="10" markerHeight="8" color="black"> + <g> + <path d="M 8 0 L 0 -3 L 0 3 Z" fill="currentColor" stroke="currentColor" stroke-width="1"/> + </g> + </marker> + <marker orient="auto" overflow="visible" markerUnits="strokeWidth" id="FilledArrow_Marker_2" stroke-linejoin="miter" stroke-miterlimit="10" viewBox="-9 -4 10 8" markerWidth="10" markerHeight="8" color="black"> + <g> + <path d="M -8 0 L 0 3 L 0 -3 Z" fill="currentColor" stroke="currentColor" stroke-width="1"/> + </g> + </marker> + </defs> + <metadata> Produced by OmniGraffle 7.12.1 + <dc:date>2020-01-11 11:10:39 +0000</dc:date> + </metadata> + <g id="Canvas_1" stroke-opacity="1" stroke-dasharray="none" stroke="none" fill="none" fill-opacity="1"> + <title>Canvas 1</title> + <rect fill="white" x="28" y="101" width="424" height="224"/> + <g id="Canvas_1: Layer 1"> + <title>Layer 1</title> + <g id="Graphic_18"> + <rect x="30" y="103" width="420" height="166" stroke="gray" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/> + </g> + <g id="Graphic_2"> + <text transform="translate(334.578 126)" fill="black"> + <tspan font-family="Hiragino Sans" font-size="22" font-weight="300" fill="black" x="48316906e-20" y="19">Choice</tspan> + </text> + </g> + <g id="Graphic_3"> + <text transform="translate(347.91 223.00002)" fill="black"> + <tspan font-family="Hiragino Sans" font-size="22" font-weight="300" fill="black" x="14566126e-20" y="19">LEM</tspan> + </text> + </g> + <g id="Graphic_4"> + <text transform="translate(133.323 286)" fill="black"> + <tspan font-family="Hiragino Sans" font-size="22" font-weight="300" fill="black" x="8952838e-19" y="19">Well ordering outside</tspan> + </text> + </g> + <g id="Graphic_7"> + <text transform="translate(83 180)" fill="black"> + <tspan font-family="Hiragino Sans" font-size="22" font-weight="300" fill="black" x="0" y="19">ε-induction</tspan> + </text> + </g> + <g id="Graphic_8"> + <text transform="translate(43.556 126)" fill="black"> + <tspan font-family="Hiragino Sans" font-size="22" font-weight="300" fill="black" x="0" y="19">Strong Regularity</tspan> + </text> + </g> + <g id="Line_9"> + <line x1="240" y1="142.50001" x2="319.678" y2="142.50001" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/> + </g> + <g id="Line_10"> + <line x1="372" y1="164.00002" x2="372" y2="208.10002" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/> + </g> + <g id="Graphic_11"> + <text transform="translate(110.66 223.00002)" fill="black"> + <tspan font-family="Hiragino Sans" font-size="22" font-weight="300" fill="black" x="0" y="19">Well ordering inside</tspan> + </text> + </g> + <g id="Line_12"> + <line x1="218.438" y1="179.55565" x2="319.95423" y2="155.05904" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/> + </g> + <g id="Group_16"> + <g id="Line_14"> + <line x1="240" y1="156" x2="272.71875" y2="188.27344" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/> + </g> + <g id="Line_15"> + <line x1="274" y1="156" x2="240" y2="188.23828" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/> + </g> + </g> + <g id="Line_17"> + <line x1="372" y1="218.00002" x2="372" y2="173.90002" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/> + </g> + <g id="Line_19"> + <line x1="329.6113" y1="169.28897" x2="260.9037" y2="212.71107" marker-end="url(#FilledArrow_Marker)" marker-start="url(#FilledArrow_Marker_2)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/> + </g> + </g> + </g> +</svg>
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/fig/axiom-type.svg Sun Jun 07 20:31:30 2020 +0900 @@ -0,0 +1,149 @@ +<?xml version="1.0" encoding="UTF-8" standalone="no"?> +<!DOCTYPE svg PUBLIC "-//W3C//DTD SVG 1.1//EN" "http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd"> +<svg xmlns="http://www.w3.org/2000/svg" xmlns:dc="http://purl.org/dc/elements/1.1/" xmlns:xl="http://www.w3.org/1999/xlink" version="1.1" viewBox="30 61 586 330" width="586" height="330"> + <defs> + <font-face font-family="Hiragino Sans" font-size="22" panose-1="2 11 3 0 0 0 0 0 0 0" units-per-em="1000" underline-position="-75" underline-thickness="50" slope="0" x-height="545" cap-height="766" ascent="880.0018" descent="-120.00024" font-weight="300"> + <font-face-src> + <font-face-name name="HiraginoSans-W3"/> + </font-face-src> + </font-face> + <font-face font-family="Helvetica Neue" font-size="22" panose-1="2 0 5 3 0 0 0 2 0 4" units-per-em="1000" underline-position="-100" underline-thickness="50" slope="0" x-height="517" cap-height="714" ascent="951.9958" descent="-212.99744" font-weight="400"> + <font-face-src> + <font-face-name name="HelveticaNeue"/> + </font-face-src> + </font-face> + <font-face font-family="Helvetica" font-size="22" units-per-em="1000" underline-position="-75.68359" underline-thickness="49.316406" slope="0" x-height="522.9492" cap-height="717.28516" ascent="770.0195" descent="-229.98047" font-weight="400"> + <font-face-src> + <font-face-name name="Helvetica"/> + </font-face-src> + </font-face> + </defs> + <metadata> Produced by OmniGraffle 7.12.1 + <dc:date>2020-01-11 11:09:31 +0000</dc:date> + </metadata> + <g id="Canvas_1" stroke-opacity="1" stroke-dasharray="none" stroke="none" fill="none" fill-opacity="1"> + <title>Canvas 1</title> + <rect fill="white" x="30" y="61" width="586" height="330"/> + <g id="Canvas_1: Layer 1"> + <title>Layer 1</title> + <g id="Graphic_2"> + <text transform="translate(184.9378 66)" fill="black"> + <tspan font-family="Hiragino Sans" font-size="22" font-weight="300" fill="black" x="19895197e-20" y="19">Axioms of Set theory in Agda</tspan> + </text> + </g> + <g id="Graphic_3"> + <text transform="translate(42.728 147)" fill="black"> + <tspan font-family="Hiragino Sans" font-size="22" font-weight="300" fill="black" x="8526513e-19" y="19">Pure logical</tspan> + </text> + </g> + <g id="Graphic_4"> + <text transform="translate(35 228.358)" fill="black"> + <tspan font-family="Hiragino Sans" font-size="22" font-weight="300" fill="black" x="6963319e-19" y="19">Negation form</tspan> + </text> + </g> + <g id="Graphic_5"> + <text transform="translate(42.728 295)" fill="black"> + <tspan font-family="Hiragino Sans" font-size="22" font-weight="300" fill="black" x="22737368e-20" y="19">Non construtive</tspan> + <tspan font-family="Hiragino Sans" font-size="22" font-weight="300" fill="black" x="18.205" y="52.00002">assumptions</tspan> + </text> + </g> + <g id="Graphic_6"> + <text transform="translate(418.057 127.71603)" fill="black"> + <tspan font-family="Helvetica Neue" font-size="22" font-weight="400" fill="black" x="0" y="21">pair</tspan> + </text> + </g> + <g id="Graphic_7"> + <text transform="translate(315.19725 212.40404)" fill="black"> + <tspan font-family="Helvetica Neue" font-size="22" font-weight="400" fill="black" x="0" y="21">union</tspan> + </text> + </g> + <g id="Graphic_8"> + <text transform="translate(315.2768 109.00002)" fill="black"> + <tspan font-family="Helvetica Neue" font-size="22" font-weight="400" fill="black" x="24868996e-20" y="21">empty</tspan> + </text> + </g> + <g id="Graphic_9"> + <text transform="translate(299.057 255.71603)" fill="black"> + <tspan font-family="Helvetica Neue" font-size="22" font-weight="400" fill="black" x="7993606e-19" y="21">power</tspan> + </text> + </g> + <g id="Graphic_10"> + <text transform="translate(454.8557 286.10003)" fill="black"> + <tspan font-family="Helvetica Neue" font-size="22" font-weight="400" fill="black" x="9094947e-19" y="21">extensionarity</tspan> + </text> + </g> + <g id="Graphic_11"> + <text transform="translate(460.5455 217.10003)" fill="black"> + <tspan font-family="Helvetica Neue" font-size="22" font-weight="400" fill="black" x="45474735e-20" y="21">infinity</tspan> + </text> + </g> + <g id="Graphic_16"> + <text transform="translate(488.237 148.71603)" fill="black"> + <tspan font-family="Helvetica" font-size="22" font-weight="400" fill="black" x="0" y="21">selection</tspan> + </text> + </g> + <g id="Graphic_18"> + <text transform="translate(454.8557 249.02004)" fill="black"> + <tspan font-family="Helvetica" font-size="22" font-weight="400" fill="black" x="0" y="21">replacement</tspan> + </text> + </g> + <g id="Graphic_19"> + <text transform="translate(339.057 358.71603)" fill="black"> + <tspan font-family="Helvetica Neue" font-size="22" font-weight="400" fill="black" x="7531753e-19" y="21">choice</tspan> + </text> + </g> + <g id="Graphic_20"> + <text transform="translate(503.237 184.71603)" fill="black"> + <tspan font-family="Helvetica" font-size="22" font-weight="400" fill="black" x="0" y="21">ε-induction</tspan> + </text> + </g> + <g id="Graphic_21"> + <text transform="translate(478.057 322.71603)" fill="black"> + <tspan font-family="Helvetica" font-size="22" font-weight="400" fill="black" x="0" y="21">regularity</tspan> + </text> + </g> + <g id="Line_23"> + <line x1="174.272" y1="158.8584" x2="413.057" y2="142.6241" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/> + </g> + <g id="Line_24"> + <line x1="174.272" y1="163.21387" x2="483.237" y2="161.91894" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/> + </g> + <g id="Line_25"> + <line x1="174.272" y1="181.47427" x2="310.19725" y2="217.25989" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/> + </g> + <g id="Line_26"> + <line x1="174.272" y1="151.78494" x2="310.2768" y2="128.44731" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/> + </g> + <g id="Line_27"> + <line x1="174.272" y1="175.32412" x2="455.5455" y2="224.03823" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/> + </g> + <g id="Line_29"> + <line x1="174.272" y1="168.67903" x2="498.237" y2="193.25456" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/> + </g> + <g id="Line_30"> + <line x1="198.114" y1="237.807" x2="310.19725" y2="228.40505" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/> + </g> + <g id="Line_31"> + <line x1="198.114" y1="254.2734" x2="294.057" y2="265.02016" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/> + </g> + <g id="Line_32"> + <line x1="198.114" y1="248.45253" x2="449.8557" y2="259.2177" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/> + </g> + <g id="Line_33"> + <line x1="221.748" y1="312.25824" x2="449.8557" y2="273.2318" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/> + </g> + <g id="Line_34"> + <line x1="221.748" y1="300.8768" x2="294.057" y2="279.56114" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/> + </g> + <g id="Line_35"> + <line x1="221.748" y1="344.74433" x2="334.057" y2="365.1827" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/> + </g> + <g id="Line_36"> + <line x1="221.748" y1="329.80394" x2="473.057" y2="334.73102" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/> + </g> + <g id="Line_37"> + <line x1="221.748" y1="321.31552" x2="449.8557" y2="304.74357" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/> + </g> + </g> + </g> +</svg>
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/fig/ord-od-mapping.svg Sun Jun 07 20:31:30 2020 +0900 @@ -0,0 +1,184 @@ +<?xml version="1.0" encoding="UTF-8" standalone="no"?> +<!DOCTYPE svg PUBLIC "-//W3C//DTD SVG 1.1//EN" "http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd"> +<svg version="1.1" xmlns="http://www.w3.org/2000/svg" xmlns:xl="http://www.w3.org/1999/xlink" xmlns:dc="http://purl.org/dc/elements/1.1/" viewBox="37 -5 449 664" width="449" height="664"> + <defs> + <font-face font-family="Helvetica Neue" font-size="22" panose-1="2 0 5 3 0 0 0 2 0 4" units-per-em="1000" underline-position="-100" underline-thickness="50" slope="0" x-height="517" cap-height="714" ascent="951.9958" descent="-212.99744" font-weight="400"> + <font-face-src> + <font-face-name name="HelveticaNeue"/> + </font-face-src> + </font-face> + <font-face font-family="Helvetica Neue" font-size="14" panose-1="2 0 5 3 0 0 0 2 0 4" units-per-em="1000" underline-position="-100" underline-thickness="50" slope="0" x-height="517" cap-height="714" ascent="951.9958" descent="-212.99744" font-weight="400"> + <font-face-src> + <font-face-name name="HelveticaNeue"/> + </font-face-src> + </font-face> + <marker orient="auto" overflow="visible" markerUnits="strokeWidth" id="FilledArrow_Marker" stroke-linejoin="miter" stroke-miterlimit="10" viewBox="-1 -4 10 8" markerWidth="10" markerHeight="8" color="black"> + <g> + <path d="M 8 0 L 0 -3 L 0 3 Z" fill="currentColor" stroke="currentColor" stroke-width="1"/> + </g> + </marker> + </defs> + <metadata> Produced by OmniGraffle 7.12.1 + <dc:date>2019-11-28 05:45:48 +0000</dc:date> + </metadata> + <g id="Canvas_1" stroke-dasharray="none" stroke="none" fill="none" stroke-opacity="1" fill-opacity="1"> + <title>Canvas 1</title> + <rect fill="white" x="37" y="-5" width="449" height="664"/> + <g id="Canvas_1: Layer 1"> + <title>Layer 1</title> + <g id="Graphic_18"> + <path d="M 159 49 L 186.21835 171 L 213.4367 49 Z" fill="white"/> + <path d="M 159 49 L 186.21835 171 L 213.4367 49 Z" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/> + </g> + <g id="Graphic_17"> + <path d="M 159 171 L 186.21835 293 L 213.4367 171 Z" fill="white"/> + <path d="M 159 171 L 186.21835 293 L 213.4367 171 Z" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/> + </g> + <g id="Graphic_16"> + <path d="M 159 293 L 186.21835 415 L 213.4367 293 Z" fill="white"/> + <path d="M 159 293 L 186.21835 415 L 213.4367 293 Z" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/> + </g> + <g id="Graphic_15"> + <path d="M 159 415 L 186.21835 537 L 213.4367 415 Z" fill="white"/> + <path d="M 159 415 L 186.21835 537 L 213.4367 415 Z" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/> + </g> + <g id="Graphic_12"> + <circle cx="186.21835" cy="16.5" r="6.50001038636233" fill="black"/> + <circle cx="186.21835" cy="16.5" r="6.50001038636233" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/> + </g> + <g id="Graphic_6"> + <text transform="translate(155.245 553)" fill="black"> + <tspan font-family="Helvetica Neue" font-size="22" font-weight="400" fill="black" x="0" y="21">Ordinal</tspan> + </text> + </g> + <g id="Graphic_5"> + <text transform="translate(337 536)" fill="black"> + <tspan font-family="Helvetica Neue" font-size="22" font-weight="400" fill="black" x="10.989" y="21">Ordinal</tspan> + <tspan font-family="Helvetica Neue" font-size="22" font-weight="400" fill="black" x="5968559e-19" y="47.616">Definable</tspan> + </text> + </g> + <g id="Graphic_20"> + <text transform="translate(406.77 98.76035)" fill="black"> + <tspan font-family="Helvetica Neue" font-size="14" font-weight="400" fill="black" x="0" y="13">max</tspan> + <tspan font-family="Helvetica Neue" font-size="14" font-weight="400" fill="black" x=".343" y="29.392">= all</tspan> + </text> + </g> + <g id="Graphic_21"> + <text transform="translate(440.722 509.608)" fill="black"> + <tspan font-family="Helvetica Neue" font-size="14" font-weight="400" fill="black" x="0" y="13">empty</tspan> + </text> + </g> + <g id="Graphic_22"> + <text transform="translate(42 .10800171)" fill="black"> + <tspan font-family="Helvetica Neue" font-size="14" font-weight="400" fill="black" x="23.261" y="13">Ordinal</tspan> + <tspan font-family="Helvetica Neue" font-size="14" font-weight="400" fill="black" x="0" y="29.392">max != Ordinal</tspan> + </text> + </g> + <g id="Line_23"> + <line x1="255.471" y1="430.5664" x2="255.471" y2="534.5664" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/> + </g> + <g id="Line_24"> + <line x1="236" y1="180" x2="236" y2="535" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/> + </g> + <g id="Graphic_25"> + <text transform="translate(99 509.608)" fill="black"> + <tspan font-family="Helvetica Neue" font-size="14" font-weight="400" fill="black" x="0" y="13">empty</tspan> + </text> + </g> + <g id="Line_27"> + <line x1="127" y1="535" x2="484.894" y2="535" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/> + </g> + <g id="Line_28"> + <line x1="389" y1="140" x2="255.471" y2="430.5664" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-dasharray="4.0,4.0" stroke-width="1"/> + </g> + <g id="Line_31"> + <line x1="389" y1="140" x2="236" y2="180.9972" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-dasharray="4.0,4.0" stroke-width="1"/> + </g> + <g id="Graphic_32"> + <circle cx="242.5" cy="146.5" r="6.50001038636233" fill="black"/> + <circle cx="242.5" cy="146.5" r="6.50001038636233" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/> + </g> + <g id="Graphic_33"> + <circle cx="255.971" cy="397.5" r="6.50001038636234" fill="black"/> + <circle cx="255.971" cy="397.5" r="6.50001038636234" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/> + </g> + <g id="Graphic_34"> + <circle cx="383.5" cy="115.15234" r="6.50001038636234" fill="black"/> + <circle cx="383.5" cy="115.15234" r="6.50001038636234" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/> + </g> + <g id="Line_35"> + <line x1="250.3103" y1="144.76358" x2="375.6897" y2="116.88876" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/> + </g> + <g id="Line_36"> + <line x1="380.20605" y1="122.44512" x2="259.26495" y2="390.20723" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/> + </g> + <g id="Line_40"> + <line x1="372.3718" y1="630.664" x2="246.9" y2="630.664" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/> + </g> + <g id="Line_39"> + <line x1="188" y1="622.218" x2="365.575" y2="622.218" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/> + </g> + <g id="Graphic_38"> + <text transform="translate(253.792 599.232)" fill="black"> + <tspan font-family="Helvetica Neue" font-size="14" font-weight="400" fill="black" x="0" y="13">non-order preserving</tspan> + </text> + </g> + <g id="Graphic_37"> + <text transform="translate(260.471 636.664)" fill="black"> + <tspan font-family="Helvetica Neue" font-size="14" font-weight="400" fill="black" x="0" y="13">order preserving</tspan> + </text> + </g> + <g id="Line_41"> + <line x1="107" y1="356" x2="107" y2="274.47422" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/> + </g> + <g id="Graphic_44"> + <text transform="translate(45.888 318.13017)" fill="black"> + <tspan font-family="Helvetica Neue" font-size="14" font-weight="400" fill="black" x="4973799e-19" y="13">larger</tspan> + </text> + </g> + <g id="Line_46"> + <line x1="399" y1="370" x2="414.93724" y2="273.84283" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/> + </g> + <g id="Graphic_45"> + <text transform="translate(433.218 318.13017)" fill="black"> + <tspan font-family="Helvetica Neue" font-size="14" font-weight="400" fill="black" x="0" y="13">defined</tspan> + <tspan font-family="Helvetica Neue" font-size="14" font-weight="400" fill="black" x="15.687" y="29.392">by</tspan> + </text> + </g> + <g id="Line_47"> + <line x1="399" y1="450" x2="399" y2="375.9664" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/> + </g> + <g id="Line_48"> + <line x1="416.556" y1="474.9336" x2="416.556" y2="400.9" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/> + </g> + <g id="Line_49"> + <line x1="407.778" y1="507.9336" x2="407.778" y2="433.9" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/> + </g> + <g id="Line_50"> + <line x1="391.54" y1="209.0664" x2="400.23237" y2="153.77986" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/> + </g> + <g id="Line_51"> + <line x1="412" y1="243.9336" x2="412" y2="169.9" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/> + </g> + <g id="Line_52"> + <line x1="391.54" y1="307" x2="391.54" y2="218.9664" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/> + </g> + <g id="Line_53"> + <line x1="416.556" y1="264.07607" x2="431.52065" y2="216.44483" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/> + </g> + <g id="Line_54"> + <line x1="399" y1="366.0664" x2="392.7805" y2="316.82197" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/> + </g> + <g id="Graphic_55"> + <text transform="translate(107 610.272)" fill="black"> + <tspan font-family="Helvetica Neue" font-size="14" font-weight="400" fill="black" x="0" y="13">Total order</tspan> + </text> + </g> + <g id="Graphic_56"> + <text transform="translate(395 614.522)" fill="black"> + <tspan font-family="Helvetica Neue" font-size="14" font-weight="400" fill="black" x="17053026e-20" y="13">Partial order</tspan> + </text> + </g> + </g> + </g> +</svg>
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/fig/set-theory.svg Sun Jun 07 20:31:30 2020 +0900 @@ -0,0 +1,93 @@ +<?xml version="1.0" encoding="UTF-8" standalone="no"?> +<!DOCTYPE svg PUBLIC "-//W3C//DTD SVG 1.1//EN" "http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd"> +<svg xmlns="http://www.w3.org/2000/svg" xmlns:dc="http://purl.org/dc/elements/1.1/" xmlns:xl="http://www.w3.org/1999/xlink" version="1.1" viewBox="38.294 90.49994 434.607 310.5001" width="434.607" height="310.5001"> + <defs> + <font-face font-family="Hiragino Sans" font-size="22" panose-1="2 11 3 0 0 0 0 0 0 0" units-per-em="1000" underline-position="-75" underline-thickness="50" slope="0" x-height="545" cap-height="766" ascent="880.0018" descent="-120.00024" font-weight="300"> + <font-face-src> + <font-face-name name="HiraginoSans-W3"/> + </font-face-src> + </font-face> + <font-face font-family="Hiragino Sans" font-size="16" panose-1="2 11 3 0 0 0 0 0 0 0" units-per-em="1000" underline-position="-75" underline-thickness="50" slope="0" x-height="545" cap-height="766" ascent="880.0018" descent="-120.00024" font-weight="300"> + <font-face-src> + <font-face-name name="HiraginoSans-W3"/> + </font-face-src> + </font-face> + </defs> + <metadata> Produced by OmniGraffle 7.12.1 + <dc:date>2020-01-11 11:07:37 +0000</dc:date> + </metadata> + <g id="Canvas_1" stroke-opacity="1" stroke-dasharray="none" stroke="none" fill="none" fill-opacity="1"> + <title>Canvas 1</title> + <rect fill="white" x="38.294" y="90.49994" width="434.607" height="310.5001"/> + <g id="Canvas_1: Layer 1"> + <title>Layer 1</title> + <g id="Graphic_21"> + <rect x="55" y="323.5" width="172" height="76.000045" stroke="gray" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/> + </g> + <g id="Graphic_22"> + <rect x="278" y="323.5" width="172" height="76.000045" stroke="gray" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/> + </g> + <g id="Graphic_20"> + <rect x="55" y="260.5" width="172" height="59.5" stroke="gray" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/> + </g> + <g id="Graphic_18"> + <rect x="278" y="197.5" width="172" height="122.5" stroke="gray" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/> + </g> + <g id="Graphic_17"> + <rect x="55" y="197.5" width="172" height="59.5" stroke="gray" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/> + </g> + <g id="Graphic_2"> + <text transform="translate(43.294 95.49994)" fill="black"> + <tspan font-family="Hiragino Sans" font-size="22" font-weight="300" fill="black" x="58264504e-20" y="19">primitive set theory</tspan> + </text> + </g> + <g id="Graphic_4"> + <text transform="translate(68.66 138.49996)" fill="black"> + <tspan font-family="Hiragino Sans" font-size="22" font-weight="300" fill="black" x="22.858" y="19">First order</tspan> + <tspan font-family="Hiragino Sans" font-size="22" font-weight="300" fill="black" x="5968559e-19" y="52.00002">predicate logic</tspan> + </text> + </g> + <g id="Graphic_5"> + <text transform="translate(78.849 279.75004)" fill="black"> + <tspan font-family="Hiragino Sans" font-size="22" font-weight="300" fill="black" x="8597567e-19" y="19">Ordinals</tspan> + </text> + </g> + <g id="Graphic_6"> + <text transform="translate(76.954 340.5001)" fill="black"> + <tspan font-family="Hiragino Sans" font-size="22" font-weight="300" fill="black" x="19895197e-20" y="19">Model on ZF</tspan> + </text> + </g> + <g id="Graphic_10"> + <text transform="translate(270.099 171.49999)" fill="black"> + <tspan font-family="Hiragino Sans" font-size="22" font-weight="300" fill="black" x="0" y="19">Higher order logic</tspan> + </text> + </g> + <g id="Graphic_13"> + <text transform="translate(292.522 210.75)" fill="black"> + <tspan font-family="Hiragino Sans" font-size="22" font-weight="300" fill="black" x="8597567e-19" y="19">Ordinals</tspan> + </text> + </g> + <g id="Graphic_14"> + <text transform="translate(292.522 242.25)" fill="black"> + <tspan font-family="Hiragino Sans" font-size="22" font-weight="300" fill="black" x="0" y="19">ZF axioms</tspan> + </text> + </g> + <g id="Graphic_15"> + <text transform="translate(285.475 272.25003)" fill="black"> + <tspan font-family="Hiragino Sans" font-size="16" font-weight="300" fill="black" x="3.573997" y="14">Non constructive</tspan> + <tspan font-family="Hiragino Sans" font-size="16" font-weight="300" fill="black" x="21.437997" y="38.000016">assumptions</tspan> + </text> + </g> + <g id="Graphic_16"> + <text transform="translate(292.522 348.5)" fill="black"> + <tspan font-family="Hiragino Sans" font-size="22" font-weight="300" fill="black" x="0" y="19">Model on OD</tspan> + </text> + </g> + <g id="Graphic_19"> + <text transform="translate(77.021 210.99999)" fill="black"> + <tspan font-family="Hiragino Sans" font-size="22" font-weight="300" fill="black" x="0" y="19">ZF axioms</tspan> + </text> + </g> + </g> + </g> +</svg>
--- a/filter.agda Thu Aug 29 16:18:37 2019 +0900 +++ b/filter.agda Sun Jun 07 20:31:30 2020 +0900 @@ -17,71 +17,76 @@ open inOrdinal O open OD O open OD.OD +open ODAxiom odAxiom open _∧_ open _∨_ open Bool -record Filter ( P max : OD ) : Set (suc n) where +_∩_ : ( A B : OD ) → OD +A ∩ B = record { def = λ x → def A x ∧ def B x } + +_∪_ : ( A B : OD ) → OD +A ∪ B = record { def = λ x → def A x ∨ def B x } + +_＼_ : ( A B : OD ) → OD +A ＼ B = record { def = λ x → def A x ∧ ( ¬ ( def B x ) ) } + + +record Filter ( L : OD ) : Set (suc n) where field - _⊇_ : OD → OD → Set n - G : OD - G∋1 : G ∋ max - Gmax : { p : OD } → P ∋ p → p ⊇ max - Gless : { p q : OD } → G ∋ p → P ∋ q → p ⊇ q → G ∋ q - Gcompat : { p q : OD } → G ∋ p → G ∋ q → ¬ ( - ( r : OD ) → (( p ⊇ r ) ∧ ( p ⊇ r ))) + filter : OD + proper : ¬ ( filter ∋ od∅ ) + inL : filter ⊆ L + filter1 : { p q : OD } → q ⊆ L → filter ∋ p → p ⊆ q → filter ∋ q + filter2 : { p q : OD } → filter ∋ p → filter ∋ q → filter ∋ (p ∩ q) -dense : Set (suc n) -dense = { D P p : OD } → ({x : OD } → P ∋ p → ¬ ( ( q : OD ) → D ∋ q → od→ord p o< od→ord q )) +open Filter + +L⊆L : (L : OD) → L ⊆ L +L⊆L L = record { incl = λ {x} lt → lt } + +L-filter : {L : OD} → (P : Filter L ) → {p : OD} → filter P ∋ p → filter P ∋ L +L-filter {L} P {p} lt = filter1 P {p} {L} (L⊆L L) lt {!!} -record NatFilter ( P : Nat → Set n) : Set (suc n) where +prime-filter : {L : OD} → Filter L → ∀ {p q : OD } → Set n +prime-filter {L} P {p} {q} = filter P ∋ ( p ∪ q) → ( filter P ∋ p ) ∨ ( filter P ∋ q ) + +ultra-filter : {L : OD} → Filter L → ∀ {p : OD } → Set n +ultra-filter {L} P {p} = L ∋ p → ( filter P ∋ p ) ∨ ( filter P ∋ ( L ＼ p) ) + + +filter-lemma1 : {L : OD} → (P : Filter L) → ∀ {p q : OD } → ( ∀ (p : OD ) → ultra-filter {L} P {p} ) → prime-filter {L} P {p} {q} +filter-lemma1 {L} P {p} {q} u lt = {!!} + +filter-lemma2 : {L : OD} → (P : Filter L) → ( ∀ {p q : OD } → prime-filter {L} P {p} {q}) → ∀ (p : OD ) → ultra-filter {L} P {p} +filter-lemma2 {L} P prime p with prime {!!} +... | t = {!!} + +generated-filter : {L : OD} → Filter L → (p : OD ) → Filter ( record { def = λ x → def L x ∨ (x ≡ od→ord p) } ) +generated-filter {L} P p = record { + proper = {!!} ; + filter = {!!} ; inL = {!!} ; + filter1 = {!!} ; filter2 = {!!} + } + +record Dense (P : OD ) : Set (suc n) where field - GN : Nat → Set n - GN∋1 : GN 0 - GNmax : { p : Nat } → P p → 0 ≤ p - GNless : { p q : Nat } → GN p → P q → q ≤ p → GN q - Gr : ( p q : Nat ) → GN p → GN q → Nat - GNcompat : { p q : Nat } → (gp : GN p) → (gq : GN q ) → ( Gr p q gp gq ≤ p ) ∨ ( Gr p q gp gq ≤ q ) - -record NatDense {n : Level} ( P : Nat → Set n) : Set (suc n) where - field - Gmid : { p : Nat } → P p → Nat - GDense : { D : Nat → Set n } → {x p : Nat } → (pp : P p ) → D (Gmid {p} pp) → Gmid pp ≤ p - -open OD.OD + dense : OD + incl : dense ⊆ P + dense-f : OD → OD + dense-p : { p : OD} → P ∋ p → p ⊆ (dense-f p) -- H(ω,2) = Power ( Power ω ) = Def ( Def ω)) -Pred : ( Dom : OD ) → OD -Pred dom = record { - def = λ x → def dom x → {!!} - } +infinite = ZF.infinite OD→ZF -Hω2 : OD -Hω2 = record { def = λ x → {dom : Ordinal } → x ≡ od→ord ( Pred ( ord→od dom )) } +module in-countable-ordinal {n : Level} where + + import ordinal -Hω2Filter : Filter Hω2 od∅ -Hω2Filter = record { - _⊇_ = _⊇_ - ; G = {!!} - ; G∋1 = {!!} - ; Gmax = {!!} - ; Gless = {!!} - ; Gcompat = {!!} - } where - P = Hω2 - _⊇_ : OD → OD → Set n - _⊇_ = {!!} - G : OD - G = {!!} - G∋1 : G ∋ od∅ - G∋1 = {!!} - Gmax : { p : OD } → P ∋ p → p ⊇ od∅ - Gmax = {!!} - Gless : { p q : OD } → G ∋ p → P ∋ q → p ⊇ q → G ∋ q - Gless = {!!} - Gcompat : { p q : OD } → G ∋ p → G ∋ q → ¬ ( - ( r : OD ) → (( p ⊇ r ) ∧ ( p ⊇ r ))) - Gcompat = {!!} + -- open ordinal.C-Ordinal-with-choice + -- both Power and infinite is too ZF, it is better to use simpler one + Hω2 : Filter (Power (Power infinite)) + Hω2 = {!!}
--- a/ordinal.agda Thu Aug 29 16:18:37 2019 +0900 +++ b/ordinal.agda Sun Jun 07 20:31:30 2020 +0900 @@ -203,7 +203,6 @@ lemma y lt | case1 refl = proj1 ( TransFinite1 lx ox ) lemma y lt | case2 lt1 = proj2 ( TransFinite1 lx ox ) y lt1 - open import Ordinals C-Ordinal : {n : Level} → Ordinals {suc n} @@ -234,75 +233,3 @@ ψ (record { lv = lx ; ord = OSuc lx x₁ }) caseOSuc lx ox prev = lt (ordinal lx (OSuc lx ox)) prev -module C-Ordinal-with-choice {n : Level} where - - import OD - -- open inOrdinal C-Ordinal - open OD (C-Ordinal {n}) - open OD.OD - - -- - -- another form of regularity - -- - ε-induction : {m : Level} { ψ : OD → Set m} - → ( {x : OD } → ({ y : OD } → x ∋ y → ψ y ) → ψ x ) - → (x : OD ) → ψ x - ε-induction {m} {ψ} ind x = subst (λ k → ψ k ) oiso (ε-induction-ord (lv (osuc (od→ord x))) (ord (osuc (od→ord x))) <-osuc) where - ε-induction-ord : (lx : Nat) ( ox : OrdinalD {suc n} lx ) {ly : Nat} {oy : OrdinalD {suc n} ly } - → (ly < lx) ∨ (oy d< ox ) → ψ (ord→od (record { lv = ly ; ord = oy } ) ) - ε-induction-ord lx (OSuc lx ox) {ly} {oy} y<x = - ind {ord→od (record { lv = ly ; ord = oy })} ( λ {y} lt → subst (λ k → ψ k ) oiso (ε-induction-ord lx ox (lemma y lt ))) where - lemma : (z : OD) → ord→od record { lv = ly ; ord = oy } ∋ z → od→ord z o< record { lv = lx ; ord = ox } - lemma z lt with osuc-≡< y<x - lemma z lt | case1 refl = o<-subst (c<→o< lt) refl diso - lemma z lt | case2 lt1 = ordtrans (o<-subst (c<→o< lt) refl diso) lt1 - ε-induction-ord (Suc lx) (Φ (Suc lx)) {ly} {oy} (case1 y<sox ) = - ind {ord→od (record { lv = ly ; ord = oy })} ( λ {y} lt → lemma y lt ) where - -- - -- if lv of z if less than x Ok - -- else lv z = lv x. We can create OSuc of z which is larger than z and less than x in lemma - -- - -- lx Suc lx (1) lz(a) <lx by case1 - -- ly(1) ly(2) (2) lz(b) <lx by case1 - -- lz(a) lz(b) lz(c) lz(c) <lx by case2 ( ly==lz==lx) - -- - lemma0 : { lx ly : Nat } → ly < Suc lx → lx < ly → ⊥ - lemma0 {Suc lx} {Suc ly} (s≤s lt1) (s≤s lt2) = lemma0 lt1 lt2 - lemma1 : {ly : Nat} {oy : OrdinalD {suc n} ly} → lv (od→ord (ord→od (record { lv = ly ; ord = oy }))) ≡ ly - lemma1 {ly} {oy} = let open ≡-Reasoning in begin - lv (od→ord (ord→od (record { lv = ly ; ord = oy }))) - ≡⟨ cong ( λ k → lv k ) diso ⟩ - lv (record { lv = ly ; ord = oy }) - ≡⟨⟩ - ly - ∎ - lemma : (z : OD) → ord→od record { lv = ly ; ord = oy } ∋ z → ψ z - lemma z lt with c<→o< {z} {ord→od (record { lv = ly ; ord = oy })} lt - lemma z lt | case1 lz<ly with <-cmp lx ly - lemma z lt | case1 lz<ly | tri< a ¬b ¬c = ⊥-elim ( lemma0 y<sox a) -- can't happen - lemma z lt | case1 lz<ly | tri≈ ¬a refl ¬c = -- ly(1) - subst (λ k → ψ k ) oiso (ε-induction-ord lx (Φ lx) {_} {ord (od→ord z)} (case1 (subst (λ k → lv (od→ord z) < k ) lemma1 lz<ly ) )) - lemma z lt | case1 lz<ly | tri> ¬a ¬b c = -- lz(a) - subst (λ k → ψ k ) oiso (ε-induction-ord lx (Φ lx) {_} {ord (od→ord z)} (case1 (<-trans lz<ly (subst (λ k → k < lx ) (sym lemma1) c)))) - lemma z lt | case2 lz=ly with <-cmp lx ly - lemma z lt | case2 lz=ly | tri< a ¬b ¬c = ⊥-elim ( lemma0 y<sox a) -- can't happen - lemma z lt | case2 lz=ly | tri> ¬a ¬b c with d<→lv lz=ly -- lz(b) - ... | eq = subst (λ k → ψ k ) oiso - (ε-induction-ord lx (Φ lx) {_} {ord (od→ord z)} (case1 (subst (λ k → k < lx ) (trans (sym lemma1)(sym eq) ) c ))) - lemma z lt | case2 lz=ly | tri≈ ¬a lx=ly ¬c with d<→lv lz=ly -- lz(c) - ... | eq = subst (λ k → ψ k ) oiso ( ε-induction-ord lx (dz oz=lx) {lv (od→ord z)} {ord (od→ord z)} (case2 (dz<dz oz=lx) )) where - oz=lx : lv (od→ord z) ≡ lx - oz=lx = let open ≡-Reasoning in begin - lv (od→ord z) - ≡⟨ eq ⟩ - lv (od→ord (ord→od (ordinal ly oy))) - ≡⟨ cong ( λ k → lv k ) diso ⟩ - lv (ordinal ly oy) - ≡⟨ sym lx=ly ⟩ - lx - ∎ - dz : lv (od→ord z) ≡ lx → OrdinalD lx - dz refl = OSuc lx (ord (od→ord z)) - dz<dz : (z=x : lv (od→ord z) ≡ lx ) → ord (od→ord z) d< dz z=x - dz<dz refl = s<refl -
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/zf-in-agda.html Sun Jun 07 20:31:30 2020 +0900 @@ -0,0 +1,1642 @@ +<html> +<META HTTP-EQUIV="Content-Type" CONTENT="text/html; charset=UTF-8"> +<head> +<STYLE type="text/css"> +.main { width:100%; } +.side { top:0px; width:0%; position:fixed; left:80%; display:none} +</STYLE> +<script type="text/javascript"> +function showElement(layer){ + var myLayer = document.getElementById(layer); + var main = document.getElementById('mmm'); + if(myLayer.style.display=="none"){ + myLayer.style.width="20%"; + main.style.width="80%"; + myLayer.style.display="block"; + myLayer.backgroundPosition="top"; + } else { + myLayer.style.width="0%"; + main.style.width="100%"; + myLayer.style.display="none"; + } +} +</script> +<title>Constructing ZF Set Theory in Agda </title> +</head> +<body> +<div class="main" id="mmm"> +<h1>Constructing ZF Set Theory in Agda </h1> +<a href="#" right="0px" onclick="javascript:showElement('menu')"> +<span>Menu</span> +</a> +<a href="#" left="0px" onclick="javascript:showElement('menu')"> +<span>Menu</span> +</a> + +<p> + +<author> Shinji KONO</author> + +<hr/> +<h2><a name="content000">ZF in Agda</a></h2> + +<pre> + zf.agda axiom of ZF + zfc.agda axiom of choice + Ordinals.agda axiom of Ordinals + ordinal.agda countable model of Ordinals + OD.agda model of ZF based on Ordinal Definable Set with assumptions + ODC.agda Law of exclude middle from axiom of choice assumptions + LEMC.agda model of choice with assumption of the Law of exclude middle + OPair.agda ordered pair on OD + BAlgbra.agda Boolean algebra on OD (not yet done) + filter.agda Filter on OD (not yet done) + cardinal.agda Caedinal number on OD (not yet done) + logic.agda some basics on logic + nat.agda some basics on Nat + +</pre> + +<hr/> +<h2><a name="content001">Programming Mathematics</a></h2> + +<p> +Programming is processing data structure with λ terms. +<p> +We are going to handle Mathematics in intuitionistic logic with λ terms. +<p> +Mathematics is a functional programming which values are proofs. +<p> +Programming ZF Set Theory in Agda +<p> + +<hr/> +<h2><a name="content002">Target</a></h2> + +<pre> + Describe ZF axioms in Agda + Construction a Model of ZF Set Theory in Agda + Show necessary assumptions for the model + Show validities of ZF axioms on the model + +</pre> +This shows consistency of Set Theory (with some assumptions), +without circulating ZF Theory assumption. +<p> +<a href="https://github.com/shinji-kono/zf-in-agda"> +ZF in Agda https://github.com/shinji-kono/zf-in-agda +</a> +<p> + +<hr/> +<h2><a name="content003">Why Set Theory</a></h2> +If we can formulate Set theory, it suppose to work on any mathematical theory. +<p> +Set Theory is a difficult point for beginners especially axiom of choice. +<p> +It has some amount of difficulty and self circulating discussion. +<p> +I'm planning to do it in my old age, but I'm enough age now. +<p> +This is done during from May to September. +<p> + +<hr/> +<h2><a name="content004">Agda and Intuitionistic Logic </a></h2> +Curry Howard Isomorphism +<p> + +<pre> + Proposition : Proof ⇔ Type : Value + +</pre> +which means +<p> + constructing a typed lambda calculus which corresponds a logic +<p> +Typed lambda calculus which allows complex type as a value of a variable (System FC) +<p> + First class Type / Dependent Type +<p> +Agda is a such a programming language which has similar syntax of Haskell +<p> +Coq is specialized in proof assistance such as command and tactics . +<p> + +<hr/> +<h2><a name="content005">Introduction of Agda </a></h2> +A length of a list of type A. +<p> + +<pre> + length : {A : Set } → List A → Nat + length [] = zero + length (_ ∷ t) = suc ( length t ) + +</pre> +Simple functional programming language. Type declaration is mandatory. +A colon means type, an equal means value. Indentation based. +<p> +Set is a base type (which may have a level ). +<p> +{} means implicit variable which can be omitted if Agda infers its value. +<p> + +<hr/> +<h2><a name="content006">data ( Sum type )</a></h2> +A data type which as exclusive multiple constructors. A similar one as +union in C or case class in Scala. +<p> +It has a similar syntax as Haskell but it has a slight difference. +<p> + +<pre> + data List (A : Set ) : Set where + [] : List A + _∷_ : A → List A → List A + +</pre> +_∷_ means infix operator. If use explicit _, it can be used in a normal function +syntax. +<p> +Natural number can be defined as a usual way. +<p> + +<pre> + data Nat : Set where + zero : Nat + suc : Nat → Nat + +</pre> + +<hr/> +<h2><a name="content007"> A → B means "A implies B"</a></h2> + +<p> +In Agda, a type can be a value of a variable, which is usually called dependent type. +Type has a name Set in Agda. +<p> + +<pre> + ex3 : {A B : Set} → Set + ex3 {A}{B} = A → B + +</pre> +ex3 is a type : A → B, which is a value of Set. It also means a formula : A implies B. +<p> + +<pre> + A type is a formula, the value is the proof + +</pre> +A value of A → B can be interpreted as an inference from the formula A to the formula B, which +can be a function from a proof of A to a proof of B. +<p> + +<hr/> +<h2><a name="content008">introduction と elimination</a></h2> +For a logical operator, there are two types of inference, an introduction and an elimination. +<p> + +<pre> + intro creating symbol / constructor / introduction + elim using symbolic / accessors / elimination + +</pre> +In Natural deduction, this can be written in proof schema. +<p> + +<pre> + A + : + B A A → B + ------------- →intro ------------------ →elim + A → B B + +</pre> +In Agda, this is a pair of type and value as follows. Introduction of → uses λ. +<p> + +<pre> + →intro : {A B : Set } → A → B → ( A → B ) + →intro _ b = λ x → b + →elim : {A B : Set } → A → ( A → B ) → B + →elim a f = f a + +</pre> +Important +<p> + +<pre> + {A B : Set } → A → B → ( A → B ) + +</pre> +is +<p> + +<pre> + {A B : Set } → ( A → ( B → ( A → B ) )) + +</pre> +This makes currying of function easy. +<p> + +<hr/> +<h2><a name="content009"> To prove A → B </a></h2> +Make a left type as an argument. (intros in Coq) +<p> + +<pre> + ex5 : {A B C : Set } → A → B → C → ? + ex5 a b c = ? + +</pre> +? is called a hole, which is unspecified part. Agda tell us which kind type is required for the Hole. +<p> +We are going to fill the holes, and if we have no warnings nor errors such as type conflict (Red), +insufficient proof or instance (Yellow), Non-termination, the proof is completed. +<p> + +<hr/> +<h2><a name="content010"> A ∧ B</a></h2> +Well known conjunction's introduction and elimination is as follow. +<p> + +<pre> + A B A ∧ B A ∧ B + ------------- ----------- proj1 ---------- proj2 + A ∧ B A B + +</pre> +We can introduce a corresponding structure in our functional programming language. +<p> + +<hr/> +<h2><a name="content011"> record</a></h2> + +<pre> + record _∧_ A B : Set + field + proj1 : A + proj2 : B + +</pre> +_∧_ means infix operator. _∧_ A B can be written as A ∧ B (Haskell uses (∧) ) +<p> +This a type which constructed from type A and type B. You may think this as an object +or struct. +<p> + +<pre> + record { proj1 = x ; proj2 = y } + +</pre> +is a constructor of _∧_. +<p> + +<pre> + ex3 : {A B : Set} → A → B → ( A ∧ B ) + ex3 a b = record { proj1 = a ; proj2 = b } + ex1 : {A B : Set} → ( A ∧ B ) → A + ex1 a∧b = proj1 a∧b + +</pre> +a∧b is a variable name. If we have no spaces in a string, it is a word even if we have symbols +except parenthesis or colons. A symbol requires space separation such as a type defining colon. +<p> +Defining record can be recursively, but we don't use the recursion here. +<p> + +<hr/> +<h2><a name="content012"> Mathematical structure</a></h2> +We have types of elements and the relationship in a mathematical structure. +<p> + +<pre> + logical relation has no ordering + there is a natural ordering in arguments and a value in a function + +</pre> +So we have typical definition style of mathematical structure with records. +<p> + +<pre> + record IsOrdinals {n : Level} (ord : Set n) + (_o<_ : ord → ord → Set n) : Set (suc (suc n)) where + field + Otrans : {x y z : ord } → x o< y → y o< z → x o< z + record Ordinals {n : Level} : Set (suc (suc n)) where + field + ord : Set n + _o<_ : ord → ord → Set n + isOrdinal : IsOrdinals ord _o<_ + +</pre> +In IsOrdinals, axioms are written in flat way. In Ordinal, we may have +inputs and outputs are put in the field including IsOrdinal. +<p> +Fields of Ordinal is existential objects in the mathematical structure. +<p> + +<hr/> +<h2><a name="content013"> A Model and a theory</a></h2> +Agda record is a type, so we can write it in the argument, but is it really exists? +<p> +If we have a value of the record, it simply exists, that is, we need to create all the existence +in the record satisfies all the axioms (= field of IsOrdinal) should be valid. +<p> + +<pre> + type of record = theory + value of record = model + +</pre> +We call the value of the record as a model. If mathematical structure has a +model, it exists. Pretty Obvious. +<p> + +<hr/> +<h2><a name="content014"> postulate と module</a></h2> +Agda proofs are separated by modules, which are large records. +<p> +postulates are assumptions. We can assume a type without proofs. +<p> + +<pre> + postulate + sup-o : ( Ordinal → Ordinal ) → Ordinal + sup-o< : { ψ : Ordinal → Ordinal } → ∀ {x : Ordinal } → ψ x o< sup-o ψ + +</pre> +sup-o is an example of upper bound of a function and sup-o< assumes it actually satisfies all the value is less than upper bound. +<p> +Writing some type in a module argument is the same as postulating a type, but +postulate can be written the middle of a proof. +<p> +postulate can be constructive. +<p> +postulate can be inconsistent, which result everything has a proof. +<p> + +<hr/> +<h2><a name="content015"> A ∨ B</a></h2> + +<pre> + data _∨_ (A B : Set) : Set where + case1 : A → A ∨ B + case2 : B → A ∨ B + +</pre> +As Haskell, case1/case2 are patterns. +<p> + +<pre> + ex3 : {A B : Set} → ( A ∨ A ) → A + ex3 = ? + +</pre> +In a case statement, Agda command C-C C-C generates possible cases in the head. +<p> + +<pre> + ex3 : {A B : Set} → ( A ∨ A ) → A + ex3 (case1 x) = ? + ex3 (case2 x) = ? + +</pre> +Proof schema of ∨ is omit due to the complexity. +<p> + +<hr/> +<h2><a name="content016"> Negation</a></h2> + +<pre> + ⊥ + ------------- ⊥-elim + A + +</pre> +Anything can be derived from bottom, in this case a Set A. There is no introduction rule +in ⊥, which can be implemented as data which has no constructor. +<p> + +<pre> + data ⊥ : Set where + +</pre> +⊥-elim can be proved like this. +<p> + +<pre> + ⊥-elim : {A : Set } -> ⊥ -> A + ⊥-elim () + +</pre> +() means no match argument nor value. +<p> +A negation can be defined using ⊥ like this. +<p> + +<pre> + ¬_ : Set → Set + ¬ A = A → ⊥ + +</pre> + +<hr/> +<h2><a name="content017">Equality </a></h2> + +<p> +All the value in Agda are terms. If we have the same normalized form, two terms are equal. +If we have variables in the terms, we will perform an unification. unifiable terms are equal. +We don't go further on the unification. +<p> + +<pre> + { x : A } x ≡ y f x y + --------------- ≡-intro --------------------- ≡-elim + x ≡ x f x x + +</pre> +equality _≡_ can be defined as a data. +<p> + +<pre> + data _≡_ {A : Set } : A → A → Set where + refl : {x : A} → x ≡ x + +</pre> +The elimination of equality is a substitution in a term. +<p> + +<pre> + subst : {A : Set } → { x y : A } → ( f : A → Set ) → x ≡ y → f x → f y + subst {A} {x} {y} f refl fx = fx + ex5 : {A : Set} {x y z : A } → x ≡ y → y ≡ z → x ≡ z + ex5 {A} {x} {y} {z} x≡y y≡z = subst ( λ k → x ≡ k ) y≡z x≡y + +</pre> + +<hr/> +<h2><a name="content018">Equivalence relation</a></h2> + +<p> + +<pre> + refl' : {A : Set} {x : A } → x ≡ x + refl' = ? + sym : {A : Set} {x y : A } → x ≡ y → y ≡ x + sym = ? + trans : {A : Set} {x y z : A } → x ≡ y → y ≡ z → x ≡ z + trans = ? + cong : {A B : Set} {x y : A } { f : A → B } → x ≡ y → f x ≡ f y + cong = ? + +</pre> + +<hr/> +<h2><a name="content019">Ordering</a></h2> + +<p> +Relation is a predicate on two value which has a same type. +<p> + +<pre> + A → A → Set + +</pre> +Defining order is the definition of this type with predicate or a data. +<p> + +<pre> + data _≤_ : Rel ℕ 0ℓ where + z≤n : ∀ {n} → zero ≤ n + s≤s : ∀ {m n} (m≤n : m ≤ n) → suc m ≤ suc n + +</pre> + +<hr/> +<h2><a name="content020">Quantifier</a></h2> + +<p> +Handling quantifier in an intuitionistic logic requires special cares. +<p> +In the input of a function, there are no restriction on it, that is, it has +a universal quantifier. (If we explicitly write ∀, Agda gives us a type inference on it) +<p> +There is no ∃ in agda, the one way is using negation like this. +<p> + ∃ (x : A ) → p x = ¬ ( ( x : A ) → ¬ ( p x ) ) +<p> +On the another way, f : A can be used like this. +<p> + +<pre> + p f + +</pre> +If we use a function which can be defined globally which has stronger meaning the +usage of ∃ x in a logical expression. +<p> + +<hr/> +<h2><a name="content021">Can we do math in this way?</a></h2> +Yes, we can. Actually we have Principia Mathematica by Russell and Whitehead (with out computer support). +<p> +In some sense, this story is a reprinting of the work, (but Principia Mathematica has a different formulation than ZF). +<p> + +<pre> + define mathematical structure as a record + program inferences as if we have proofs in variables + +</pre> + +<hr/> +<h2><a name="content022">Things which Agda cannot prove</a></h2> + +<p> +The infamous Internal Parametricity is a limitation of Agda, it cannot prove so called Free Theorem, which +leads uniqueness of a functor in Category Theory. +<p> +Functional extensionality cannot be proved. +<pre> + (∀ x → f x ≡ g x) → f ≡ g + +</pre> +Agda has no law of exclude middle. +<p> + +<pre> + a ∨ ( ¬ a ) + +</pre> +For example, (A → B) → ¬ B → ¬ A can be proved but, ( ¬ B → ¬ A ) → A → B cannot. +<p> +It also other problems such as termination, type inference or unification which we may overcome with +efforts or devices or may not. +<p> +If we cannot prove something, we can safely postulate it unless it leads a contradiction. +<pre> + + +</pre> + +<hr/> +<h2><a name="content023">Classical story of ZF Set Theory</a></h2> + +<p> +Assuming ZF, constructing a model of ZF is a flow of classical Set Theory, which leads +a relative consistency proof of the Set Theory. +Ordinal number is used in the flow. +<p> +In Agda, first we defines Ordinal numbers (Ordinals), then introduce Ordinal Definable Set (OD). +We need some non constructive assumptions in the construction. A model of Set theory is +constructed based on these assumptions. +<p> +<img src="fig/set-theory.svg"> + +<p> + +<hr/> +<h2><a name="content024">Ordinals</a></h2> +Ordinals are our intuition of infinite things, which has ∅ and orders on the things. +It also has a successor osuc. +<p> + +<pre> + record Ordinals {n : Level} : Set (suc (suc n)) where + field + ord : Set n + o∅ : ord + osuc : ord → ord + _o<_ : ord → ord → Set n + isOrdinal : IsOrdinals ord o∅ osuc _o<_ + +</pre> +It is different from natural numbers in way. The order of Ordinals is not defined in terms +of successor. It is given from outside, which make it possible to have higher order infinity. +<p> + +<hr/> +<h2><a name="content025">Axiom of Ordinals</a></h2> +Properties of infinite things. We request a transfinite induction, which states that if +some properties are satisfied below all possible ordinals, the properties are true on all +ordinals. +<p> +Successor osuc has no ordinal between osuc and the base ordinal. There are some ordinals +which is not a successor of any ordinals. It is called limit ordinal. +<p> +Any two ordinal can be compared, that is less, equal or more, that is total order. +<p> + +<pre> + record IsOrdinals {n : Level} (ord : Set n) (o∅ : ord ) + (osuc : ord → ord ) + (_o<_ : ord → ord → Set n) : Set (suc (suc n)) where + field + Otrans : {x y z : ord } → x o< y → y o< z → x o< z + OTri : Trichotomous {n} _≡_ _o<_ + ¬x<0 : { x : ord } → ¬ ( x o< o∅ ) + <-osuc : { x : ord } → x o< osuc x + osuc-≡< : { a x : ord } → x o< osuc a → (x ≡ a ) ∨ (x o< a) + TransFinite : { ψ : ord → Set (suc n) } + → ( (x : ord) → ( (y : ord ) → y o< x → ψ y ) → ψ x ) + → ∀ (x : ord) → ψ x + +</pre> + +<hr/> +<h2><a name="content026">Concrete Ordinals</a></h2> + +<p> +We can define a list like structure with level, which is a kind of two dimensional infinite array. +<p> + +<pre> + data OrdinalD {n : Level} : (lv : Nat) → Set n where + Φ : (lv : Nat) → OrdinalD lv + OSuc : (lv : Nat) → OrdinalD {n} lv → OrdinalD lv + +</pre> +The order of the OrdinalD can be defined in this way. +<p> + +<pre> + data _d<_ {n : Level} : {lx ly : Nat} → OrdinalD {n} lx → OrdinalD {n} ly → Set n where + Φ< : {lx : Nat} → {x : OrdinalD {n} lx} → Φ lx d< OSuc lx x + s< : {lx : Nat} → {x y : OrdinalD {n} lx} → x d< y → OSuc lx x d< OSuc lx y + +</pre> +This is a simple data structure, it has no abstract assumptions, and it is countable many data +structure. +<p> + +<pre> + Φ 0 + OSuc 2 ( Osuc 2 ( Osuc 2 (Φ 2))) + Osuc 0 (Φ 0) d< Φ 1 + +</pre> + +<hr/> +<h2><a name="content027">Model of Ordinals</a></h2> + +<p> +It is easy to show OrdinalD and its order satisfies the axioms of Ordinals. +<p> +So our Ordinals has a mode. This means axiom of Ordinals are consistent. +<p> + +<hr/> +<h2><a name="content028">Debugging axioms using Model</a></h2> +Whether axiom is correct or not can be checked by a validity on a mode. +<p> +If not, we may fix the axioms or the model, such as the definitions of the order. +<p> +We can also ask whether the inputs exist. +<p> + +<hr/> +<h2><a name="content029">Countable Ordinals can contains uncountable set?</a></h2> +Yes, the ordinals contains any level of infinite Set in the axioms. +<p> +If we handle real-number in the model, only countable number of real-number is used. +<p> + +<pre> + from the outside view point, it is countable + from the internal view point, it is uncountable + +</pre> +The definition of countable/uncountable is the same, but the properties are different +depending on the context. +<p> +We don't show the definition of cardinal number here. +<p> + +<hr/> +<h2><a name="content030">What is Set</a></h2> +The word Set in Agda is not a Set of ZF Set, but it is a type (why it is named Set?). +<p> +From naive point view, a set i a list, but in Agda, elements have all the same type. +A set in ZF may contain other Sets in ZF, which not easy to implement it as a list. +<p> +Finite set may be written in finite series of ∨, but ... +<p> + +<hr/> +<h2><a name="content031">We don't ask the contents of Set. It can be anything.</a></h2> +From empty set φ, we can think a set contains a φ, and a pair of φ and the set, and so on, +and all of them, and again we repeat this. +<p> + +<pre> + φ {φ} {φ,{φ}}, {φ,{φ},...} + +</pre> +It is called V. +<p> +This operation can be performed within a ZF Set theory. Classical Set Theory assumes +ZF, so this kind of thing is allowed. +<p> +But in our case, we have no ZF theory, so we are going to use Ordinals. +<p> + +<hr/> +<h2><a name="content032">Ordinal Definable Set</a></h2> +We can define a sbuset of Ordinals using predicates. What is a subset? +<p> + +<pre> + a predicate has an Ordinal argument + +</pre> +is an Ordinal Definable Set (OD). In Agda, OD is defined as follows. +<p> + +<pre> + record OD : Set (suc n ) where + field + def : (x : Ordinal ) → Set n + +</pre> +Ordinals itself is not a set in a ZF Set theory but a class. In OD, +<p> + +<pre> + record { def = λ x → true } + +</pre> +means Ordinals itself, so ODs are larger than a notion of ZF Set Theory, +but we don't care about it. +<p> + +<hr/> +<h2><a name="content033">∋ in OD</a></h2> +OD is a predicate on Ordinals and it does not contains OD directly. If we have a mapping +<p> + +<pre> + od→ord : OD → Ordinal + +</pre> +we may check an OD is an element of the OD using def. +<p> +A ∋ x can be define as follows. +<p> + +<pre> + _∋_ : ( A x : OD ) → Set n + _∋_ A x = def A ( od→ord x ) + +</pre> +In ψ : Ordinal → Set, if A is a record { def = λ x → ψ x } , then +<p> + +<pre> + A x = def A ( od→ord x ) = ψ (od→ord x) + +</pre> + +<hr/> +<h2><a name="content034">1 to 1 mapping between an OD and an Ordinal</a></h2> + +<p> + +<pre> + od→ord : OD → Ordinal + ord→od : Ordinal → OD + oiso : {x : OD } → ord→od ( od→ord x ) ≡ x + diso : {x : Ordinal } → od→ord ( ord→od x ) ≡ x + +</pre> +They say the existing of the mappings can be proved in Classical Set Theory, but we +simply assumes these non constructively. +<p> +We use postulate, it may contains additional restrictions which are not clear now. It look like the mapping should be a subset of Ordinals, but we don't explicitly +state it. +<p> +<img src="fig/ord-od-mapping.svg"> + +<p> + +<hr/> +<h2><a name="content035">Order preserving in the mapping of OD and Ordinal</a></h2> +Ordinals have the order and OD has a natural order based on inclusion ( def / ∋ ). +<p> + +<pre> + def y ( od→ord x ) + +</pre> +An elements of OD should be defined before the OD, that is, an ordinal corresponding an elements +have to be smaller than the corresponding ordinal of the containing OD. +<p> + +<pre> + c<→o< : {x y : OD } → def y ( od→ord x ) → od→ord x o< od→ord y + +</pre> +This is also said to be provable in classical Set Theory, but we simply assumes it. +<p> +OD has an order based on the corresponding ordinal, but it may not have corresponding def / ∋relation. This means the reverse order preservation, +<p> + +<pre> + o<→c< : {n : Level} {x y : Ordinal } → x o< y → def (ord→od y) x + +</pre> +is not valid. If we assumes it, ∀ x ∋ ∅ becomes true, which manes all OD becomes Ordinals in +the model. +<p> +<img src="fig/ODandOrdinals.svg"> + +<p> + +<hr/> +<h2><a name="content036">ISO</a></h2> +It also requires isomorphisms, +<p> + +<pre> + oiso : {x : OD } → ord→od ( od→ord x ) ≡ x + diso : {x : Ordinal } → od→ord ( ord→od x ) ≡ x + +</pre> + +<hr/> +<h2><a name="content037">Various Sets</a></h2> + +<p> +In classical Set Theory, there is a hierarchy call L, which can be defined by a predicate. +<p> + +<pre> + Ordinal / things satisfies axiom of Ordinal / extension of natural number + V / hierarchical construction of Set from φ + L / hierarchical predicate definable construction of Set from φ + OD / equational formula on Ordinals + Agda Set / Type / it also has a level + +</pre> + +<hr/> +<h2><a name="content038">Fixes on ZF to intuitionistic logic</a></h2> + +<p> +We use ODs as Sets in ZF, and defines record ZF, that is, we have to define +ZF axioms in Agda. +<p> +It may not valid in our model. We have to debug it. +<p> +Fixes are depends on axioms. +<p> +<img src="fig/axiom-type.svg"> + +<p> +<a href="fig/zf-record.html"> +ZFのrecord </a> +<p> + +<hr/> +<h2><a name="content039">Pure logical axioms</a></h2> + +<pre> + empty, pair, select, ε-induction??infinity + +</pre> +These are logical relations among OD. +<p> + +<pre> + empty : ∀( x : ZFSet ) → ¬ ( ∅ ∋ x ) + pair→ : ( x y t : ZFSet ) → (x , y) ∋ t → ( t ≈ x ) ∨ ( t ≈ y ) + pair← : ( x y t : ZFSet ) → ( t ≈ x ) ∨ ( t ≈ y ) → (x , y) ∋ t + selection : { ψ : ZFSet → Set m } → ∀ { X y : ZFSet } → ( ( y ∈ X ) ∧ ψ y ) ⇔ (y ∈ Select X ψ ) + infinity∅ : ∅ ∈ infinite + infinity : ∀( x : ZFSet ) → x ∈ infinite → ( x ∪ ( x , x ) ) ∈ infinite + ε-induction : { ψ : OD → Set (suc n)} + → ( {x : OD } → ({ y : OD } → x ∋ y → ψ y ) → ψ x ) + → (x : OD ) → ψ x + +</pre> +finitely can be define by Agda data. +<p> + +<pre> + data infinite-d : ( x : Ordinal ) → Set n where + iφ : infinite-d o∅ + isuc : {x : Ordinal } → infinite-d x → + infinite-d (od→ord ( Union (ord→od x , (ord→od x , ord→od x ) ) )) + +</pre> +Union (x , ( x , x )) should be an direct successor of x, but we cannot prove it in our model. +<p> + +<hr/> +<h2><a name="content040">Axiom of Pair</a></h2> +In the Tanaka's book, axiom of pair is as follows. +<p> + +<pre> + ∀ x ∀ y ∃ z ∀ t ( z ∋ t ↔ t ≈ x ∨ t ≈ y) + +</pre> +We have fix ∃ z, a function (x , y) is defined, which is _,_ . +<p> + +<pre> + _,_ : ( A B : ZFSet ) → ZFSet + +</pre> +using this, we can define two directions in separates axioms, like this. +<p> + +<pre> + pair→ : ( x y t : ZFSet ) → (x , y) ∋ t → ( t ≈ x ) ∨ ( t ≈ y ) + pair← : ( x y t : ZFSet ) → ( t ≈ x ) ∨ ( t ≈ y ) → (x , y) ∋ t + +</pre> +This is already written in Agda, so we use these as axioms. All inputs have ∀. +<p> + +<hr/> +<h2><a name="content041">pair in OD</a></h2> +OD is an equation on Ordinals, we can simply write axiom of pair in the OD. +<p> + +<pre> + _,_ : OD → OD → OD + x , y = record { def = λ t → (t ≡ od→ord x ) ∨ ( t ≡ od→ord y ) } + +</pre> +≡ is an equality of λ terms, but please not that this is equality on Ordinals. +<p> + +<hr/> +<h2><a name="content042">Validity of Axiom of Pair</a></h2> +Assuming ZFSet is OD, we are going to prove pair→ . +<p> + +<pre> + pair→ : ( x y t : OD ) → (x , y) ∋ t → ( t == x ) ∨ ( t == y ) + pair→ x y t p = ? + +</pre> +In this program, type of p is ( x , y ) ∋ t , that is def ( x , y ) that is, (t ≡ od→ord x ) ∨ ( t ≡ od→ord y ) . +<p> +Since _∨_ is a data, it can be developed as (C-c C-c : agda2-make-case ). +<p> + +<pre> + pair→ x y t (case1 t≡x ) = ? + pair→ x y t (case2 t≡y ) = ? + +</pre> +The type of the ? is ( t == x ) ∨ ( t == y ), again it is data _∨_ . +<p> + +<pre> + pair→ x y t (case1 t≡x ) = case1 ? + pair→ x y t (case2 t≡y ) = case2 ? + +</pre> +The ? in case1 is t == x, so we have to create this from t≡x, which is a name of a variable +which type is +<p> + +<pre> + t≡x : od→ord t ≡ od→ord x + +</pre> +which is shown by an Agda command (C-C C-E : agda2-show-context ). +<p> +But we haven't defined == yet. +<p> + +<hr/> +<h2><a name="content043">Equality of OD and Axiom of Extensionality </a></h2> +OD is defined by a predicates, if we compares normal form of the predicates, even if +it contains the same elements, it may be different, which is no good as an equality of +Sets. +<p> +Axiom of Extensionality requires sets having the same elements are handled in the same way +each other. +<p> + +<pre> + ∀ z ( z ∈ x ⇔ z ∈ y ) ⇒ ∀ w ( x ∈ w ⇔ y ∈ w ) + +</pre> +We can write this axiom in Agda as follows. +<p> + +<pre> + extensionality : { A B w : ZFSet } → ( (z : ZFSet) → ( A ∋ z ) ⇔ (B ∋ z) ) → ( A ∈ w ⇔ B ∈ w ) + +</pre> +So we use ( A ∋ z ) ⇔ (B ∋ z) as an equality (_==_) of our model. We have to show +A ∈ w ⇔ B ∈ w from A == B. +<p> +x == y can be defined in this way. +<p> + +<pre> + record _==_ ( a b : OD ) : Set n where + field + eq→ : ∀ { x : Ordinal } → def a x → def b x + eq← : ∀ { x : Ordinal } → def b x → def a x + +</pre> +Actually, (z : OD) → (A ∋ z) ⇔ (B ∋ z) implies A == B. +<p> + +<pre> + extensionality0 : {A B : OD } → ((z : OD) → (A ∋ z) ⇔ (B ∋ z)) → A == B + eq→ (extensionality0 {A} {B} eq ) {x} d = ? + eq← (extensionality0 {A} {B} eq ) {x} d = ? + +</pre> +? are def B x and def A x and these are generated from eq : (z : OD) → (A ∋ z) ⇔ (B ∋ z) . +<p> +Actual proof is rather complicated. +<p> + +<pre> + eq→ (extensionality0 {A} {B} eq ) {x} d = def-iso {A} {B} (sym diso) (proj1 (eq (ord→od x))) d + eq← (extensionality0 {A} {B} eq ) {x} d = def-iso {B} {A} (sym diso) (proj2 (eq (ord→od x))) d + +</pre> +where +<p> + +<pre> + def-iso : {A B : OD } {x y : Ordinal } → x ≡ y → (def A y → def B y) → def A x → def B x + def-iso refl t = t + +</pre> + +<hr/> +<h2><a name="content044">Validity of Axiom of Extensionality</a></h2> + +<p> +If we can derive (w ∋ A) ⇔ (w ∋ B) from A == B, the axiom becomes valid, but it seems impossible, so we assumes +<p> + +<pre> + ==→o≡ : { x y : OD } → (x == y) → x ≡ y + +</pre> +Using this, we have +<p> + +<pre> + extensionality : {A B w : OD } → ((z : OD ) → (A ∋ z) ⇔ (B ∋ z)) → (w ∋ A) ⇔ (w ∋ B) + proj1 (extensionality {A} {B} {w} eq ) d = subst (λ k → w ∋ k) ( ==→o≡ (extensionality0 {A} {B} eq) ) d + proj2 (extensionality {A} {B} {w} eq ) d = subst (λ k → w ∋ k) (sym ( ==→o≡ (extensionality0 {A} {B} eq) )) d + +</pre> +This assumption means we may have an equivalence set on any predicates. +<p> + +<hr/> +<h2><a name="content045">Non constructive assumptions so far</a></h2> +We have correspondence between OD and Ordinals and one directional order preserving. +<p> +We also have equality assumption. +<p> + +<pre> + od→ord : OD → Ordinal + ord→od : Ordinal → OD + oiso : {x : OD } → ord→od ( od→ord x ) ≡ x + diso : {x : Ordinal } → od→ord ( ord→od x ) ≡ x + c<→o< : {x y : OD } → def y ( od→ord x ) → od→ord x o< od→ord y + ==→o≡ : { x y : OD } → (x == y) → x ≡ y + +</pre> + +<hr/> +<h2><a name="content046">Axiom which have negation form</a></h2> + +<p> + +<pre> + Union, Selection + +</pre> +These axioms contains ∃ x as a logical relation, which can be described in ¬ ( ∀ x ( ¬ p )). +<p> +Axiom of replacement uses upper bound of function on Ordinals, which makes it non-constructive. +<p> +Power Set axiom requires double negation, +<p> + +<pre> + power→ : ∀( A t : ZFSet ) → Power A ∋ t → ∀ {x} → t ∋ x → ¬ ¬ ( A ∋ x ) + power← : ∀( A t : ZFSet ) → t ⊆_ A → Power A ∋ t + +</pre> +If we have an assumption of law of exclude middle, we can recover the original A ∋ x form. +<p> + +<hr/> +<h2><a name="content047">Union </a></h2> +The original form of the Axiom of Union is +<p> + +<pre> + ∀ x ∃ y ∀ z (z ∈ y ⇔ ∃ u ∈ x ∧ (z ∈ u)) + +</pre> +Union requires the existence of b in a ⊇ ∃ b ∋ x . We will use negation form of ∃. +<p> + +<pre> + union→ : ( X z u : ZFSet ) → ( X ∋ u ) ∧ (u ∋ z ) → Union X ∋ z + union← : ( X z : ZFSet ) → (X∋z : Union X ∋ z ) → ¬ ( (u : ZFSet ) → ¬ ((X ∋ u) ∧ (u ∋ z ))) + +</pre> +The definition of Union in OD is like this. +<p> + +<pre> + Union : OD → OD + Union U = record { def = λ x → ¬ (∀ (u : Ordinal ) → ¬ ((def U u) ∧ (def (ord→od u) x))) } + +</pre> +Proof of validity is straight forward. +<p> + +<pre> + union→ : (X z u : OD) → (X ∋ u) ∧ (u ∋ z) → Union X ∋ z + union→ X z u xx not = ⊥-elim ( not (od→ord u) ( record { proj1 = proj1 xx + ; proj2 = subst ( λ k → def k (od→ord z)) (sym oiso) (proj2 xx) } )) + union← : (X z : OD) (X∋z : Union X ∋ z) → ¬ ( (u : OD ) → ¬ ((X ∋ u) ∧ (u ∋ z ))) + union← X z UX∋z = FExists _ lemma UX∋z where + lemma : {y : Ordinal} → def X y ∧ def (ord→od y) (od→ord z) → ¬ ((u : OD) → ¬ (X ∋ u) ∧ (u ∋ z)) + lemma {y} xx not = not (ord→od y) record { proj1 = subst ( λ k → def X k ) (sym diso) (proj1 xx ) ; proj2 = proj2 xx } + +</pre> +where +<p> + +<pre> + FExists : {m l : Level} → ( ψ : Ordinal → Set m ) + → {p : Set l} ( P : { y : Ordinal } → ψ y → ¬ p ) + → (exists : ¬ (∀ y → ¬ ( ψ y ) )) + → ¬ p + FExists {m} {l} ψ {p} P = contra-position ( λ p y ψy → P {y} ψy p ) + +</pre> +which checks existence using contra-position. +<p> + +<hr/> +<h2><a name="content048">Axiom of replacement</a></h2> +We can replace the elements of a set by a function and it becomes a set. From the book, +<p> + +<pre> + ∀ x ∀ y ∀ z ( ( ψ ( x , y ) ∧ ψ ( x , z ) ) → y = z ) → ∀ X ∃ A ∀ y ( y ∈ A ↔ ∃ x ∈ X ψ ( x , y ) ) + +</pre> +The existential quantifier can be related by a function, +<p> + +<pre> + Replace : OD → (OD → OD ) → OD + +</pre> +The axioms becomes as follows. +<p> + +<pre> + replacement← : {ψ : ZFSet → ZFSet} → ∀ ( X x : ZFSet ) → x ∈ X → ψ x ∈ Replace X ψ + replacement→ : {ψ : ZFSet → ZFSet} → ∀ ( X x : ZFSet ) → ( lt : x ∈ Replace X ψ ) → ¬ ( ∀ (y : ZFSet) → ¬ ( x ≈ ψ y ) ) + +</pre> +In the axiom, the existence of the original elements is necessary. In order to do that we use OD which has +negation form of existential quantifier in the definition. +<p> + +<pre> + in-codomain : (X : OD ) → ( ψ : OD → OD ) → OD + in-codomain X ψ = record { def = λ x → ¬ ( (y : Ordinal ) → ¬ ( def X y ∧ ( x ≡ od→ord (ψ (ord→od y ))))) } + +</pre> +Besides this upper bounds is required. +<p> + +<pre> + Replace : OD → (OD → OD ) → OD + Replace X ψ = record { def = λ x → (x o< sup-o ( λ x → od→ord (ψ (ord→od x )))) ∧ def (in-codomain X ψ) x } + +</pre> +We omit the proof of the validity, but it is rather straight forward. +<p> + +<hr/> +<h2><a name="content049">Validity of Power Set Axiom</a></h2> +The original Power Set Axiom is this. +<p> + +<pre> + ∀ X ∃ A ∀ t ( t ∈ A ↔ t ⊆ X ) ) + +</pre> +The existential quantifier is replaced by a function +<p> + +<pre> + Power : ( A : OD ) → OD + +</pre> +t ⊆ X is a record like this. +<p> + +<pre> + record _⊆_ ( A B : OD ) : Set (suc n) where + field + incl : { x : OD } → A ∋ x → B ∋ x + +</pre> +Axiom becomes likes this. +<p> + +<pre> + power→ : ( A t : OD) → Power A ∋ t → {x : OD} → t ∋ x → ¬ ¬ (A ∋ x) + power← : (A t : OD) → ({x : OD} → (t ∋ x → A ∋ x)) → Power A ∋ t + +</pre> +The validity of the axioms are slight complicated, we have to define set of all subset. We define +subset in a different form. +<p> + +<pre> + ZFSubset : (A x : OD ) → OD + ZFSubset A x = record { def = λ y → def A y ∧ def x y } + +</pre> +We can prove, +<p> + +<pre> + ( {y : OD } → x ∋ y → ZFSubset A x ∋ y ) ⇔ ( x ⊆ A ) + +</pre> +We only have upper bound as an ordinal, but we have an obvious OD based on the order of Ordinals, +which is an Ordinals with our Model. +<p> + +<pre> + Ord : ( a : Ordinal ) → OD + Ord a = record { def = λ y → y o< a } + Def : (A : OD ) → OD + Def A = Ord ( sup-o ( λ x → od→ord ( ZFSubset A (ord→od x )) ) ) + +</pre> +This is slight larger than Power A, so we replace all elements x by A ∩ x (some of them may empty). +<p> + +<pre> + Power : OD → OD + Power A = Replace (Def (Ord (od→ord A))) ( λ x → A ∩ x ) + +</pre> +Creating Power Set of Ordinals is rather easy, then we use replacement axiom on A ∩ x since we have this. +<p> + +<pre> + ∩-≡ : { a b : OD } → ({x : OD } → (a ∋ x → b ∋ x)) → a == ( b ∩ a ) + +</pre> +In case of Ord a intro of Power Set axiom becomes valid. +<p> + +<pre> + ord-power← : (a : Ordinal ) (t : OD) → ({x : OD} → (t ∋ x → (Ord a) ∋ x)) → Def (Ord a) ∋ t + +</pre> +Using this, we can prove, +<p> + +<pre> + power→ : ( A t : OD) → Power A ∋ t → {x : OD} → t ∋ x → ¬ ¬ (A ∋ x) + power← : (A t : OD) → ({x : OD} → (t ∋ x → A ∋ x)) → Power A ∋ t + +</pre> + +<hr/> +<h2><a name="content050">Axiom of regularity, Axiom of choice, ε-induction</a></h2> + +<p> +Axiom of regularity requires non self intersectable elements (which is called minimum), if we +replace it by a function, it becomes a choice function. It makes axiom of choice valid. +<p> +This means we cannot prove axiom regularity form our model, and if we postulate this, axiom of +choice also becomes valid. +<p> + +<pre> + minimal : (x : OD ) → ¬ (x == od∅ )→ OD + x∋minimal : (x : OD ) → ( ne : ¬ (x == od∅ ) ) → def x ( od→ord ( minimal x ne ) ) + minimal-1 : (x : OD ) → ( ne : ¬ (x == od∅ ) ) → (y : OD ) → ¬ ( def (minimal x ne) (od→ord y)) ∧ (def x (od→ord y) ) + +</pre> +We can avoid this using ε-induction (a predicate is valid on all set if the predicate is true on some element of set). +Assuming law of exclude middle, they say axiom of regularity will be proved, but we haven't check it yet. +<p> + +<pre> + ε-induction : { ψ : OD → Set (suc n)} + → ( {x : OD } → ({ y : OD } → x ∋ y → ψ y ) → ψ x ) + → (x : OD ) → ψ x + +</pre> +In our model, we assumes the mapping between Ordinals and OD, this is actually the TransFinite induction in Ordinals. +<p> +The axiom of choice in the book is complicated using any pair in a set, so we use use a form in the Wikipedia. +<p> + +<pre> + ∀ X [ ∅ ∉ X → (∃ f : X → ⋃ X ) → ∀ A ∈ X ( f ( A ) ∈ A ) ] + +</pre> +We can formulate like this. +<p> + +<pre> + choice-func : (X : ZFSet ) → {x : ZFSet } → ¬ ( x ≈ ∅ ) → ( X ∋ x ) → ZFSet + choice : (X : ZFSet ) → {A : ZFSet } → ( X∋A : X ∋ A ) → (not : ¬ ( A ≈ ∅ )) → A ∋ choice-func X not X∋A + +</pre> +It does not requires ∅ ∉ X . +<p> + +<hr/> +<h2><a name="content051">Axiom of choice and Law of Excluded Middle</a></h2> +In our model, since OD has a mapping to Ordinals, it has evident order, which means well ordering theorem is valid, +but it don't have correct form of the axiom yet. They say well ordering axiom is equivalent to the axiom of choice, +but it requires law of the exclude middle. +<p> +Actually, it is well known to prove law of the exclude middle from axiom of choice in intuitionistic logic, and we can +perform the proof in our mode. Using the definition like this, predicates and ODs are related and we can ask the +set is empty or not if we have an axiom of choice, so we have the law of the exclude middle p ∨ ( ¬ p ) . +<p> + +<pre> + ppp : { p : Set n } { a : OD } → record { def = λ x → p } ∋ a → p + ppp {p} {a} d = d + +</pre> +We can prove axiom of choice from law excluded middle since we have TransFinite induction. So Axiom of choice +and Law of Excluded Middle is equivalent in our mode. +<p> + +<hr/> +<h2><a name="content052">Relation-ship among ZF axiom</a></h2> +<img src="fig/axiom-dependency.svg"> + +<p> + +<hr/> +<h2><a name="content053">Non constructive assumption in our model</a></h2> +mapping between OD and Ordinals +<p> + +<pre> + od→ord : OD → Ordinal + ord→od : Ordinal → OD + oiso : {x : OD } → ord→od ( od→ord x ) ≡ x + diso : {x : Ordinal } → od→ord ( ord→od x ) ≡ x + c<→o< : {x y : OD } → def y ( od→ord x ) → od→ord x o< od→ord y + +</pre> +Equivalence on OD +<p> + +<pre> + ==→o≡ : { x y : OD } → (x == y) → x ≡ y + +</pre> +Upper bound +<p> + +<pre> + sup-o : ( Ordinal → Ordinal ) → Ordinal + sup-o< : { ψ : Ordinal → Ordinal } → ∀ {x : Ordinal } → ψ x o< sup-o ψ + +</pre> +Axiom of choice and strong axiom of regularity. +<p> + +<pre> + minimal : (x : OD ) → ¬ (x == od∅ )→ OD + x∋minimal : (x : OD ) → ( ne : ¬ (x == od∅ ) ) → def x ( od→ord ( minimal x ne ) ) + minimal-1 : (x : OD ) → ( ne : ¬ (x == od∅ ) ) → (y : OD ) → ¬ ( def (minimal x ne) (od→ord y)) ∧ (def x (od→ord y) ) + +</pre> + +<hr/> +<h2><a name="content054">So it this correct?</a></h2> + +<p> +Our axiom are syntactically the same in the text book, but negations are slightly different. +<p> +If we assumes excluded middle, these are exactly same. +<p> +Even if we assumes excluded middle, intuitionistic logic itself remains consistent, but we cannot prove it. +<p> +Except the upper bound, axioms are simple logical relation. +<p> +Proof of existence of mapping between OD and Ordinals are not obvious. We don't know we prove it or not. +<p> +Existence of the Upper bounds is a pure assumption, if we have not limit on Ordinals, it may contradicts, +but we don't have explicit upper limit on Ordinals. +<p> +Several inference on our model or our axioms are basically parallel to the set theory text book, so it looks like correct. +<p> + +<hr/> +<h2><a name="content055">How to use Agda Set Theory</a></h2> +Assuming record ZF, classical set theory can be developed. If necessary, axiom of choice can be +postulated or assuming law of excluded middle. +<p> +Instead, simply assumes non constructive assumption, various theory can be developed. We haven't check +these assumptions are proved in record ZF, so we are not sure, these development is a result of ZF Set theory. +<p> +ZF record itself is not necessary, for example, topology theory without ZF can be possible. +<p> + +<hr/> +<h2><a name="content056">Topos and Set Theory</a></h2> +Topos is a mathematical structure in Category Theory, which is a Cartesian closed category which has a +sub-object classifier. +<p> +Topos itself is model of intuitionistic logic. +<p> +Transitive Sets are objects of Cartesian closed category. +It is possible to introduce Power Set Functor on it +<p> +We can use replacement A ∩ x for each element in Transitive Set, +in the similar way of our power set axiom. I +<p> +A model of ZF Set theory can be constructed on top of the Topos which is shown in Oisus. +<p> +Our Agda model is a proof theoretic version of it. +<p> + +<hr/> +<h2><a name="content057">Cardinal number and Continuum hypothesis</a></h2> +Axiom of choice is required to define cardinal number +<p> +definition of cardinal number is not yet done +<p> +definition of filter is not yet done +<p> +we may have a model without axiom of choice or without continuum hypothesis +<p> +Possible representation of continuum hypothesis is this. +<p> + +<pre> + continuum-hyphotheis : (a : Ordinal) → Power (Ord a) ⊆ Ord (osuc a) + +</pre> + +<hr/> +<h2><a name="content058">Filter</a></h2> + +<p> +filter is a dual of ideal on boolean algebra or lattice. Existence on natural number +is depends on axiom of choice. +<p> + +<pre> + record Filter ( L : OD ) : Set (suc n) where + field + filter : OD + proper : ¬ ( filter ∋ od∅ ) + inL : filter ⊆ L + filter1 : { p q : OD } → q ⊆ L → filter ∋ p → p ⊆ q → filter ∋ q + filter2 : { p q : OD } → filter ∋ p → filter ∋ q → filter ∋ (p ∩ q) + +</pre> +We may construct a model of non standard analysis or set theory. +<p> +This may be simpler than classical forcing theory ( not yet done). +<p> + +<hr/> +<h2><a name="content059">Programming Mathematics</a></h2> +Mathematics is a functional programming in Agda where proof is a value of a variable. The mathematical +structure are +<p> + +<pre> + record and data + +</pre> +Proof is check by type consistency not by the computation, but it may include some normalization. +<p> +Type inference and termination is not so clear in multi recursions. +<p> +Defining Agda record is a good way to understand mathematical theory, for examples, +<p> + +<pre> + Category theory ( Yoneda lemma, Floyd Adjunction functor theorem, Applicative functor ) + Automaton ( Subset construction、Language containment) + +</pre> +are proved in Agda. +<p> + +<hr/> +<h2><a name="content060">link</a></h2> +Summer school of foundation of mathematics (in Japanese)<br> <a href="https://www.sci.shizuoka.ac.jp/~math/yorioka/ss2019/">https://www.sci.shizuoka.ac.jp/~math/yorioka/ss2019/</a> +<p> +Foundation of axiomatic set theory (in Japanese)<br> <a href="https://www.sci.shizuoka.ac.jp/~math/yorioka/ss2019/sakai0.pdf">https://www.sci.shizuoka.ac.jp/~math/yorioka/ss2019/sakai0.pdf +</a> +<p> +Agda +<br> <a href="https://agda.readthedocs.io/en/v2.6.0.1/">https://agda.readthedocs.io/en/v2.6.0.1/</a> +<p> +ZF-in-Agda source +<br> <a href="https://github.com/shinji-kono/zf-in-agda.git">https://github.com/shinji-kono/zf-in-agda.git +</a> +<p> +Category theory in Agda source +<br> <a href="https://github.com/shinji-kono/category-exercise-in-agda">https://github.com/shinji-kono/category-exercise-in-agda +</a> +<p> +</div> +<ol class="side" id="menu"> +Constructing ZF Set Theory in Agda +<li><a href="#content000"> ZF in Agda</a> +<li><a href="#content001"> Programming Mathematics</a> +<li><a href="#content002"> Target</a> +<li><a href="#content003"> Why Set Theory</a> +<li><a href="#content004"> Agda and Intuitionistic Logic </a> +<li><a href="#content005"> Introduction of Agda </a> +<li><a href="#content006"> data ( Sum type )</a> +<li><a href="#content007"> A → B means "A implies B"</a> +<li><a href="#content008"> introduction と elimination</a> +<li><a href="#content009"> To prove A → B </a> +<li><a href="#content010"> A ∧ B</a> +<li><a href="#content011"> record</a> +<li><a href="#content012"> Mathematical structure</a> +<li><a href="#content013"> A Model and a theory</a> +<li><a href="#content014"> postulate と module</a> +<li><a href="#content015"> A ∨ B</a> +<li><a href="#content016"> Negation</a> +<li><a href="#content017"> Equality </a> +<li><a href="#content018"> Equivalence relation</a> +<li><a href="#content019"> Ordering</a> +<li><a href="#content020"> Quantifier</a> +<li><a href="#content021"> Can we do math in this way?</a> +<li><a href="#content022"> Things which Agda cannot prove</a> +<li><a href="#content023"> Classical story of ZF Set Theory</a> +<li><a href="#content024"> Ordinals</a> +<li><a href="#content025"> Axiom of Ordinals</a> +<li><a href="#content026"> Concrete Ordinals</a> +<li><a href="#content027"> Model of Ordinals</a> +<li><a href="#content028"> Debugging axioms using Model</a> +<li><a href="#content029"> Countable Ordinals can contains uncountable set?</a> +<li><a href="#content030"> What is Set</a> +<li><a href="#content031"> We don't ask the contents of Set. It can be anything.</a> +<li><a href="#content032"> Ordinal Definable Set</a> +<li><a href="#content033"> ∋ in OD</a> +<li><a href="#content034"> 1 to 1 mapping between an OD and an Ordinal</a> +<li><a href="#content035"> Order preserving in the mapping of OD and Ordinal</a> +<li><a href="#content036"> ISO</a> +<li><a href="#content037"> Various Sets</a> +<li><a href="#content038"> Fixes on ZF to intuitionistic logic</a> +<li><a href="#content039"> Pure logical axioms</a> +<li><a href="#content040"> Axiom of Pair</a> +<li><a href="#content041"> pair in OD</a> +<li><a href="#content042"> Validity of Axiom of Pair</a> +<li><a href="#content043"> Equality of OD and Axiom of Extensionality </a> +<li><a href="#content044"> Validity of Axiom of Extensionality</a> +<li><a href="#content045"> Non constructive assumptions so far</a> +<li><a href="#content046"> Axiom which have negation form</a> +<li><a href="#content047"> Union </a> +<li><a href="#content048"> Axiom of replacement</a> +<li><a href="#content049"> Validity of Power Set Axiom</a> +<li><a href="#content050"> Axiom of regularity, Axiom of choice, ε-induction</a> +<li><a href="#content051"> Axiom of choice and Law of Excluded Middle</a> +<li><a href="#content052"> Relation-ship among ZF axiom</a> +<li><a href="#content053"> Non constructive assumption in our model</a> +<li><a href="#content054"> So it this correct?</a> +<li><a href="#content055"> How to use Agda Set Theory</a> +<li><a href="#content056"> Topos and Set Theory</a> +<li><a href="#content057"> Cardinal number and Continuum hypothesis</a> +<li><a href="#content058"> Filter</a> +<li><a href="#content059"> Programming Mathematics</a> +<li><a href="#content060"> link</a> +</ol> + +<hr/> Shinji KONO / Sat May 9 16:41:10 2020 +</body></html>
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/zf-in-agda.ind Sun Jun 07 20:31:30 2020 +0900 @@ -0,0 +1,1127 @@ +-title: Constructing ZF Set Theory in Agda + +--author: Shinji KONO + +--ZF in Agda + + zf.agda axiom of ZF + zfc.agda axiom of choice + Ordinals.agda axiom of Ordinals + ordinal.agda countable model of Ordinals + OD.agda model of ZF based on Ordinal Definable Set with assumptions + ODC.agda Law of exclude middle from axiom of choice assumptions + LEMC.agda model of choice with assumption of the Law of exclude middle + OPair.agda ordered pair on OD + + BAlgbra.agda Boolean algebra on OD (not yet done) + filter.agda Filter on OD (not yet done) + cardinal.agda Caedinal number on OD (not yet done) + + logic.agda some basics on logic + nat.agda some basics on Nat + +--Programming Mathematics + +Programming is processing data structure with λ terms. + +We are going to handle Mathematics in intuitionistic logic with λ terms. + +Mathematics is a functional programming which values are proofs. + +Programming ZF Set Theory in Agda + +--Target + + Describe ZF axioms in Agda + Construction a Model of ZF Set Theory in Agda + Show necessary assumptions for the model + Show validities of ZF axioms on the model + +This shows consistency of Set Theory (with some assumptions), +without circulating ZF Theory assumption. + +<a href="https://github.com/shinji-kono/zf-in-agda"> +ZF in Agda https://github.com/shinji-kono/zf-in-agda +</a> + +--Why Set Theory + +If we can formulate Set theory, it suppose to work on any mathematical theory. + +Set Theory is a difficult point for beginners especially axiom of choice. + +It has some amount of difficulty and self circulating discussion. + +I'm planning to do it in my old age, but I'm enough age now. + +This is done during from May to September. + +--Agda and Intuitionistic Logic + +Curry Howard Isomorphism + + Proposition : Proof ⇔ Type : Value + +which means + + constructing a typed lambda calculus which corresponds a logic + +Typed lambda calculus which allows complex type as a value of a variable (System FC) + + First class Type / Dependent Type + +Agda is a such a programming language which has similar syntax of Haskell + +Coq is specialized in proof assistance such as command and tactics . + +--Introduction of Agda + +A length of a list of type A. + + length : {A : Set } → List A → Nat + length [] = zero + length (_ ∷ t) = suc ( length t ) + +Simple functional programming language. Type declaration is mandatory. +A colon means type, an equal means value. Indentation based. + +Set is a base type (which may have a level ). + +{} means implicit variable which can be omitted if Agda infers its value. + +--data ( Sum type ) + +A data type which as exclusive multiple constructors. A similar one as +union in C or case class in Scala. + +It has a similar syntax as Haskell but it has a slight difference. + + data List (A : Set ) : Set where + [] : List A + _∷_ : A → List A → List A + +_∷_ means infix operator. If use explicit _, it can be used in a normal function +syntax. + +Natural number can be defined as a usual way. + + data Nat : Set where + zero : Nat + suc : Nat → Nat + +-- A → B means "A implies B" + +In Agda, a type can be a value of a variable, which is usually called dependent type. +Type has a name Set in Agda. + + ex3 : {A B : Set} → Set + ex3 {A}{B} = A → B + +ex3 is a type : A → B, which is a value of Set. It also means a formula : A implies B. + + A type is a formula, the value is the proof + +A value of A → B can be interpreted as an inference from the formula A to the formula B, which +can be a function from a proof of A to a proof of B. + +--introduction と elimination + +For a logical operator, there are two types of inference, an introduction and an elimination. + + intro creating symbol / constructor / introduction + elim using symbolic / accessors / elimination + +In Natural deduction, this can be written in proof schema. + + A + : + B A A → B + ------------- →intro ------------------ →elim + A → B B + +In Agda, this is a pair of type and value as follows. Introduction of → uses λ. + + →intro : {A B : Set } → A → B → ( A → B ) + →intro _ b = λ x → b + + →elim : {A B : Set } → A → ( A → B ) → B + →elim a f = f a + +Important + + {A B : Set } → A → B → ( A → B ) + +is + + {A B : Set } → ( A → ( B → ( A → B ) )) + +This makes currying of function easy. + +-- To prove A → B + +Make a left type as an argument. (intros in Coq) + + ex5 : {A B C : Set } → A → B → C → ? + ex5 a b c = ? + +? is called a hole, which is unspecified part. Agda tell us which kind type is required for the Hole. + +We are going to fill the holes, and if we have no warnings nor errors such as type conflict (Red), +insufficient proof or instance (Yellow), Non-termination, the proof is completed. + +-- A ∧ B + +Well known conjunction's introduction and elimination is as follow. + + A B A ∧ B A ∧ B + ------------- ----------- proj1 ---------- proj2 + A ∧ B A B + +We can introduce a corresponding structure in our functional programming language. + +-- record + + record _∧_ A B : Set + field + proj1 : A + proj2 : B + +_∧_ means infix operator. _∧_ A B can be written as A ∧ B (Haskell uses (∧) ) + +This a type which constructed from type A and type B. You may think this as an object +or struct. + + record { proj1 = x ; proj2 = y } + +is a constructor of _∧_. + + ex3 : {A B : Set} → A → B → ( A ∧ B ) + ex3 a b = record { proj1 = a ; proj2 = b } + + ex1 : {A B : Set} → ( A ∧ B ) → A + ex1 a∧b = proj1 a∧b + +a∧b is a variable name. If we have no spaces in a string, it is a word even if we have symbols +except parenthesis or colons. A symbol requires space separation such as a type defining colon. + +Defining record can be recursively, but we don't use the recursion here. + +-- Mathematical structure + +We have types of elements and the relationship in a mathematical structure. + + logical relation has no ordering + there is a natural ordering in arguments and a value in a function + +So we have typical definition style of mathematical structure with records. + + record IsOrdinals {n : Level} (ord : Set n) + (_o<_ : ord → ord → Set n) : Set (suc (suc n)) where + field + Otrans : {x y z : ord } → x o< y → y o< z → x o< z + + record Ordinals {n : Level} : Set (suc (suc n)) where + field + ord : Set n + _o<_ : ord → ord → Set n + isOrdinal : IsOrdinals ord _o<_ + +In IsOrdinals, axioms are written in flat way. In Ordinal, we may have +inputs and outputs are put in the field including IsOrdinal. + +Fields of Ordinal is existential objects in the mathematical structure. + +-- A Model and a theory + +Agda record is a type, so we can write it in the argument, but is it really exists? + +If we have a value of the record, it simply exists, that is, we need to create all the existence +in the record satisfies all the axioms (= field of IsOrdinal) should be valid. + + type of record = theory + value of record = model + +We call the value of the record as a model. If mathematical structure has a +model, it exists. Pretty Obvious. + +-- postulate と module + +Agda proofs are separated by modules, which are large records. + +postulates are assumptions. We can assume a type without proofs. + + postulate + sup-o : ( Ordinal → Ordinal ) → Ordinal + sup-o< : { ψ : Ordinal → Ordinal } → ∀ {x : Ordinal } → ψ x o< sup-o ψ + +sup-o is an example of upper bound of a function and sup-o< assumes it actually +satisfies all the value is less than upper bound. + +Writing some type in a module argument is the same as postulating a type, but +postulate can be written the middle of a proof. + +postulate can be constructive. + +postulate can be inconsistent, which result everything has a proof. + +-- A ∨ B + + data _∨_ (A B : Set) : Set where + case1 : A → A ∨ B + case2 : B → A ∨ B + +As Haskell, case1/case2 are patterns. + + ex3 : {A B : Set} → ( A ∨ A ) → A + ex3 = ? + +In a case statement, Agda command C-C C-C generates possible cases in the head. + + ex3 : {A B : Set} → ( A ∨ A ) → A + ex3 (case1 x) = ? + ex3 (case2 x) = ? + +Proof schema of ∨ is omit due to the complexity. + +-- Negation + + ⊥ + ------------- ⊥-elim + A + +Anything can be derived from bottom, in this case a Set A. There is no introduction rule +in ⊥, which can be implemented as data which has no constructor. + + data ⊥ : Set where + +⊥-elim can be proved like this. + + ⊥-elim : {A : Set } -> ⊥ -> A + ⊥-elim () + +() means no match argument nor value. + +A negation can be defined using ⊥ like this. + + ¬_ : Set → Set + ¬ A = A → ⊥ + +--Equality + +All the value in Agda are terms. If we have the same normalized form, two terms are equal. +If we have variables in the terms, we will perform an unification. unifiable terms are equal. +We don't go further on the unification. + + { x : A } x ≡ y f x y + --------------- ≡-intro --------------------- ≡-elim + x ≡ x f x x + +equality _≡_ can be defined as a data. + + data _≡_ {A : Set } : A → A → Set where + refl : {x : A} → x ≡ x + +The elimination of equality is a substitution in a term. + + subst : {A : Set } → { x y : A } → ( f : A → Set ) → x ≡ y → f x → f y + subst {A} {x} {y} f refl fx = fx + + ex5 : {A : Set} {x y z : A } → x ≡ y → y ≡ z → x ≡ z + ex5 {A} {x} {y} {z} x≡y y≡z = subst ( λ k → x ≡ k ) y≡z x≡y + + +--Equivalence relation + + refl' : {A : Set} {x : A } → x ≡ x + refl' = ? + sym : {A : Set} {x y : A } → x ≡ y → y ≡ x + sym = ? + trans : {A : Set} {x y z : A } → x ≡ y → y ≡ z → x ≡ z + trans = ? + cong : {A B : Set} {x y : A } { f : A → B } → x ≡ y → f x ≡ f y + cong = ? + +--Ordering + +Relation is a predicate on two value which has a same type. + + A → A → Set + +Defining order is the definition of this type with predicate or a data. + + data _≤_ : Rel ℕ 0ℓ where + z≤n : ∀ {n} → zero ≤ n + s≤s : ∀ {m n} (m≤n : m ≤ n) → suc m ≤ suc n + + +--Quantifier + +Handling quantifier in an intuitionistic logic requires special cares. + +In the input of a function, there are no restriction on it, that is, it has +a universal quantifier. (If we explicitly write ∀, Agda gives us a type inference on it) + +There is no ∃ in agda, the one way is using negation like this. + + ∃ (x : A ) → p x = ¬ ( ( x : A ) → ¬ ( p x ) ) + +On the another way, f : A can be used like this. + + p f + +If we use a function which can be defined globally which has stronger meaning the +usage of ∃ x in a logical expression. + + +--Can we do math in this way? + +Yes, we can. Actually we have Principia Mathematica by Russell and Whitehead (with out computer support). + +In some sense, this story is a reprinting of the work, (but Principia Mathematica has a different formulation than ZF). + + define mathematical structure as a record + program inferences as if we have proofs in variables + +--Things which Agda cannot prove + +The infamous Internal Parametricity is a limitation of Agda, it cannot prove so called Free Theorem, which +leads uniqueness of a functor in Category Theory. + +Functional extensionality cannot be proved. + (∀ x → f x ≡ g x) → f ≡ g + +Agda has no law of exclude middle. + + a ∨ ( ¬ a ) + +For example, (A → B) → ¬ B → ¬ A can be proved but, ( ¬ B → ¬ A ) → A → B cannot. + +It also other problems such as termination, type inference or unification which we may overcome with +efforts or devices or may not. + +If we cannot prove something, we can safely postulate it unless it leads a contradiction. + +--Classical story of ZF Set Theory + +Assuming ZF, constructing a model of ZF is a flow of classical Set Theory, which leads +a relative consistency proof of the Set Theory. +Ordinal number is used in the flow. + +In Agda, first we defines Ordinal numbers (Ordinals), then introduce Ordinal Definable Set (OD). +We need some non constructive assumptions in the construction. A model of Set theory is +constructed based on these assumptions. + +<center><img src="fig/set-theory.svg"></center> + +--Ordinals + +Ordinals are our intuition of infinite things, which has ∅ and orders on the things. +It also has a successor osuc. + + record Ordinals {n : Level} : Set (suc (suc n)) where + field + ord : Set n + o∅ : ord + osuc : ord → ord + _o<_ : ord → ord → Set n + isOrdinal : IsOrdinals ord o∅ osuc _o<_ + +It is different from natural numbers in way. The order of Ordinals is not defined in terms +of successor. It is given from outside, which make it possible to have higher order infinity. + +--Axiom of Ordinals + +Properties of infinite things. We request a transfinite induction, which states that if +some properties are satisfied below all possible ordinals, the properties are true on all +ordinals. + +Successor osuc has no ordinal between osuc and the base ordinal. There are some ordinals +which is not a successor of any ordinals. It is called limit ordinal. + +Any two ordinal can be compared, that is less, equal or more, that is total order. + + record IsOrdinals {n : Level} (ord : Set n) (o∅ : ord ) + (osuc : ord → ord ) + (_o<_ : ord → ord → Set n) : Set (suc (suc n)) where + field + Otrans : {x y z : ord } → x o< y → y o< z → x o< z + OTri : Trichotomous {n} _≡_ _o<_ + ¬x<0 : { x : ord } → ¬ ( x o< o∅ ) + <-osuc : { x : ord } → x o< osuc x + osuc-≡< : { a x : ord } → x o< osuc a → (x ≡ a ) ∨ (x o< a) + TransFinite : { ψ : ord → Set (suc n) } + → ( (x : ord) → ( (y : ord ) → y o< x → ψ y ) → ψ x ) + → ∀ (x : ord) → ψ x + +--Concrete Ordinals + +We can define a list like structure with level, which is a kind of two dimensional infinite array. + + data OrdinalD {n : Level} : (lv : Nat) → Set n where + Φ : (lv : Nat) → OrdinalD lv + OSuc : (lv : Nat) → OrdinalD {n} lv → OrdinalD lv + +The order of the OrdinalD can be defined in this way. + + data _d<_ {n : Level} : {lx ly : Nat} → OrdinalD {n} lx → OrdinalD {n} ly → Set n where + Φ< : {lx : Nat} → {x : OrdinalD {n} lx} → Φ lx d< OSuc lx x + s< : {lx : Nat} → {x y : OrdinalD {n} lx} → x d< y → OSuc lx x d< OSuc lx y + +This is a simple data structure, it has no abstract assumptions, and it is countable many data +structure. + + Φ 0 + OSuc 2 ( Osuc 2 ( Osuc 2 (Φ 2))) + Osuc 0 (Φ 0) d< Φ 1 + +--Model of Ordinals + +It is easy to show OrdinalD and its order satisfies the axioms of Ordinals. + +So our Ordinals has a mode. This means axiom of Ordinals are consistent. + +--Debugging axioms using Model + +Whether axiom is correct or not can be checked by a validity on a mode. + +If not, we may fix the axioms or the model, such as the definitions of the order. + +We can also ask whether the inputs exist. + +--Countable Ordinals can contains uncountable set? + +Yes, the ordinals contains any level of infinite Set in the axioms. + +If we handle real-number in the model, only countable number of real-number is used. + + from the outside view point, it is countable + from the internal view point, it is uncountable + +The definition of countable/uncountable is the same, but the properties are different +depending on the context. + +We don't show the definition of cardinal number here. + +--What is Set + +The word Set in Agda is not a Set of ZF Set, but it is a type (why it is named Set?). + +From naive point view, a set i a list, but in Agda, elements have all the same type. +A set in ZF may contain other Sets in ZF, which not easy to implement it as a list. + +Finite set may be written in finite series of ∨, but ... + +--We don't ask the contents of Set. It can be anything. + +From empty set φ, we can think a set contains a φ, and a pair of φ and the set, and so on, +and all of them, and again we repeat this. + + φ {φ} {φ,{φ}}, {φ,{φ},...} + +It is called V. + +This operation can be performed within a ZF Set theory. Classical Set Theory assumes +ZF, so this kind of thing is allowed. + +But in our case, we have no ZF theory, so we are going to use Ordinals. + + +--Ordinal Definable Set + +We can define a sbuset of Ordinals using predicates. What is a subset? + + a predicate has an Ordinal argument + +is an Ordinal Definable Set (OD). In Agda, OD is defined as follows. + + record OD : Set (suc n ) where + field + def : (x : Ordinal ) → Set n + +Ordinals itself is not a set in a ZF Set theory but a class. In OD, + + record { def = λ x → true } + +means Ordinals itself, so ODs are larger than a notion of ZF Set Theory, +but we don't care about it. + + +--∋ in OD + +OD is a predicate on Ordinals and it does not contains OD directly. If we have a mapping + + od→ord : OD → Ordinal + +we may check an OD is an element of the OD using def. + +A ∋ x can be define as follows. + + _∋_ : ( A x : OD ) → Set n + _∋_ A x = def A ( od→ord x ) + +In ψ : Ordinal → Set, if A is a record { def = λ x → ψ x } , then + + A x = def A ( od→ord x ) = ψ (od→ord x) + +--1 to 1 mapping between an OD and an Ordinal + + od→ord : OD → Ordinal + ord→od : Ordinal → OD + oiso : {x : OD } → ord→od ( od→ord x ) ≡ x + diso : {x : Ordinal } → od→ord ( ord→od x ) ≡ x + +They say the existing of the mappings can be proved in Classical Set Theory, but we +simply assumes these non constructively. + +We use postulate, it may contains additional restrictions which are not clear now. +It look like the mapping should be a subset of Ordinals, but we don't explicitly +state it. + +<center><img src="fig/ord-od-mapping.svg"></center> + +--Order preserving in the mapping of OD and Ordinal + +Ordinals have the order and OD has a natural order based on inclusion ( def / ∋ ). + + def y ( od→ord x ) + +An elements of OD should be defined before the OD, that is, an ordinal corresponding an elements +have to be smaller than the corresponding ordinal of the containing OD. + + c<→o< : {x y : OD } → def y ( od→ord x ) → od→ord x o< od→ord y + +This is also said to be provable in classical Set Theory, but we simply assumes it. + +OD has an order based on the corresponding ordinal, but it may not have corresponding def / ∋ +relation. This means the reverse order preservation, + + o<→c< : {n : Level} {x y : Ordinal } → x o< y → def (ord→od y) x + +is not valid. If we assumes it, ∀ x ∋ ∅ becomes true, which manes all OD becomes Ordinals in +the model. + +<center><img src="fig/ODandOrdinals.svg"></center> + +--ISO + +It also requires isomorphisms, + + oiso : {x : OD } → ord→od ( od→ord x ) ≡ x + diso : {x : Ordinal } → od→ord ( ord→od x ) ≡ x + + +--Various Sets + +In classical Set Theory, there is a hierarchy call L, which can be defined by a predicate. + + Ordinal / things satisfies axiom of Ordinal / extension of natural number + V / hierarchical construction of Set from φ + L / hierarchical predicate definable construction of Set from φ + OD / equational formula on Ordinals + Agda Set / Type / it also has a level + + +--Fixes on ZF to intuitionistic logic + +We use ODs as Sets in ZF, and defines record ZF, that is, we have to define +ZF axioms in Agda. + +It may not valid in our model. We have to debug it. + +Fixes are depends on axioms. + +<center><img src="fig/axiom-type.svg"></center> + +<a href="fig/zf-record.html"> +ZFのrecord +</a> + +--Pure logical axioms + + empty, pair, select, ε-induction??infinity + +These are logical relations among OD. + + empty : ∀( x : ZFSet ) → ¬ ( ∅ ∋ x ) + pair→ : ( x y t : ZFSet ) → (x , y) ∋ t → ( t ≈ x ) ∨ ( t ≈ y ) + pair← : ( x y t : ZFSet ) → ( t ≈ x ) ∨ ( t ≈ y ) → (x , y) ∋ t + selection : { ψ : ZFSet → Set m } → ∀ { X y : ZFSet } → ( ( y ∈ X ) ∧ ψ y ) ⇔ (y ∈ Select X ψ ) + infinity∅ : ∅ ∈ infinite + infinity : ∀( x : ZFSet ) → x ∈ infinite → ( x ∪ ( x , x ) ) ∈ infinite + ε-induction : { ψ : OD → Set (suc n)} + → ( {x : OD } → ({ y : OD } → x ∋ y → ψ y ) → ψ x ) + → (x : OD ) → ψ x + +finitely can be define by Agda data. + + data infinite-d : ( x : Ordinal ) → Set n where + iφ : infinite-d o∅ + isuc : {x : Ordinal } → infinite-d x → + infinite-d (od→ord ( Union (ord→od x , (ord→od x , ord→od x ) ) )) + +Union (x , ( x , x )) should be an direct successor of x, but we cannot prove it in our model. + +--Axiom of Pair + +In the Tanaka's book, axiom of pair is as follows. + + ∀ x ∀ y ∃ z ∀ t ( z ∋ t ↔ t ≈ x ∨ t ≈ y) + +We have fix ∃ z, a function (x , y) is defined, which is _,_ . + + _,_ : ( A B : ZFSet ) → ZFSet + +using this, we can define two directions in separates axioms, like this. + + pair→ : ( x y t : ZFSet ) → (x , y) ∋ t → ( t ≈ x ) ∨ ( t ≈ y ) + pair← : ( x y t : ZFSet ) → ( t ≈ x ) ∨ ( t ≈ y ) → (x , y) ∋ t + +This is already written in Agda, so we use these as axioms. All inputs have ∀. + +--pair in OD + +OD is an equation on Ordinals, we can simply write axiom of pair in the OD. + + _,_ : OD → OD → OD + x , y = record { def = λ t → (t ≡ od→ord x ) ∨ ( t ≡ od→ord y ) } + +≡ is an equality of λ terms, but please not that this is equality on Ordinals. + +--Validity of Axiom of Pair + +Assuming ZFSet is OD, we are going to prove pair→ . + + pair→ : ( x y t : OD ) → (x , y) ∋ t → ( t == x ) ∨ ( t == y ) + pair→ x y t p = ? + +In this program, type of p is ( x , y ) ∋ t , that is +def ( x , y ) that is, (t ≡ od→ord x ) ∨ ( t ≡ od→ord y ) . + +Since _∨_ is a data, it can be developed as (C-c C-c : agda2-make-case ). + + pair→ x y t (case1 t≡x ) = ? + pair→ x y t (case2 t≡y ) = ? + +The type of the ? is ( t == x ) ∨ ( t == y ), again it is data _∨_ . + + pair→ x y t (case1 t≡x ) = case1 ? + pair→ x y t (case2 t≡y ) = case2 ? + +The ? in case1 is t == x, so we have to create this from t≡x, which is a name of a variable +which type is + + t≡x : od→ord t ≡ od→ord x + +which is shown by an Agda command (C-C C-E : agda2-show-context ). + +But we haven't defined == yet. + +--Equality of OD and Axiom of Extensionality + +OD is defined by a predicates, if we compares normal form of the predicates, even if +it contains the same elements, it may be different, which is no good as an equality of +Sets. + +Axiom of Extensionality requires sets having the same elements are handled in the same way +each other. + + ∀ z ( z ∈ x ⇔ z ∈ y ) ⇒ ∀ w ( x ∈ w ⇔ y ∈ w ) + +We can write this axiom in Agda as follows. + + extensionality : { A B w : ZFSet } → ( (z : ZFSet) → ( A ∋ z ) ⇔ (B ∋ z) ) → ( A ∈ w ⇔ B ∈ w ) + +So we use ( A ∋ z ) ⇔ (B ∋ z) as an equality (_==_) of our model. We have to show +A ∈ w ⇔ B ∈ w from A == B. + +x == y can be defined in this way. + + record _==_ ( a b : OD ) : Set n where + field + eq→ : ∀ { x : Ordinal } → def a x → def b x + eq← : ∀ { x : Ordinal } → def b x → def a x + +Actually, (z : OD) → (A ∋ z) ⇔ (B ∋ z) implies A == B. + + extensionality0 : {A B : OD } → ((z : OD) → (A ∋ z) ⇔ (B ∋ z)) → A == B + eq→ (extensionality0 {A} {B} eq ) {x} d = ? + eq← (extensionality0 {A} {B} eq ) {x} d = ? + +? are def B x and def A x and these are generated from eq : (z : OD) → (A ∋ z) ⇔ (B ∋ z) . + +Actual proof is rather complicated. + + eq→ (extensionality0 {A} {B} eq ) {x} d = def-iso {A} {B} (sym diso) (proj1 (eq (ord→od x))) d + eq← (extensionality0 {A} {B} eq ) {x} d = def-iso {B} {A} (sym diso) (proj2 (eq (ord→od x))) d + +where + + def-iso : {A B : OD } {x y : Ordinal } → x ≡ y → (def A y → def B y) → def A x → def B x + def-iso refl t = t + +--Validity of Axiom of Extensionality + +If we can derive (w ∋ A) ⇔ (w ∋ B) from A == B, the axiom becomes valid, but it seems impossible, +so we assumes + + ==→o≡ : { x y : OD } → (x == y) → x ≡ y + +Using this, we have + + extensionality : {A B w : OD } → ((z : OD ) → (A ∋ z) ⇔ (B ∋ z)) → (w ∋ A) ⇔ (w ∋ B) + proj1 (extensionality {A} {B} {w} eq ) d = subst (λ k → w ∋ k) ( ==→o≡ (extensionality0 {A} {B} eq) ) d + proj2 (extensionality {A} {B} {w} eq ) d = subst (λ k → w ∋ k) (sym ( ==→o≡ (extensionality0 {A} {B} eq) )) d + +This assumption means we may have an equivalence set on any predicates. + +--Non constructive assumptions so far + +We have correspondence between OD and Ordinals and one directional order preserving. + +We also have equality assumption. + + od→ord : OD → Ordinal + ord→od : Ordinal → OD + oiso : {x : OD } → ord→od ( od→ord x ) ≡ x + diso : {x : Ordinal } → od→ord ( ord→od x ) ≡ x + c<→o< : {x y : OD } → def y ( od→ord x ) → od→ord x o< od→ord y + ==→o≡ : { x y : OD } → (x == y) → x ≡ y + + +--Axiom which have negation form + + Union, Selection + +These axioms contains ∃ x as a logical relation, which can be described in ¬ ( ∀ x ( ¬ p )). + +Axiom of replacement uses upper bound of function on Ordinals, which makes it non-constructive. + +Power Set axiom requires double negation, + + power→ : ∀( A t : ZFSet ) → Power A ∋ t → ∀ {x} → t ∋ x → ¬ ¬ ( A ∋ x ) + power← : ∀( A t : ZFSet ) → t ⊆_ A → Power A ∋ t + +If we have an assumption of law of exclude middle, we can recover the original A ∋ x form. + +--Union + +The original form of the Axiom of Union is + + ∀ x ∃ y ∀ z (z ∈ y ⇔ ∃ u ∈ x ∧ (z ∈ u)) + +Union requires the existence of b in a ⊇ ∃ b ∋ x . We will use negation form of ∃. + + union→ : ( X z u : ZFSet ) → ( X ∋ u ) ∧ (u ∋ z ) → Union X ∋ z + union← : ( X z : ZFSet ) → (X∋z : Union X ∋ z ) → ¬ ( (u : ZFSet ) → ¬ ((X ∋ u) ∧ (u ∋ z ))) + +The definition of Union in OD is like this. + + Union : OD → OD + Union U = record { def = λ x → ¬ (∀ (u : Ordinal ) → ¬ ((def U u) ∧ (def (ord→od u) x))) } + +Proof of validity is straight forward. + + union→ : (X z u : OD) → (X ∋ u) ∧ (u ∋ z) → Union X ∋ z + union→ X z u xx not = ⊥-elim ( not (od→ord u) ( record { proj1 = proj1 xx + ; proj2 = subst ( λ k → def k (od→ord z)) (sym oiso) (proj2 xx) } )) + union← : (X z : OD) (X∋z : Union X ∋ z) → ¬ ( (u : OD ) → ¬ ((X ∋ u) ∧ (u ∋ z ))) + union← X z UX∋z = FExists _ lemma UX∋z where + lemma : {y : Ordinal} → def X y ∧ def (ord→od y) (od→ord z) → ¬ ((u : OD) → ¬ (X ∋ u) ∧ (u ∋ z)) + lemma {y} xx not = not (ord→od y) record { proj1 = subst ( λ k → def X k ) (sym diso) (proj1 xx ) ; proj2 = proj2 xx } + +where + + FExists : {m l : Level} → ( ψ : Ordinal → Set m ) + → {p : Set l} ( P : { y : Ordinal } → ψ y → ¬ p ) + → (exists : ¬ (∀ y → ¬ ( ψ y ) )) + → ¬ p + FExists {m} {l} ψ {p} P = contra-position ( λ p y ψy → P {y} ψy p ) + +which checks existence using contra-position. + +--Axiom of replacement + +We can replace the elements of a set by a function and it becomes a set. From the book, + + ∀ x ∀ y ∀ z ( ( ψ ( x , y ) ∧ ψ ( x , z ) ) → y = z ) → ∀ X ∃ A ∀ y ( y ∈ A ↔ ∃ x ∈ X ψ ( x , y ) ) + +The existential quantifier can be related by a function, + + Replace : OD → (OD → OD ) → OD + +The axioms becomes as follows. + + replacement← : {ψ : ZFSet → ZFSet} → ∀ ( X x : ZFSet ) → x ∈ X → ψ x ∈ Replace X ψ + replacement→ : {ψ : ZFSet → ZFSet} → ∀ ( X x : ZFSet ) → ( lt : x ∈ Replace X ψ ) → ¬ ( ∀ (y : ZFSet) → ¬ ( x ≈ ψ y ) ) + +In the axiom, the existence of the original elements is necessary. In order to do that we use OD which has +negation form of existential quantifier in the definition. + + in-codomain : (X : OD ) → ( ψ : OD → OD ) → OD + in-codomain X ψ = record { def = λ x → ¬ ( (y : Ordinal ) → ¬ ( def X y ∧ ( x ≡ od→ord (ψ (ord→od y ))))) } + +Besides this upper bounds is required. + + Replace : OD → (OD → OD ) → OD + Replace X ψ = record { def = λ x → (x o< sup-o ( λ x → od→ord (ψ (ord→od x )))) ∧ def (in-codomain X ψ) x } + +We omit the proof of the validity, but it is rather straight forward. + +--Validity of Power Set Axiom + +The original Power Set Axiom is this. + + ∀ X ∃ A ∀ t ( t ∈ A ↔ t ⊆ X ) ) + +The existential quantifier is replaced by a function + + Power : ( A : OD ) → OD + +t ⊆ X is a record like this. + + record _⊆_ ( A B : OD ) : Set (suc n) where + field + incl : { x : OD } → A ∋ x → B ∋ x + +Axiom becomes likes this. + + power→ : ( A t : OD) → Power A ∋ t → {x : OD} → t ∋ x → ¬ ¬ (A ∋ x) + power← : (A t : OD) → ({x : OD} → (t ∋ x → A ∋ x)) → Power A ∋ t + +The validity of the axioms are slight complicated, we have to define set of all subset. We define +subset in a different form. + + ZFSubset : (A x : OD ) → OD + ZFSubset A x = record { def = λ y → def A y ∧ def x y } + +We can prove, + + ( {y : OD } → x ∋ y → ZFSubset A x ∋ y ) ⇔ ( x ⊆ A ) + +We only have upper bound as an ordinal, but we have an obvious OD based on the order of Ordinals, +which is an Ordinals with our Model. + + Ord : ( a : Ordinal ) → OD + Ord a = record { def = λ y → y o< a } + + Def : (A : OD ) → OD + Def A = Ord ( sup-o ( λ x → od→ord ( ZFSubset A (ord→od x )) ) ) + +This is slight larger than Power A, so we replace all elements x by A ∩ x (some of them may empty). + + Power : OD → OD + Power A = Replace (Def (Ord (od→ord A))) ( λ x → A ∩ x ) + +Creating Power Set of Ordinals is rather easy, then we use replacement axiom on A ∩ x since we have this. + + ∩-≡ : { a b : OD } → ({x : OD } → (a ∋ x → b ∋ x)) → a == ( b ∩ a ) + +In case of Ord a intro of Power Set axiom becomes valid. + + ord-power← : (a : Ordinal ) (t : OD) → ({x : OD} → (t ∋ x → (Ord a) ∋ x)) → Def (Ord a) ∋ t + +Using this, we can prove, + + power→ : ( A t : OD) → Power A ∋ t → {x : OD} → t ∋ x → ¬ ¬ (A ∋ x) + power← : (A t : OD) → ({x : OD} → (t ∋ x → A ∋ x)) → Power A ∋ t + + +--Axiom of regularity, Axiom of choice, ε-induction + +Axiom of regularity requires non self intersectable elements (which is called minimum), if we +replace it by a function, it becomes a choice function. It makes axiom of choice valid. + +This means we cannot prove axiom regularity form our model, and if we postulate this, axiom of +choice also becomes valid. + + minimal : (x : OD ) → ¬ (x == od∅ )→ OD + x∋minimal : (x : OD ) → ( ne : ¬ (x == od∅ ) ) → def x ( od→ord ( minimal x ne ) ) + minimal-1 : (x : OD ) → ( ne : ¬ (x == od∅ ) ) → (y : OD ) → ¬ ( def (minimal x ne) (od→ord y)) ∧ (def x (od→ord y) ) + +We can avoid this using ε-induction (a predicate is valid on all set if the predicate is true on some element of set). +Assuming law of exclude middle, they say axiom of regularity will be proved, but we haven't check it yet. + + ε-induction : { ψ : OD → Set (suc n)} + → ( {x : OD } → ({ y : OD } → x ∋ y → ψ y ) → ψ x ) + → (x : OD ) → ψ x + +In our model, we assumes the mapping between Ordinals and OD, this is actually the TransFinite induction in Ordinals. + +The axiom of choice in the book is complicated using any pair in a set, so we use use a form in the Wikipedia. + + ∀ X [ ∅ ∉ X → (∃ f : X → ⋃ X ) → ∀ A ∈ X ( f ( A ) ∈ A ) ] + +We can formulate like this. + + choice-func : (X : ZFSet ) → {x : ZFSet } → ¬ ( x ≈ ∅ ) → ( X ∋ x ) → ZFSet + choice : (X : ZFSet ) → {A : ZFSet } → ( X∋A : X ∋ A ) → (not : ¬ ( A ≈ ∅ )) → A ∋ choice-func X not X∋A + +It does not requires ∅ ∉ X . + +--Axiom of choice and Law of Excluded Middle + +In our model, since OD has a mapping to Ordinals, it has evident order, which means well ordering theorem is valid, +but it don't have correct form of the axiom yet. They say well ordering axiom is equivalent to the axiom of choice, +but it requires law of the exclude middle. + +Actually, it is well known to prove law of the exclude middle from axiom of choice in intuitionistic logic, and we can +perform the proof in our mode. Using the definition like this, predicates and ODs are related and we can ask the +set is empty or not if we have an axiom of choice, so we have the law of the exclude middle p ∨ ( ¬ p ) . + + ppp : { p : Set n } { a : OD } → record { def = λ x → p } ∋ a → p + ppp {p} {a} d = d + +We can prove axiom of choice from law excluded middle since we have TransFinite induction. So Axiom of choice +and Law of Excluded Middle is equivalent in our mode. + +--Relation-ship among ZF axiom + +<center><img src="fig/axiom-dependency.svg"></center> + +--Non constructive assumption in our model + +mapping between OD and Ordinals + + od→ord : OD → Ordinal + ord→od : Ordinal → OD + oiso : {x : OD } → ord→od ( od→ord x ) ≡ x + diso : {x : Ordinal } → od→ord ( ord→od x ) ≡ x + c<→o< : {x y : OD } → def y ( od→ord x ) → od→ord x o< od→ord y + +Equivalence on OD + + ==→o≡ : { x y : OD } → (x == y) → x ≡ y + +Upper bound + + sup-o : ( Ordinal → Ordinal ) → Ordinal + sup-o< : { ψ : Ordinal → Ordinal } → ∀ {x : Ordinal } → ψ x o< sup-o ψ + +Axiom of choice and strong axiom of regularity. + + minimal : (x : OD ) → ¬ (x == od∅ )→ OD + x∋minimal : (x : OD ) → ( ne : ¬ (x == od∅ ) ) → def x ( od→ord ( minimal x ne ) ) + minimal-1 : (x : OD ) → ( ne : ¬ (x == od∅ ) ) → (y : OD ) → ¬ ( def (minimal x ne) (od→ord y)) ∧ (def x (od→ord y) ) + +--So it this correct? + +Our axiom are syntactically the same in the text book, but negations are slightly different. + +If we assumes excluded middle, these are exactly same. + +Even if we assumes excluded middle, intuitionistic logic itself remains consistent, but we cannot prove it. + +Except the upper bound, axioms are simple logical relation. + +Proof of existence of mapping between OD and Ordinals are not obvious. We don't know we prove it or not. + +Existence of the Upper bounds is a pure assumption, if we have not limit on Ordinals, it may contradicts, +but we don't have explicit upper limit on Ordinals. + +Several inference on our model or our axioms are basically parallel to the set theory text book, so it looks like correct. + +--How to use Agda Set Theory + +Assuming record ZF, classical set theory can be developed. If necessary, axiom of choice can be +postulated or assuming law of excluded middle. + +Instead, simply assumes non constructive assumption, various theory can be developed. We haven't check +these assumptions are proved in record ZF, so we are not sure, these development is a result of ZF Set theory. + +ZF record itself is not necessary, for example, topology theory without ZF can be possible. + +--Topos and Set Theory + +Topos is a mathematical structure in Category Theory, which is a Cartesian closed category which has a +sub-object classifier. + +Topos itself is model of intuitionistic logic. + +Transitive Sets are objects of Cartesian closed category. +It is possible to introduce Power Set Functor on it + +We can use replacement A ∩ x for each element in Transitive Set, +in the similar way of our power set axiom. I + +A model of ZF Set theory can be constructed on top of the Topos which is shown in Oisus. + +Our Agda model is a proof theoretic version of it. + +--Cardinal number and Continuum hypothesis + +Axiom of choice is required to define cardinal number + +definition of cardinal number is not yet done + +definition of filter is not yet done + +we may have a model without axiom of choice or without continuum hypothesis + +Possible representation of continuum hypothesis is this. + + continuum-hyphotheis : (a : Ordinal) → Power (Ord a) ⊆ Ord (osuc a) + +--Filter + +filter is a dual of ideal on boolean algebra or lattice. Existence on natural number +is depends on axiom of choice. + + record Filter ( L : OD ) : Set (suc n) where + field + filter : OD + proper : ¬ ( filter ∋ od∅ ) + inL : filter ⊆ L + filter1 : { p q : OD } → q ⊆ L → filter ∋ p → p ⊆ q → filter ∋ q + filter2 : { p q : OD } → filter ∋ p → filter ∋ q → filter ∋ (p ∩ q) + +We may construct a model of non standard analysis or set theory. + +This may be simpler than classical forcing theory ( not yet done). + +--Programming Mathematics + +Mathematics is a functional programming in Agda where proof is a value of a variable. The mathematical +structure are + + record and data + +Proof is check by type consistency not by the computation, but it may include some normalization. + +Type inference and termination is not so clear in multi recursions. + +Defining Agda record is a good way to understand mathematical theory, for examples, + + Category theory ( Yoneda lemma, Floyd Adjunction functor theorem, Applicative functor ) + Automaton ( Subset construction、Language containment) + +are proved in Agda. + +--link + +Summer school of foundation of mathematics (in Japanese) +<br> <a href="https://www.sci.shizuoka.ac.jp/~math/yorioka/ss2019/"> +https://www.sci.shizuoka.ac.jp/~math/yorioka/ss2019/ +</a> + +Foundation of axiomatic set theory (in Japanese) +<br> <a href="https://www.sci.shizuoka.ac.jp/~math/yorioka/ss2019/sakai0.pdf"> +https://www.sci.shizuoka.ac.jp/~math/yorioka/ss2019/sakai0.pdf +</a> + +Agda +<br> <a href="https://agda.readthedocs.io/en/v2.6.0.1/"> +https://agda.readthedocs.io/en/v2.6.0.1/ +</a> + +ZF-in-Agda source +<br> <a href="https://github.com/shinji-kono/zf-in-agda.git"> +https://github.com/shinji-kono/zf-in-agda.git +</a> + +Category theory in Agda source +<br> <a href="https://github.com/shinji-kono/category-exercise-in-agda"> +https://github.com/shinji-kono/category-exercise-in-agda +</a> + + +
--- a/zf.agda Thu Aug 29 16:18:37 2019 +0900 +++ b/zf.agda Sun Jun 07 20:31:30 2020 +0900 @@ -19,7 +19,7 @@ (Select : (X : ZFSet ) → ( ψ : (x : ZFSet ) → Set m ) → ZFSet ) (Replace : ZFSet → ( ZFSet → ZFSet ) → ZFSet ) (infinite : ZFSet) - : Set (suc (n ⊔ m)) where + : Set (suc (n ⊔ suc m)) where field isEquivalence : IsEquivalence {n} {m} {ZFSet} _≈_ -- ∀ x ∀ y ∃ z ∀ t ( z ∋ t → t ≈ x ∨ t ≈ y) @@ -35,7 +35,7 @@ _∩_ : ( A B : ZFSet ) → ZFSet A ∩ B = Select A ( λ x → ( A ∋ x ) ∧ ( B ∋ x ) ) _∪_ : ( A B : ZFSet ) → ZFSet - A ∪ B = Union (A , B) -- Select A ( λ x → ( A ∋ x ) ∨ ( B ∋ x ) ) is easier + A ∪ B = Union (A , B) ｛_｝ : ZFSet → ZFSet ｛ x ｝ = ( x , x ) infixr 200 _∈_ @@ -48,14 +48,10 @@ power← : ∀( A t : ZFSet ) → ( ∀ {x} → _⊆_ t A {x}) → Power A ∋ t -- extensionality : ∀ z ( z ∈ x ⇔ z ∈ y ) ⇒ ∀ w ( x ∈ w ⇔ y ∈ w ) extensionality : { A B w : ZFSet } → ( (z : ZFSet) → ( A ∋ z ) ⇔ (B ∋ z) ) → ( A ∈ w ⇔ B ∈ w ) - -- This form of regurality forces choice function - -- regularity : ∀ x ( x ≠ ∅ → ∃ y ∈ x ( y ∩ x = ∅ ) ) - -- minimul : (x : ZFSet ) → ¬ (x ≈ ∅) → ZFSet - -- regularity : ∀( x : ZFSet ) → (not : ¬ (x ≈ ∅)) → ( minimul x not ∈ x ∧ ( minimul x not ∩ x ≈ ∅ ) ) - -- another form of regularity - -- ε-induction : { ψ : ZFSet → Set m} - -- → ( {x : ZFSet } → ({ y : ZFSet } → x ∋ y → ψ y ) → ψ x ) - -- → (x : ZFSet ) → ψ x + -- regularity without minimum + ε-induction : { ψ : ZFSet → Set (suc m)} + → ( {x : ZFSet } → ({ y : ZFSet } → x ∋ y → ψ y ) → ψ x ) + → (x : ZFSet ) → ψ x -- infinity : ∃ A ( ∅ ∈ A ∧ ∀ x ∈ A ( x ∪ { x } ∈ A ) ) infinity∅ : ∅ ∈ infinite infinity : ∀( x : ZFSet ) → x ∈ infinite → ( x ∪ ｛ x ｝) ∈ infinite @@ -63,11 +59,8 @@ -- replacement : ∀ x ∀ y ∀ z ( ( ψ ( x , y ) ∧ ψ ( x , z ) ) → y = z ) → ∀ X ∃ A ∀ y ( y ∈ A ↔ ∃ x ∈ X ψ ( x , y ) ) replacement← : {ψ : ZFSet → ZFSet} → ∀ ( X x : ZFSet ) → x ∈ X → ψ x ∈ Replace X ψ replacement→ : {ψ : ZFSet → ZFSet} → ∀ ( X x : ZFSet ) → ( lt : x ∈ Replace X ψ ) → ¬ ( ∀ (y : ZFSet) → ¬ ( x ≈ ψ y ) ) - -- ∀ X [ ∅ ∉ X → (∃ f : X → ⋃ X ) → ∀ A ∈ X ( f ( A ) ∈ A ) ] - choice-func : (X : ZFSet ) → {x : ZFSet } → ¬ ( x ≈ ∅ ) → ( X ∋ x ) → ZFSet - choice : (X : ZFSet ) → {A : ZFSet } → ( X∋A : X ∋ A ) → (not : ¬ ( A ≈ ∅ )) → A ∋ choice-func X not X∋A -record ZF {n m : Level } : Set (suc (n ⊔ m)) where +record ZF {n m : Level } : Set (suc (n ⊔ suc m)) where infixr 210 _,_ infixl 200 _∋_ infixr 220 _≈_
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/zfc.agda Sun Jun 07 20:31:30 2020 +0900 @@ -0,0 +1,34 @@ +module zfc where + +open import Level +open import Relation.Binary +open import Relation.Nullary +open import logic + +record IsZFC {n m : Level } + (ZFSet : Set n) + (_∋_ : ( A x : ZFSet ) → Set m) + (_≈_ : Rel ZFSet m) + (∅ : ZFSet) + (Select : (X : ZFSet ) → ( ψ : (x : ZFSet ) → Set m ) → ZFSet ) + : Set (suc (n ⊔ suc m)) where + field + -- ∀ X [ ∅ ∉ X → (∃ f : X → ⋃ X ) → ∀ A ∈ X ( f ( A ) ∈ A ) ] + choice-func : (X : ZFSet ) → {x : ZFSet } → ¬ ( x ≈ ∅ ) → ( X ∋ x ) → ZFSet + choice : (X : ZFSet ) → {A : ZFSet } → ( X∋A : X ∋ A ) → (not : ¬ ( A ≈ ∅ )) → A ∋ choice-func X not X∋A + infixr 200 _∈_ + infixr 230 _∩_ + _∈_ : ( A B : ZFSet ) → Set m + A ∈ B = B ∋ A + _∩_ : ( A B : ZFSet ) → ZFSet + A ∩ B = Select A ( λ x → ( A ∋ x ) ∧ ( B ∋ x ) ) + +record ZFC {n m : Level } : Set (suc (n ⊔ suc m)) where + field + ZFSet : Set n + _∋_ : ( A x : ZFSet ) → Set m + _≈_ : ( A B : ZFSet ) → Set m + ∅ : ZFSet + Select : (X : ZFSet ) → ( ψ : (x : ZFSet ) → Set m ) → ZFSet + isZFC : IsZFC ZFSet _∋_ _≈_ ∅ Select +