...
 
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