# Creative Commons Attribution-Share Alike 3.0 Unported (http://creativecommons.org/licenses/by-sa/3.0/) # {{modules # | parameters = [[Interface:Classical propositional calculus|Classical propositional calculus]], [[Interface:First-order logic with quantifiability|first-order logic]] # | importedby = [[Relations]] # | exportedby = [[Basic operations of Zermelo-Fraenkel set theory]] # }} # # This page covers some of the simplest operations of set theory including the empty set, singletons, unordered pairs, power set, and unions. # # == Variables, objects (classes), and membership == # # We build on [[Interface:Classical propositional calculus|propositional logic]] and [[Interface:First-order logic with quantifiability|first-order logic]] (including equality): # param (CLASSICAL Classical_propositional_calculus.ghi () "") param (FIRSTORDER First-order_logic_with_quantifiability.ghi (CLASSICAL) "") # # First-order logic provides us with two kinds: `variable` is a variable, which represents a set and can be quantified over, and `object` is an expression which represents a set. For example, a variable might be `x`, `y`, or `z`, but an object could be the singleton `{ x }`, the unordered pair `{ x, y }`, the ordered pair `〈 x, y 〉`, etc. To some extent the concepts of variable and object correspond to set and class in some theories (like metamath's set.mm), but one key difference is that we have no [[w:proper class|proper classes]] thanks to the [[Interface:Axiom of quantifiability|axiom of quantifiability]]. # var (object x y z w) tvar (object A B C A0 A1 B0 B1) tvar (formula φ ψ φx φy antecedent) # # We can test whether one set is an element of another, and define an abbreviation for the negated version. term (formula (∈ A B)) # # Here are two ways of combining membership with a substitution: stmt (MembershipForAll ((A x) (B x)) () (↔ (∈ A B) (∀ x (→ (= x A) (∈ x B))))) stmt (MembershipThereExists ((A x) (B x)) () (↔ (∈ A B) (∃ x (∧ (= x A) (∈ x B))))) # # == Empty set == # We assert the existence of the empty set, a set with no elements. term (object (∅)) stmt (EmptySet () () (¬ (∈ A (∅)))) # # == Singleton == # Given a set, we can form a set `{ s }` which has only it as an element.[http://us.metamath.org/mpeuni/elsncg.html elsncg], metamath's set.mm, accessed August 7, 2010 term (object (singleton A)) stmt (Singleton () () (↔ (∈ A (singleton B)) (= A B))) # # A set is an element of its singleton: `A ∈ {A}`.[http://us.metamath.org/mpeuni/snid.html snid], metamath's set.mm, accessed August 5, 2010 stmt (SingletonMembership () () (∈ A (singleton A))) # # == Unordered pair == # Given two sets, we can form a unordered pair `{ s, t }` which has only those sets as elements. term (object (unorderedPair A B)) stmt (UnorderedPair () () (↔ (∈ B (unorderedPair A0 A1)) (∨ (= B A0) (= B A1)))) # # An unordered pair contains each of its members: `A ∈ {A, B}`. stmt (UnorderedPairLeftMembership () () (∈ A (unorderedPair A B))) stmt (UnorderedPairRightMembership () () (∈ B (unorderedPair A B))) # # Unordered pairs are unordered: `{A, B} = {B, A}`. stmt (UnorderedPairCommutativity () () (= (unorderedPair A B) (unorderedPair B A))) # # Unordered pair equality can imply equality of members: `{A, C} = {B, C} → A = B`,[http://us.metamath.org/mpeuni/preqr1.html preqr1], metamath's set.mm, accessed August 4, 2010 and likewise if the unordered pairs are commuted. # stmt (UnorderedPairFirstMembersEqual () () (→ (= (unorderedPair A C) (unorderedPair B C)) (= A B))) stmt (UnorderedPairSecondMembersEqual () () (→ (= (unorderedPair C A) (unorderedPair C B)) (= A B))) # # A singleton is equal to an unordered pair with the same element listed twice. stmt (SingletonUnorderedPair () () (= (singleton A) (unorderedPair A A))) # # == Subset == # The subset relationship is equivalent to various statements involving membership, unions, intersections, and set differences.[http://us.metamath.org/mpeuni/df-ss.html df-ss] term (formula (⊆ A B)) stmt (Subset ((A x) (B x)) () (↔ (⊆ A B) (∀ x (→ (∈ x A) (∈ x B))))) stmt (SubsetMembership () () (→ (⊆ A B) (→ (∈ C A) (∈ C B)))) stmt (SingletonSubset () () (↔ (∈ A B) (⊆ (singleton A) B))) stmt (UnorderedPairSubset () () (↔ (∧ (∈ A C) (∈ B C)) (⊆ (unorderedPair A B) C))) # # === Partial order === # The subset relationship has the three properties of a [[w:Partially ordered set|partial order]]. That is, it is reflexive, antisymmetric, and transitive. # stmt (SubsetReflexivity () () (⊆ A A)) stmt (SubsetAntisymmetry () () (→ (∧ (⊆ A B) (⊆ B A)) (= A B))) stmt (SubsetTransitivity () () (→ (∧ (⊆ A B) (⊆ B C)) (⊆ A C))) # # == Union == # The union of a set has as its elements everything which is an element of some set in the given set. term (object (⋃ A)) stmt (Union ((A x) (B x)) () (↔ (∈ B (⋃ A)) (∃ x (∧ (∈ B x) (∈ x A))))) # # The union of two sets is just a special case of the union of a set. term (object (∪ A B)) stmt (BinaryUnionAsUnion () () (= (∪ A B) (⋃ (unorderedPair A B)))) stmt (BinaryUnion () () (↔ (∈ A (∪ B C)) (∨ (∈ A B) (∈ A C)))) stmt (MembershipUnionRightIntroduction () () (→ (∈ A B) (∈ A (∪ B C)))) stmt (MembershipUnionLeftIntroduction () () (→ (∈ A C) (∈ A (∪ B C)))) stmt (UnionIdempotence () () (= (∪ A A) A)) stmt (UnionSingleton () () (= (⋃ (singleton A)) A)) # # An unordered pair is the union of singletons for each of its elements. stmt (UnorderedPairSingleton () () (= (unorderedPair A B) (∪ (singleton A) (singleton B)))) # # === Subsets and unions === stmt (SubsetUnion () () (→ (∧ (⊆ A B) (∈ B C)) (⊆ A (⋃ C)))) stmt (MembershipSubsetUnion () () (→ (∈ A B) (⊆ A (⋃ B)))) stmt (SubsetUnionRightIntroduction () () (→ (⊆ A B) (⊆ A (∪ B C)))) # # == Power set == # The power set of a set has as its elements all of the subsets of the given set. term (object (power A)) stmt (PowerSet () () (↔ (∈ B (power A)) (⊆ B A))) # # == Separation == # We define `{x ∈ A | φ}`, the set of all elements in `A` which also satisfy `φ`. Although we write `{x ∈ A | φ}` informally, for JHilbert it needs to be `(separate x A φ)`. term (object (separate x A φ) (x A)) stmt (Separation () () (↔ (∈ C (separate x A φ)) (∧ (∈ C A) (subst C x φ)))) stmt (FormulaBound ((A z) (B z)) ((→ φ (∈ z A))) (↔ (∈ B (separate z A φ)) (subst B z φ))) # # The term `{x ∈ A | φ}` is like a quantifier in the sense that it binds `x`, and we can change the variable in a similar manner. stmt (ChangeVariableSeparation ((φx y) (φy x)) ((→ (= x y) (↔ φx φy))) (= (separate x A φx) (separate y A φy))) # # == Builders == # Equals can be substituted for equals, in the context of set operations. # stmt (MembershipBuilderLL () () (→ (= B0 B1) (↔ (∈ A B0) (∈ A B1)))) stmt (MembershipBuilderRR () () (→ (= A0 A1) (↔ (∈ A0 B) (∈ A1 B)))) stmt (buildMembershipLL () ((= B0 B1)) (↔ (∈ A B0) (∈ A B1))) stmt (buildMembershipRR () ((= A0 A1)) (↔ (∈ A0 B) (∈ A1 B))) stmt (buildMembershipLLInConsequent () ((→ antecedent (= B0 B1))) (→ antecedent (↔ (∈ A B0) (∈ A B1)))) stmt (buildMembershipRRInConsequent () ((→ antecedent (= A0 A1))) (→ antecedent (↔ (∈ A0 B) (∈ A1 B)))) stmt (SingletonBuilder () () (→ (= A B) (= (singleton A) (singleton B)))) stmt (UnorderedPairBuilder () () (→ (∧ (= A0 B0) (= A1 B1)) (= (unorderedPair A0 A1) (unorderedPair B0 B1)))) stmt (SeparationBuilder () () (→ (∧ (= A B) (∀ x (↔ φ ψ))) (= (separate x A φ) (separate x B ψ)))) stmt (buildSeparation () ((↔ φ ψ)) (= (separate x A φ) (separate x A ψ))) stmt (UnionBuilder () () (→ (= A B) (= (⋃ A) (⋃ B)))) stmt (buildUnion () ((= A B)) (= (⋃ A) (⋃ B))) stmt (SubsetBuilderLL () () (→ (= B0 B1) (↔ (⊆ A B0) (⊆ A B1)))) stmt (SubsetBuilderRR () () (→ (= A0 A1) (↔ (⊆ A0 B) (⊆ A1 B)))) stmt (buildSubsetLL () ((= B0 B1)) (↔ (⊆ A B0) (⊆ A B1))) stmt (buildSubsetRR () ((= A0 A1)) (↔ (⊆ A0 B) (⊆ A1 B))) # # == Extensionality == # Sets with the same elements are equal. stmt (Extensionality ((A z) (B z)) () (→ (∀ z (↔ (∈ z A) (∈ z B))) (= A B))) stmt (applyExtensionality ((A x) (B x)) ((↔ (∈ x A) (∈ x B))) (= A B)) # # == References == # # # [[Category:Other classical set theory|{{PAGENAME}}]]