...
 
Commits (2)
namespace http://mathhub.info/MitM/smglom ❚
import base http://mathhub.info/MitM/Foundation ❚
import sig http://gl.mathhub.info/MMT/LFX/Sigma ❚
import lfxcop http://gl.mathhub.info/MMT/LFX/Coproducts❚
theory DependentIf : base:?Logic =
include sig:?LFSigma ❙
// probably wrong . This is just a guess how one would implement a ifthenelse that doesn't loose its information about branching condition using fake pattern matching ❙
dependentIf : {A : type}{B : type} {a : A} {cond : A ⟶ bool} ( ⊦ cond a ≐ true ⟶ B ) ⟶ (⊦ cond a ≐ false ⟶ B) ⟶ B❙
dependentIf_true : {A : type}{B : type} {a : A} {cond : A ⟶ bool} {bt : ⊦ cond a ≐ true ⟶ B } {bf : ⊦ cond a ≐ false ⟶ B} {h : ⊦ cond a ≐ true} ⊦ dependentIf A B a cond bt bf ≐ bt h ❙
dependentIf_false : {A : type}{B : type} {a : A} {cond : A ⟶ bool} {bt : ⊦ cond a ≐ true ⟶ B } {bf : ⊦ cond a ≐ false ⟶ B} {h : ⊦ cond a ≐ false} ⊦ dependentIf A B a cond bt bf ≐ bf h ❙
theory CoproductIf : base:?Logic =
include lfxcop:?LFCoprod ❙
copIf : ❙
......@@ -3,14 +3,13 @@ namespace http://mathhub.info/MitM/smglom ❚
import base http://mathhub.info/MitM/Foundation ❚
import arith http://mathhub.info/MitM/smglom/arithmetics ❚
import sigma http://gl.mathhub.info/MMT/LFX/Sigma
// import sub http://gl.mathhub.info/MMT/LFX/Subtyping
theory FinSequences : base:?Logic =
include arith:?NaturalArithmetics ❙
include sigma:?LFSigma ❙
include base:?OptionType ❙
finiteSequence : ℕ ⟶ type ⟶ type ❘ = [n , A] Σ x : nat ⟶ Option A . ∀
finiteSequence : ℕ ⟶ type ⟶ type ❘ = [n , A] ⟨ f : nat ⟶ Option A . f 0 = None ∧ (∀ [i] n < i ⇒ f i ≐ None) ∧ (∀ [x] 0 < x ⇒ x ≤ n ⇒ f x ≠ None) ⟩
......@@ -3,7 +3,7 @@ namespace http://mathhub.info/MitM/smglom ❚
import base http://mathhub.info/MitM/Foundation ❚
import arith http://mathhub.info/MitM/smglom/arithmetics ❚
import copro http://gl.mathhub.info/MMT/LFX/Coproducts ❚
// import copro http://gl.mathhub.info/MMT/LFX/Coproducts ❚
......@@ -33,8 +33,7 @@ theory FinSeqProps : base:?Logic =
theory FinSeqFunctions : base:?InductiveTypes =
include ?FinSequences ❙
include arith:?INatProps❙
include http://gl.mathhub.info/MMT/LFX/Coproducts?LFCoprod ❙
// include http://gl.mathhub.info/MMT/LFX/Coproducts?LFCoprod ❙
finiteSequenceMap : {A : type} {B : type} {n : ℕ} finSeq n A ⟶ (A ⟶ B) ⟶ finSeq n B ❘= [A , B , n , fn , mp] [a ,b ,c] mp (fn a b c) ❘ # finSeqMap 4 5 ❙
......@@ -42,10 +41,14 @@ theory FinSeqFunctions : base:?InductiveTypes =
// helper for finiteSequenceFoldLeft ❙
finiteSequenceFoldLeftLoop : {A : type}{B : type}{n : ℕ}{m : ℕ} (A ⟶ B ⟶ A) ⟶ A ⟶ finSeq n B ⟶ A ❘ = [A , B , n , m , f , start , fs] incIf ❙
// also : fake pattern matching ❙
finiteSequenceFoldLeftLoop : {A : type}{B : type}{n : ℕ}{m : ℕ} ⊦ 0 < n ⟶ ⊦ n ≤ m ⟶ (A ⟶ B ⟶ A) ⟶ A ⟶ finSeq n B ⟶ A ❙
finiteSequenceFoldLeftLoopS : {A : type}{B : type}{n : ℕ}{m : ℕ} { h : ⊦ 0 < n} { h0 : ⊦ n ≤ m} {f : (A ⟶ B ⟶ A)} {start : A} {fn : finSeq n B} ⊦ finiteSequenceFoldLeftLoop ❙
finiteSequenceFoldLeft : {A : type}{B : type} {n : ℕ} (A ⟶ B ⟶ A) ⟶ A ⟶ finSeq n B ⟶ A ❘ # finSeqFoldL 1 2 3 4 5 6 ❙
finiteSequenceFoldLeftBZ : {A : type}{B : type}{f : A ⟶ B ⟶ A}{start : A}{fs : finSeq 0 B} ⊦ finiteSequenceFoldLeft A B 0 f start fs ≐ start❙
// finiteSequenceFoldLeft : {A : type}{B : type} {n : ℕ} (A ⟶ B ⟶ A) ⟶ A ⟶ finSeq n B ⟶ A ❘ # finSeqFoldL 1 2 3 4 5 6 ❙
// finiteSequenceFoldLeftBZ : {A : type}{B : type}{f : A ⟶ B ⟶ A}{start : A}{fs : finSeq 0 B} ⊦ finiteSequenceFoldLeft A B 0 f start fs ≐ start❙
// finiteSequenceFoldLeftB : {A : type}{B : type}{n : ℕ}{f : A ⟶ B ⟶ A}{start : A}{fs : finSeq n B} ⊦ finSeqFoldL f start fs ≐ start❙
......
......@@ -15,9 +15,12 @@ theory Set_Operations : fnd:?Logic =
symmetric_difference : set ⟶ set ⟶ set ❘= [A,B] (A \ B) ∪ (B \ A) ❘ # 1 Δ 2 ❙
complement : {a : set } {b : set} ⊦ a ⊆‍ b ⟶ set ❘ = [a,b,h] b \ a ❙
cons : set ⟶ set ⟶ set ❘ = [a,b] upair a a ∪ b ❙
succ : set ⟶ set ❘ = [a] cons a a ❙
theory Set_Properties : fnd:?Logic =
......@@ -38,6 +41,10 @@ theory Set_Properties : fnd:?Logic =
empty : set ⟶ prop ❘ = [A] ¬ ∃ [x] x ∈ A ❙
ball : set ⟶ (set ⟶ prop) ⟶ prop ❘ = [s , p ] ∀ [x] x ∈ s ⇒ p s ❙
bex : set ⟶ (set ⟶ prop) ⟶ prop ❘ = [s , p] ∃[x] x ∈ s ⇒ p s ❙
theory Set_Lemmata : fnd:?Logic =
......
......@@ -3,7 +3,7 @@ namespace http://mathhub.info/MitM/smglom/other_foundations/mmt_tg ❚
import fnd http://mathhub.info/MitM/Foundation ❚
theory PairsTG : fnd:?Logic =
include ?ZF_Base
include http://mathhub.info/MitM/smglom/other_foundations/mmt_tg?Set_Properties
tuple = opair ❙
pair = tuple ❙
......@@ -17,27 +17,24 @@ theory PairsTG : fnd:?Logic =
cartesian_product : set ⟶ set ⟶ set ❘ = [A,B] ⟪ ℘ (℘ (A ∪ B)) | ([x] ∃ [a] ∃ [b] a ∈ A ∧ b ∈ B ∧ x ≐ opair a b ) ⟫ ❘ # 1 × 2 prec 20 ❙
// proof that the only "constructor" of the cartesian product is an opair (i.e. the shape of all elements that are in the cartesian product are opairs)❙
constructor_cartesian_product : ∀ [x] x ∈ cartesian_product ❙
ternary_product : set ⟶ set ⟶ set ⟶ set ❘= [A,B,C] ((A × B ) × C)❙
quarternary_product : set ⟶ set ⟶ set ⟶ set ⟶ set ❘ = [A,B,C,D] (((A × B) × C) × D)❙
lemma_pair_in_cartesian_product : {A , B} {a ,b} ⊦ a ∈ A ⟶ ⊦ b ∈ B ⟶ ⊦ pair ∈ a × b
lemma_pair_in_cartesian_product : {A , B} {a ,b} ⊦ a ∈ A ⟶ ⊦ b ∈ B ⟶ ⊦ pair a b ∈ A × B
projl : {b}{c} {a : set} ⊦ a ∈ b × c ⟶ set
projl_def : {a , b} {A,B} ⊦ projl A B (pair a b ) (lemma_pair_in_cartesian_product A B a b) ≐ a
projl : set ⟶ set ❘ = [s] ⋂ (⋃ s)
red_projl : {a ,b} ⊦ projl (opair a b) ≐ a
projr : {b}{c} {a : set } ⊦ a ∈ set ⟶ set
projr_def : {a,b} ⊦ projr (pair a b ) ≐ b
projr : set ⟶ set ❘= [s] ⋃ (⟪ ⋃ s | ([x] ⋃ s ≠ ⋂ s ⇒ x ∉ (⋂ s)) ⟫)
red_projr : {a ,b} ⊦ projl (opair a b) ≐ b
lefts : set ⟶ set ❙
lefts_def : {s : set} {D : set }{ C : set } {h : ⊦ s ∈ D × C } ⊦ lefts s ≐ ⟪ D | ([x] ∃ [y] opair x y ∈ s ) ⟫ ❙
lefts : set ⟶ set ❘ = [s] ⟪ ⋃ ⋃ s | ([x] ∃[y] tuple x y ∈ s) ⟫ ❙
rights : set ⟶ set ❙
rights_def : {s : set} {D : set }{ C : set } {h : ⊦ s ∈ D × C } ⊦ rights s ≐ ⟪ C | ([x] ∃ [y] opair y x ∈ s ) ⟫ ❙
rights : set ⟶ set ❘ = [s] ⟪ ⋃ ⋃ s | ([x] ∃ [y] tuple y x ∈ s) ⟫ ❙
theory Paris_theorems : fnd:?Logic =
......@@ -47,7 +44,9 @@ theory Paris_theorems : fnd:?Logic =
lemma_pair_id : {a, b, c} ⊦ a ≐ pair b c ⟶ ⊦ pair (projl a) (projr a) ≐ a ❙
lemma_pair_id2 : {a, b, c , d } ⊦ a ∈ (c × d) ⟶ ⊦ b ∈ (c × d ) ⟶ ⊦ projl a ≐ projl b ⟶ ⊦ projr b ≐ projr b ⟶ ⊦ a ≐ b ❙
lemma_pair_id2 : {a, b} ⊦ projl a ≐ projl b ⟶ ⊦ projr b ≐ projr b ⟶ ⊦ a ≐ b ❙
lemma_in_cartesian_is_pair : {a} {b,c} ⊦ a ∈ b × c ⇒ ∃[x] ∃ [y] a ≐ opair x y❙
......@@ -8,16 +8,14 @@ theory Relations : fnd:?Logic =
is_binary_relation_of : set ⟶ set ⟶ set ⟶ prop ❘ = [s,f,t] ∀ [x] (x ∈ s) ⇒ is_opair x ∧ ∃ [a] ∃ [b] (a ∈ f) ∧ (b ∈ t) ∧ projl x ≐ a ∧ projr x ≐ b ❙
relation : set ⟶ set ⟶ set ❘ = [a,b] ℘ (a × b) ❙ // "relation type" ❙
// relation : set ⟶ set ⟶ set ❘ = [a,b] ℘ (a × b) ❙ // "relation type" ❙
domain = lefts ❙
range = rights ❙
field : set ⟶ set ❙
field_def : {r} {D} {C}{h : ⊦ r ∈ relation D C} ⊦ field r ≐ domain r ∪ range r ❙
// field : set ⟶ set ❘ = [s] ❙
converse : set ⟶ set ❙
converse_def : {a : set} {d } {c : set }{h : ⊦ a ∈ relation d c } ⊦ converse a ≐ ⟪ c × d | ([x] opair (projr x )(projl x) ∈ a) ⟫❙
converse : set ⟶ set ❘= [a] ⟪ | ⟫❙
composition : set ⟶ set ⟶ set ❙
// composition_def : {a}{b}{x}{y}{z} {h : ⊦ a ∈ relation x y}{h0 : ⊦ b ∈ relation y z} ⊦ composition a b ≐ ❙
......
......@@ -4,9 +4,17 @@ import fnd http://mathhub.info/MitM/Foundation ❚
import TG http://mathhub.info/MitM/smglom/other_foundations/mmt_tg❚
theory TT : fnd:?Logic =
include TG:?ZF_Base ❙
include TG:?ZFC_Base ❙
typ = set ❙
ttt : typ ❙
typle : set ⟶ set ⟶ type ❙
be : {a : set}{typS : set} context ⟶ ❙
testFn : set ⟶ set ❙
......
......@@ -76,6 +76,12 @@ theory Union : fnd:?Logic =
theory Replacement : fnd:?Logic =
include ?preAxioms ❙
axiom_schema_replacement : {E : set ⟶ set ⟶ prop} ⊦ ∀[x] ∀[y] ∀[z] (E x y ∧ E x z ⇒ y ≐ z) ⇒ ∀[A] ∃[M] ∀[y] (y ∈ M ⇔ ∃ [x] (x ∈ A ∧ E x y)) ❙
lemma_schema_replacement_alt : {E : set ⟶ set ⟶ prop} ⊦ ∀[A] ∃[M] ( ∀[x] ∀[y] ∀[z] (E x y ∧ E x z ⇒ y ≐ z) ⇒ ∀[y] (y ∈ M ⇔ ∃ [x] (x ∈ A ∧ E x y)) ) ❙ // this is valid in classical logic ❙
theorem_schema_replacement_alt_is_unique : {E : set ⟶ set ⟶ prop} ⊦ ∀[A] ∃![M] ( ∀[x] ∀[y] ∀[z] (E x y ∧ E x z ⇒ y ≐ z) ⇒ ∀[y] (y ∈ M ⇔ ∃ [x] (x ∈ A ∧ E x y)) ) ❙
replace : set ⟶ (set ⟶ set ⟶ prop) ⟶ set ❘ = [s,p] ❙
......@@ -123,3 +129,13 @@ theory ZF_Base : fnd:?Logic =
include ?PowerSet ❙
theory Choice : fnd:?Logic =
include ?ZF_Base ❙
axiom_choice : ⊦ ∀ [A] (((∅ ∈ A) ∧ ∀ [X] ∀ [Y] ∀ [Z] (( X ∈ A ∧ Y ∈ A ∧ Z ∈ X ∧ Z ∈ Y ) ⇒ (X ≐ Y))) ⇒ ∃ [B] ∀ [X] (X ∈ A ⇒ ∃![Y](Y ∈ X ∧ Y ∈ B)))❙
theory ZFC_Base : fnd:?Logic =
include ?Choice ❙
\ No newline at end of file
namespace http://mathhub.info/MitM/smglom/other_foundations/mmt_tg ❚
import fnd http://mathhub.info/MitM/Foundation ❚
theory the_descriptor : fnd:?Logic =
include http://mathhub.info/MitM/smglom/other_foundations/mmt_tg?ZFC_Base ❙
the : (set ⟶ prop) ⟶ set ❘ = [p] ⋃ (⟪ | ⟫) ❙
namespace http://mathhub.info/MitM/smglom/other_foundations/mmt_tg ❚
import fnd http://mathhub.info/MitM/Foundation ❚
theory preAxiomsT : fnd:?Logic =
set : type ❙
elem : set ⟶ set ⟶ prop ❘# 1 ∈ 2❙
/T axiom_all_objects_are_sets = "all objects in Tarski Grothendiek set theory are sets"❙
theory ExtensionalityT : fnd:?Logic =
include ?preAxiomsT ❙
include fnd:?NaturalDeduction ❙
axiom_extensionality : ⊦ ∀ [X] ∀ [Y] (∀[x] ( x ∈ X ⇔ x ∈ Y ) ⇒ X ≐ Y ) ❙
axiom_extensionality_alt : {X , Y} ⊦ (∀[x] ( x ∈ X ⇔ x ∈ Y ) ⇒ X ≐ Y ) ❙
axiom_extensionality_alt2 : {X , Y} ⊦ (∀[x] ( x ∈ X ⇔ x ∈ Y ) ⇒ X ≐ Y ) ❘ = [x, y] forallE (forallE axiom_extensionality x) y ❙
theory RegularityT : fnd:?Logic =
include ?preAxiomsT ❙
axiom_regularity : ⊦ ∀ [X] (∃ [z] z ∈ X ⇒ ∃ [Y] (Y ∈ X ∧ ¬ ∃ [x] (x ∈ X ∧ x ∈ Y))) ❙
theory SpecificationT : fnd:?Logic =
include ?preAxiomsT ❙
include fnd:?DescriptionOperator ❙
include fnd:?NaturalDeduction ❙
axiom_schema_specification : {P : set ⟶ prop} ⊦ ∀ [A] ∃ [M] ∀[x] (x ∈ M ⇔ x ∈ A ∧ P x ) ❙ //T also called axiom of separation ❙ // here P is used as an LF parameter because unlike the ❙
theorem_specified_set_is_unique : {P : set ⟶ prop} ⊦ ∀ [A] ∃! [M] ∀[x] (x ∈ M ⇔ x ∈ A ∧ P x ) ❘# theorem_specified_set_is_unique 1 ❙ // using extensionality axiom ❙
set_builder : set ⟶ (set ⟶ prop) ⟶ set ❘ = [s][p] that set ([M] ∀[x] (x ∈ M ⇔ x ∈ s ∧ p x ) ) (forallE (theorem_specified_set_is_unique p) s) ❘# ⟪ 1 | 2 ⟫ prec -1 ❙
theory PairingT : fnd:?Logic =
include ?ExtensionalityT ❙
include fnd:?DescriptionOperator ❙
include fnd:?Subtyping ❙
axiom_pairing : ⊦ ∀ [x] ∀ [y] ∃ [z] (x ∈ z ∧ y ∈ z)❙
theorem_pair_unique : ⊦ ∀[X] ∀ [Y] ∃! [Z] (X ∈ Z ∧ Y ∈ Z) ❙ // by axiom of extensionality❙
theorem_pair_unique_alt : {X: set} {Y :set } ⊦ ∃! [Z] (X ∈ Z ∧ Y ∈ Z) ❘ # theorem_pair_unique_alt 1 2 ❘ = [X,Y] forallE (forallE theorem_pair_unique X) Y ❙ // by axiom of extensionality❙
upair : set ⟶ set ⟶ set ❘ = [A :set][B : set] that set ([Z] (A ∈ Z ∧ B ∈ Z)) (theorem_pair_unique_alt A B) ❙ // unordered pair ❙
singleton : set ⟶ set ❘ = [A : set] upair A A ❙
opair : set ⟶ set ⟶ set ❘ = [a ,b ] upair (singleton a) (upair a b) ❙ // ordered pair ❙
opairT : type ❘= ⟨ s : set | ⊦ ∃ [a] ∃[b] s ≐ opair a b⟩ ❙
opairC : set ⟶ set ⟶ opairT ❘ = [s1,s2] opair s1 s2 ❙
theory UnionT : fnd:?Logic =
include ?PairingT ❙
axiom_union : ⊦ ∀[A] ∃[B] ∀[c] (c ∈ B ⇔ ∃ [D] (c ∈ D ∧ D ∈ A )) ❙
theorem_union_unique : ⊦ ∀ [A] ∃! [B] ∀[c] (c ∈ B ⇔ ∃ [D] (c ∈ D ∧ D ∈ A )) ❙ // again using the extensionality axiom ❙
bigUnion : set ⟶ set ❘ = [S] that set ([B] ∀[c] (c ∈ B ⇔ ∃ [D] (c ∈ D ∧ D ∈ S ))) (forallE theorem_union_unique S) ❘ # ⋃ 1 ❙
binaryUnion : set ⟶ set ⟶ set ❘ = [A , B] ⋃ upair A B ❘ # 1 ∪ 2 ❙
theory ReplacementT : fnd:?Logic =
include ?preAxiomsT ❙
axiom_schema_replacement : {E : set ⟶ set ⟶ prop} ⊦ ∀[x] ∀[y] ∀[z] (E x y ∧ E x z ⇒ y ≐ z) ⇒ ∀[A] ∃[M] ∀[y] (y ∈ M ⇔ ∃ [x] (x ∈ A ∧ E x y)) ❙
theory EmptySetT : fnd:?DescriptionOperator =
include ?preAxiomsT ❙
axiom_empty_set : ⊦ ∃ [X] ∀ [y] ¬ ( y ∈ X)❙
theorem_empty_set_unique : ⊦ ∃! [X] ∀ [y] ¬ (y ∈ X) ❙ // by axiom of extensionality ❙
empty_set : set ❘= that set ([X : set ] ∀ [y] ¬ (y ∈ X)) theorem_empty_set_unique ❘ # ∅ ❙
theory InfinityT : fnd:?Logic =
include ?EmptySetT ❙
include ?UnionT ❙
axiom_infinity : ⊦ ∃ [X] ( ∅ ∈ X ∧ ∀ [y] (y ∈ X ⇒ ( y ∪ singleton y ) ∈ X )) ❙
prop_is_infinite : set ⟶ prop ❘ = [S] ( ∅ ∈ S ∧ ∀ [y] (y ∈ S ⇒ ( y ∪ singleton y ) ∈ S )) ❙
theorem_not_all_infinite_sets_are_equal : ⊦ ∃ [A] ∃ [B] prop_is_infinite A ⇒ prop_is_infinite B ⇒ A ≠ B ❙
theory PowerSetT : fnd:?Logic =
include ?preAxiomsT ❙
include fnd:?DescriptionOperator ❙
include fnd:?NaturalDeduction ❙
is_subset : set ⟶ set ⟶ prop ❘ = [A , B] ∀[x] (x ∈ A ⇒ x ∈ B) ❘ # 1 ⊆‍ 2 ❙
axiom_power_set : ⊦ ∀ [X] ∃ [Y] ∀ [Z] (Z ⊆‍ X ⇒ Z ∈ Y) ❙
theorem_power_set_unique : ⊦ ∀ [X] ∃! [Y] ∀ [Z] (Z ⊆‍ X ⇒ Z ∈ Y) ❙
powerSet : set ⟶ set ❘= [s] that set ([Y] ∀ [Z] (Z ⊆‍ s ⇒ Z ∈ Y) ) (forallE theorem_power_set_unique s) ❘ # ℘ 1 ❙
theory ZF_BaseT : fnd:?Logic =
include ?RegularityT ❙
include ?SpecificationT ❙
include ?ReplacementT ❙
include ?InfinityT ❙
include ?PowerSetT ❙
theory ChoiceT : fnd:?Logic =
include ?ZF_BaseT ❙
axiom_choice : ⊦ ∀ [A] (((∅ ∈ A) ∧ ∀ [X] ∀ [Y] ∀ [Z] (( X ∈ A ∧ Y ∈ A ∧ Z ∈ X ∧ Z ∈ Y ) ⇒ (X ≐ Y))) ⇒ ∃ [B] ∀ [X] (X ∈ A ⇒ ∃![Y](Y ∈ X ∧ Y ∈ B)))❙
theory ZFC_BaseT : fnd:?Logic =
include ?ChoiceT ❙
\ No newline at end of file