...

Commits (3)

 ... ... @@ -272,6 +272,8 @@ theory OptionType : ur:?PLF = None : {A : 𝒰 100} Option A ❘ # None ❙ None_is_not_Defined : {A : 𝒰 100} ⊦ isDefined (None A) ≐ false ❙ Not_None_is_Defined : {A, a : Option A} ⊦ (a ≠ None A) ⟶ ⊦ isDefined a ❙ Some : {A : 𝒰 100} A ⟶ Option A ❙ ❚ theory DescriptionOperator : ur:?PLF = ... ...
 ... ... @@ -33,22 +33,41 @@ theory Regularity : fnd:?Logic = 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 ❙ 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 } ❙ ❚ theory Pairing : fnd:?Logic = include ?preAxioms ❙ 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) ❘ # { 1 , 2 } prec -10 ❙ singleton : set ⟶ set ❘ = [A : set] { A , A } ❘ # { 1 } prec -9❙ ❚ theory Union : fnd:?Logic = include ?preAxioms ❙ 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] ⋃ { A , B } ❘ # 1 ∪ 2 ❙ ❚ theory Replacement : fnd:?Logic = ... ... @@ -57,7 +76,7 @@ theory Replacement : fnd:?Logic = ❚ theory Empty : fnd:?DescriptionOperator = theory EmptySet : fnd:?DescriptionOperator = include ?preAxioms ❙ axiom_empty_set : ⊦ ∃ [X] ∀ [y] ¬ ( y ∈ X)❙ ... ... @@ -68,9 +87,56 @@ theory Empty : fnd:?DescriptionOperator = ❚ theory Infinity : fnd:?Logic = include ?Empty ❙ axiom_infinity : ⊦ ∃ [I] (∅ ∈ I ∧ ∀ [x] ∈ I ()) ❙ include ?EmptySet ❙ include ?Union ❙ axiom_infinity : ⊦ ∃ [X] ( ∅ ∈ X ∧ ∀ [y] (y ∈ X ⇒ ( y ∪ {y}) ∈ X )) ❙ prop_is_infinite : set ⟶ prop ❘ = [S] ( ∅ ∈ S ∧ ∀ [y] (y ∈ S ⇒ ( y ∪ {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) ❙ ❚ theory ZF : fnd:?Logic = include ?Regularity ❙ include ?Specification ❙ include ?Replacement ❙ include ?Infinity ❙ include ?PowerSet ❙ ❚ theory AxiomOfChoice : fnd:?Logic = ❚ theory ZFC : fnd:?Logic = include ?ZF ❙ include ?AxiomOfChoice ❙ ❚ theory TarskisAxiom : fnd:?Logic = ❚ theory Tarski : fnd:?Logic = ❚ theory TarskiGrothendieck : fnd:?Logic = include ?Regularity ❙ // include ❙ ❚ \ No newline at end of file