Commit b8a58821 by Sven Wille

### relations

parent 1ebd8412
 ... ... @@ -5,24 +5,45 @@ import fnd http://mathhub.info/MitM/Foundation ❚ theory Relations : fnd:?Logic = include ?PairsTG ❙ 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" ❙ is_relation = [r] ∀ [z] z ∈ r ⇒ ∃ [x] ∃ [y] z ≐ opair x y ❙ is_function = [r] ∀ [x] ∀ [y] opair x y ∈ r ⇒ ∀ [z] opair x z ∈ r ⇒ y ≐ z ❙ domain = lefts ❙ range = rights ❙ // field : set ⟶ set ❘ = [s] ❙ image = [r] [A] ⟪ range r | ([y] ∃ [x] x ∈ A ⇒ opair x y ∈ r) ⟫ ❙ field = [r] domain r ∪ range r ❙ converseCond : set ⟶ set ⟶ prop ❘ = [a,b] ∃ [x] ∃ [y] a ≐ opair x y ∧ b ≐ opair y x ❙ converseCondRightUnique : ⊦ propIsRightUnique converseCond ❙ converse : set ⟶ set ❘= [a] ⟪ | ⟫❙ converse : set ⟶ set ❘= [a] replace a converseCond converseCondRightUnique ❙ inverse_image = [r] image (converse r)❙ restrict = [r][A] ⟪ r | ([z] ∃ [x] x ∈ A ⇒ ∃ [y] z ≐ opair x y) ⟫ ❙ SigmaRightUnique : {x : set} ⊦ propIsRightUnique ([y][z] z ≐ opair x y) ❘ # SigmaRightUnique 1 ❙ SigmaRightUnique2 : {B : set ⟶ set } ⊦ propIsRightUnique ([x][zz] zz ≐ replace (B x) ([y][z] z ≐ opair x y) (SigmaRightUnique x) ) ❘# SigmaRightUnique2 ❙ Sigma = [A][B] ⋃ replace A ([x][zz] zz ≐ replace (B x) ([y][z] z ≐ opair x y) (SigmaRightUnique x)) (SigmaRightUnique2 B) ❙ composition : set ⟶ set ⟶ set ❙ // composition_def : {a}{b}{x}{y}{z} {h : ⊦ a ∈ relation x y}{h0 : ⊦ b ∈ relation y z} ⊦ composition a b ≐ ❙ ❚ theory Abstractions : fnd:?Logic = // include ?Relatioins ❙ // Lambda = [A,b] ❙ ❚ theory Relations_theorems : fnd:?Logic = include ?Relations ❙ // include ?Relations ❙ ❚ \ No newline at end of file
 ... ... @@ -40,6 +40,7 @@ theory Specification : fnd:?Logic = 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 ❙ // the usage of the russelle iota is a conservative extension to the standard fol-logic , hence there is no problem in using it to formalize zfc ❙ 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 ❙ ❚ ... ... @@ -83,7 +84,7 @@ theory Replacement : fnd:?Logic = theorem_schema_replacement_unique : {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))) ❘ # theorem_schema_replacement_unique 1 ❙ replacePropProp : (set ⟶ set ⟶ prop) ⟶ prop ❘ = [E] (∀ [x] ∀[y] ∀[z] (E x y ∧ E x z ⇒ y ≐ z)) ❘ # replacePropProp 1❙ propIsRightUnique : (set ⟶ set ⟶ prop) ⟶ prop ❘ = [E] (∀ [x] ∀[y] ∀[z] (E x y ∧ E x z ⇒ y ≐ z)) ❘ # propIsRightUnique 1❙ replace : set ⟶ {E : set ⟶ set ⟶ prop} ⊦ (∀ [x] ∀[y] ∀[z] (E x y ∧ E x z ⇒ y ≐ z)) ⟶ set ❘ = [s,E,h] that set ([M] ∀[y] (y ∈ M ⇔ ∃ [x] (x ∈ s ∧ E x y))) (forallE (impE h (theorem_schema_replacement_unique E) ) s) ❙ ... ...
 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:?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 ❙ // adding the set builder and the corresponding axioms are a conservative extension to the zfc langauge (an alternative would be to use russels iota "ι") ❙ // using the axiom of specification withould "set builder" would make theorems/proofs/etc. very tidious ❙ set_builder : set ⟶ (set ⟶ prop) ⟶ set ❘ # ⟪ 1 | 2 ⟫ prec -1 ❙ axiom_that_set_builder : {P : set ⟶ prop} ⊦ ∀ [A] ∀[x] (x ∈ set_builder A P ⇔ x ∈ A ∧ P x)❙ theorem_that_set_builder2 : {P : set ⟶ prop} ⊦ ∀ [A] ∀ [M] ( set_builder A P ≐ M ⇔ (∀ [x] x ∈ M ⇔ x ∈ A ∧ P x)) ❙ ❚ 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 ❘# ⋃ 1 ❙ axiom_that_bigUnion : ⊦ ∀ [A] ∀[c] (c ∈ ⋃ A ⇔ ∃ [D] (c ∈ D ∧ D ∈ A )) ❙ theorem_that_bigUnion2 : ⊦ ∀ [A] ∀ [B] ⋃ A ≐ B ⇔ ∀[c] (c ∈ B ⇔ ∃ [D] (c ∈ D ∧ D ∈ A )) ❙ ❚ 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 ❘ # ∅ ❙ axiom_that_empty_set : ⊦ ∀ [y] ¬ ( y ∈ ∅) ❙ theorem_that_empty_set2 : ⊦ ∀[X] (∀ [y] ¬ (y ∈ X)) ⇔ X ≐ ∅ ❙ // by axiom of extensionality ❙ ❚ theory the_descriptor : fnd:?Logic = include ?EmptySet ❙ include ? ❚ 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) ❙ // unordered pair ❙ singleton : set ⟶ set ❘ = [A : set] upair A A ❙ opair : set ⟶ set ⟶ set ❘ = [a ,b ] upair (singleton a) (upair a b) ❙ // ordered pair ❙ ❚ theory Replacement : fnd:?Logic = include ?preAxioms ❙ include fnd:?DescriptionOperator ❙ include fnd:?NaturalDeduction ❙ 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)) ❙ theorem_schema_replacement_unique : {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))) ❘ # theorem_schema_replacement_unique 1 ❙ replacePropProp : (set ⟶ set ⟶ prop) ⟶ prop ❘ = [E] (∀ [x] ∀[y] ∀[z] (E x y ∧ E x z ⇒ y ≐ z)) ❘ # replacePropProp 1❙ replace : set ⟶ {E : set ⟶ set ⟶ prop} ⊦ (∀ [x] ∀[y] ∀[z] (E x y ∧ E x z ⇒ y ≐ z)) ⟶ set ❘ = [s,E,h] that set ([M] ∀[y] (y ∈ M ⇔ ∃ [x] (x ∈ s ∧ E x y))) (forallE (impE h (theorem_schema_replacement_unique E) ) s) ❙ ❚ // 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 ❘ # ℘ 1 ❙ that_powerSet : ⊦ ∀ [X] ∀[Z] (Z ⊆‍ X ⇔ Z ∈ ℘ X) ❙ that_powerSet2 : ⊦ ∀ [P] ∀ [X] (∀[Z] (Z ⊆‍ X ⇔ Z ∈ P)) ⇔ P ≐ ℘ X ❙ // 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 ❙ ❚ 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
 ... ... @@ -7,7 +7,17 @@ import fnd http://mathhub.info/MitM/Foundation ❚ theory the_descriptor : fnd:?Logic = include http://mathhub.info/MitM/smglom/other_foundations/mmt_tg?ZFC_Base ❙ thePropInj : {p : set ⟶ prop} {h : ⊦ ∃![y] p y} ⊦ (replacePropProp ([x : set ] [z : set ] p z )) ❘ # thePropInj 1 2 ❙ thePropRight : {p : set ⟶ prop} {h : ⊦ ∃![y] p y} ⊦ (propIsRightUnique ([x : set ] [z : set ] p z )) ❘ # thePropRight 1 2 ❙ the : {p :set ⟶ prop} ⊦ (∃! [y] p y) ⟶ set ❘ = [p,h] ⋃ (replace (singleton ∅) ([x] [y] p y) (thePropInj p h))❙ the : {p :set ⟶ prop} ⊦ (∃! [y] p y) ⟶ set ❘ = [p,h] ⋃ (replace (singleton ∅) ([x] [y] p y) (thePropRight p h))❙ ❚ theory ifThenElseZFC : fnd:?Logic = include http://mathhub.info/MitM/smglom/other_foundations/mmt_tg?ZFC_Base ❙ include ?the_descriptor ❙ ifThenElseUnique: ⊦ ∀ [c : prop ] ∀ [a] ∀ [b] ∃![y : set ] (y ≐ a ∧ c) ∨ (y ≐ b ∧ ¬ c) ❘# ifThenElseUnique ❙ ifdef : prop ⟶ set ⟶ set ⟶ set ❘ = [c , a , b] the ([z] (z ≐ a ∧ c) ∨ (z ≐ b ∧ ¬ c)) (forallE (forallE (forallE ifThenElseUnique c) a) b)❙ ❚ \ No newline at end of file
 namespace http://mathhub.info/MitM/smglom/other_foundations/mmt_tg ❚ import fnd http://mathhub.info/MitM/Foundation ❚ // this version of the replacement scheme uses an unary lf-function instead of a binary predicate to avoid the proof that the binary predicate is "right unique" ❚ theory ReplacementFunction : fnd:?Logic = include ?preAxioms ❙ include fnd:?DescriptionOperator ❙ include fnd:?NaturalDeduction ❙ axiom_schema_replacementFn : {E : set ⟶ set} ⊦ ∀[A] ∃[M] ∀[y] (y ∈ M ⇔ ∃ [x] (x ∈ A ∧ E x ≐ y)) ❙ theorem_schema_replacementFn_unique : {E : set ⟶ set} ⊦ (∀[A] ∃![M] ∀[y] (y ∈ M ⇔ ∃ [x] (x ∈ A ∧ E x ≐ y))) ❘ # theorem_schema_replacement_unique 1 ❙ replaceFn : set ⟶ (set ⟶ set) ⟶ set ❘ = [s,E] that set ([M] ∀[y] (y ∈ M ⇔ ∃ [x] (x ∈ s ∧ E x ≐ y))) (forallE (theorem_schema_replacementFn_unique E) s) ❙ ❚
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!