Commit 09777e98 by Sven Wille

### tarski grothendieck

parent 0a31244f
 namespace http://mathhub.info/MitM/smglom/other_foundations/mmt_tg ❚ import fnd http://mathhub.info/MitM/Foundation ❚ theory Set_Operations : fnd:?Logic = include http://mathhub.info/MitM/smglom/other_foundations/mmt_tg?ZF_Base ❙ bigintersection : set ⟶ set ❘ = [S] ⟪ (⋃ S) | ([x] ∀ [Z] (Z ∈ S ⇒ x ∈ Z)) ⟫ ❘ # ⋂ 1 ❙ binaryIntersection : set ⟶ set ⟶ set ❘ = [A , B] ⋂ upair A B ❘ # 1 ∩ 2 prec 10 ❙ set_complement : set ⟶ set ⟶ set ❘= [A,B] ⟪ A | ([x] ¬ (x ∈ B)) ⟫ ❘# 1 \ 2 ❙ symmetric_difference : set ⟶ set ⟶ set ❘= [A,B] (A \ B) ∪ (B \ A) ❘ # 1 Δ 2 ❙ ❚ theory Set_Properties : fnd:?Logic = include http://mathhub.info/MitM/smglom/other_foundations/mmt_tg?ZF_Base ❙ include ?Set_Operations ❙ disjoint : set ⟶ set ⟶ prop ❘ = [A,B] A ∩ B ≐ ∅ ❙ joint : set ⟶ set ⟶ prop ❘ = [A,B] A ∩ B ≠ ∅ ❙ proper_subset : set ⟶ set ⟶ prop ❘ = [A , B] A ⊆‍ B ∧ A ≠ B ❘ # 1 ⊊ 2 ❙ set_iff : set ⟶ set ⟶ prop ❘ = [A , B] (A ≐ B) ⇔ (A ⊆‍ B ∧ B ⊆‍ A) ❙ not_member : set ⟶ set ⟶ prop ❘ = [A,B] ¬ (A ∈ B) ❘ # 1 ∉ 2 ❙ nonempty : set ⟶ prop ❘ = [A] ∃ [x] x ∈ A ❙ empty : set ⟶ prop ❘ = [A] ¬ ∃ [x] x ∈ A ❙ ❚ theory Set_Lemmata : fnd:?Logic = include ?Set_Properties ❙ lemma_set_symdifference_iff : {A , B , x } ⊦ x ∈ (A Δ B) ⇔ (x ∈ A ∧ x ∉ B) ∨ (x ∈ B ∧ x ∉ A) ❙ lemma_set_symdifference1 : {X,Y,Z, x } ⊦ x ∉ X ⇔ (x ∈ Y ⇔ x ∈ Z) ⟶ ⊦ X ≐ Y Δ Z ❙ lemma_singleton_non_empty : {A : set } ⊦ (singleton A ≠ ∅) ❙ lemma_union_non_empty1 : {A,B} ⊦ nonempty A ⟶ ⊦ nonempty (A ∪ B) ❙ lemma_union_non_empty2 : {A,B} ⊦ nonempty A ⟶ ⊦ nonempty (B ∪ A) ❙ corollary_empty_set_is_empty : ⊦ empty ∅ ❙ ❚
 namespace http://mathhub.info/MitM/smglom/other_foundations/mmt_tg ❚ import fnd http://mathhub.info/MitM/Foundation ❚ theory preAxioms : fnd:?Logic = include fnd:?InformalProofs ❙ set : type ❙ elem : set ⟶ set ⟶ prop ❘# 1 ∈ 2❙ /T axiom_all_objects_are_sets = "all objects in Tarski Grothendiek set theory are sets"❙ ❚ theory Extensionality : fnd:?Logic = include ?preAxioms ❙ 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 Regularity : fnd:?Logic = include ?preAxioms ❙ axiom_regularity : ⊦ ∀ [X] (∃ [z] z ∈ X ⇒ ∃ [Y] (Y ∈ X ∧ ¬ ∃ [x] (x ∈ X ∧ x ∈ Y))) ❙ ❚ theory Specification : fnd:?Logic = include ?preAxioms ❙ 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 Pairing : fnd:?Logic = include ?Extensionality ❙ include fnd:?DescriptionOperator ❙ 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) ❙ singleton : set ⟶ set ❘ = [A : set] upair A A ❙ ❚ theory Union : fnd:?Logic = include ?Pairing ❙ 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 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)) ❙ ❚ theory EmptySet : fnd:?DescriptionOperator = include ?preAxioms ❙ 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 Infinity : fnd:?Logic = include ?EmptySet ❙ include ?Union ❙ 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 PowerSet : fnd:?Logic = include ?preAxioms ❙ 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_Base : fnd:?Logic = include ?Regularity ❙ include ?Specification ❙ include ?Replacement ❙ include ?Infinity ❙ include ?PowerSet ❙ ❚
 Xboole_0 : are_c=-comparable XBOOLE_0:5 \ No newline at end of file
 namespace http://mathhub.info/MitM/smglom/other_foundations/mmt_tg ❚ import sets http://mathhub.info/MitM/Foundation/sets ❚ import fnd http://mathhub.info/MitM/Foundation ❚ theory Intersection : fnd:?Logic = ❚
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!