Interface:Set theory

From Wikiproofs
Jump to: navigation, search
Module usage
Classical propositional calculus, first-order logic
Imported by
Interface:Complex number axioms and others
Exported by
Relations 2

This page will eventually cover as much of set theory as is generally used in the bulk of mathematics: empty set, singletons, unordered and ordered pairs, relations, functions, subset, union, intersection, etc.

We build on propositional logic and first-order logic (including equality):

param (CLASSICAL Interface:Classical_propositional_calculus () ())
param (FIRSTORDER Interface:First-order_logic_with_quantifiability (CLASSICAL) ())

Variables (sets) and objects (classes)[edit]

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, but one key difference is that we have no proper classes thanks to the axiom of quantifiability.

var (variable a b x y z w)
var (object A B C A0 A1 B0 B1)
var (formula φ ψ φx φy antecedent)

Set membership[edit]

We can test whether one set is an element of another, and define an abbreviation for the negated version.

term (formula ( object object))
def (( A B) (¬ (A  B)))

Empty set[edit]

We assert the existence of the empty set, a set with no elements.

term (object ())
stmt (EmptySet () () (A  ()))


Given a set, we can form a set { s } which has only it as an element.[1]

term (object (singleton object))
stmt (Singleton () () ((A  (singleton B))  (A = B)))

A set is an element of its singleton: A ∈ {A}.[2]

stmt (SingletonMembership () () (A  (singleton A)))

Unordered pair[edit]

Given two sets, we can form a unordered pair { s, t } which has only those sets as elements.

term (object (unorderedPair object object))
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,[3] 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)))

Ordered pair[edit]

An ordered pair has a first element and a second element, and two ordered pairs are equal if and only if their first elements are equal and their second elements are equal.

term (object (orderedPair object object))
stmt (OrderedPairTheorem () () (((orderedPair A0 B0) = (orderedPair A1 B1))  ((A0 = A1)  (B0 = B1))))

We can extract the first or second element of an ordered pair.

term (object (1st object))
stmt (First () () ((1st (orderedPair A B)) = A))
term (object (2nd object))
stmt (Second () () ((2nd (orderedPair A B)) = B))


A relation is a set of ordered pairs. We define relation A as a formula meaning "A is a relation". We customarily use the letters R, S, and T for relations.

term (formula (relation object))
stmt (Relation ((x y z A)) ()
  ((relation A)  ( z (((value z)  A)  ( x ( y ((value z) = (orderedPair (value x) (value y)))))))))

var (object R S T)

The Cartesian product of two sets is the set of all ordered pairs consisting of one set from the first given set and one set from the second given set.[4]

term (object (× object object))
stmt (MembershipCartesianProduct
  ((a b A) (a b B) (a b C)) ()
  ((C  (A × B)) 
    ( a ( b ((C = (orderedPair (value a) (value b)))
       (((value a)  A)  ((value b)  B)))))))
stmt (OrderedPairCartesianProduct () ()
  (((orderedPair A0 B0)  (A × B))  ((A0  A)  (B0  B))))
stmt (FirstSecondCartesianProduct () ()
  ((A  (B × C))  (((1st A)  B)  ((2nd A)  C))))

The domain of a relation is a set consisting of all of the first elements of the ordered pairs in the relation. Our definition, and the theorems that follow, do not require R to be a relation, but they aren't especially interesting if it is not.

term (object (domain object))
stmt (Domain ((y B) (y R)) ()
  ((B  (domain R))  ( y ((orderedPair B (value y))  R))))
stmt (DomainSingletonRelation () ()
  ((domain (singleton (orderedPair A B))) = (singleton A)))

The range is a set containing exactly the values which the second members of the ordered pairs in the relation can take on (as opposed to the other common definition, which is a set which is a superset of what we call the range).

term (object (range object))
stmt (Range ((x B) (x R)) ()
  ((B  (range R))  ( x ((orderedPair (value x) B)  R))))
stmt (RangeSingletonRelation () ()
  ((range (singleton (orderedPair A B))) = (singleton B)))


The subset relationship is equivalent to various statements involving membership, unions, intersections, and set differences.[5]

term (formula ( object object))
stmt (Subset ((x A) (x B)) ()
  ((A  B)  ( x (((value x)  A)  ((value 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[edit]

The subset relationship has the three properties of a 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)))


The union of a set has as its elements everything which is an element of some set in the given set.

term (object ( object))
stmt (Union ((x A) (x B)) () ((B  ( A))  ( x ((B  (value x))  ((value x)  A)))))

The union of two sets is just a special case of the union of a set.

def (( 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[edit]

stmt (SubsetUnion () () (((A  B)  (B  C))  (A  ( C))))
stmt (MembershipSubsetUnion () () ((A  B)  (A  ( B))))

stmt (SubsetUnionRightIntroduction () ()
  ((A  B)  (A  (B  C))))

Power set[edit]

The power set of a set has as its elements all of the subsets of the given set.

term (object (power object))
stmt (PowerSet () () ((B  (power A))  (B  A)))


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 variable object formula))
stmt (Separation ((x A)) ()
  ((C  (separate x A φ))  ((C  A)  (subst C x φ))))

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
  ((y φx) (x φy) (x y A))
  ((((value x) = (value y))  (φx  φy)))
  ((separate x A φx) = (separate y A φy)))


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 (OrderedPairBuilder () () (((A0 = A1)  (B0 = B1))  ((orderedPair A0 B0) = (orderedPair A1 B1))))
stmt (OrderedPairBuilderLL () () ((B0 = B1)  ((orderedPair A B0) = (orderedPair A B1))))
stmt (buildOrderedPairLLInConsequent ()
  ((antecedent  (B0 = B1)))
  (antecedent  ((orderedPair A B0) = (orderedPair A B1))))
stmt (OrderedPairBuilderRR () () ((A0 = A1)  ((orderedPair A0 B) = (orderedPair A1 B))))
stmt (buildOrderedPairRRInConsequent ()
  ((antecedent  (A0 = A1)))
  (antecedent  ((orderedPair A0 B) = (orderedPair A1 B))))

stmt (buildSeparation ((x A)) ((φ  ψ)) ((separate x A φ) = (separate x A ψ)))

stmt (UnionBuilder () () ((A = B)  (( A) = ( B))))
stmt (buildUnion () ((A = B)) (( A) = ( B)))

stmt (FirstBuilder () () ((A = B)  ((1st A) = (1st B))))
stmt (SecondBuilder () () ((A = B)  ((2nd A) = (2nd B))))
stmt (DomainBuilder () () ((R = S)  ((domain R) = (domain S))))
stmt (RangeBuilder () () ((R = S)  ((range R) = (range S))))


Sets with the same elements are equal.

stmt (Extensionality ((A z) (B z)) () (( z (((value z)  A)  ((value z)  B)))  (A = B)))
stmt (applyExtensionality ((x A) (x B)) ((((value x)  A)  ((value x)  B))) (A = B))

Here's a variant with explicit freeness hypotheses rather than distinct variable constraints.

stmt (ExtensionalityNotFree ((y A) (y B) (y x))
  ((x is-not-free-in ((value y)  A))
   (x is-not-free-in ((value y)  B))
  ((A = B)  ( x (((value x)  A)  ((value x)  B)))))


  1. elsncg, metamath's, accessed August 7, 2010
  2. snid, metamath's, accessed August 5, 2010
  3. preqr1, metamath's, accessed August 4, 2010
  4. opelxp, metamath's, accessed November 3, 2010
  5. df-ss

Interface module parsed successfully