...

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