...

Commits (2)
 namespace http://mathhub.info/MitM/Foundation/sets ❚ import fnd http://mathhub.info/MitM/Foundation ❚
 namespace http://mathhub.info/MitM/Foundation/sets ❚ 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 ❙ axiom_schema_specification : {P : set ⟶ prop} ⊦ ∀ [A] ∃ [M] ∀[x] (x ∈ M ⇔ x ∈ A ∧ P x ) ❙ //T also called axiom of separation ❙ ❚ theory Pairing : fnd:?Logic = include ?preAxioms ❙ axiom_pairing : ⊦ ∀ [x] ∀ [y] ∃ [z] (x ∈ z ∧ y ∈ z)❙ ❚ theory Union : fnd:?Logic = include ?preAxioms ❙ axiom_union : ⊦ ∀[A] ∃[B] ∀[c] (c ∈ B ⇔ ∃ [D] (c ∈ D ∧ D ∈ A )) ❙ ❚ 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 Empty : 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 ?Empty ❙ axiom_infinity : ⊦ ∃ [I] (∅ ∈ I ∧ ∀ [x] ∈ I ()) ❙ ❚ theory TarskisAxiom : fnd:?Logic = ❚ \ No newline at end of file