The construction that allows us to form sets with more than two elements is the union. It allows us to take existing sets and form a single set containing all the elements of those sets.
Axiom (Union)
Given a set of sets, there exists a set such that if and only if for some .
Definition Given a set of sets, we call a set as in the Axiom of Union, a union over and denote it .
Example Let , and . Now let . Then .
Theorem Given a set of sets as in the Axiom of Union, the union over is unique.
Proof If and were both unions over then iff for some . Similarly iff for some . Thus iff , and so by extensionality.
We recover the familiar definition of the union of two sets as follows.
Definition If we denote by and call it the union of and .
Theorem If and are sets then is a set.
Proof By the Axiom of Pair, is a set. Thus by the Axiom of Union is a set.
Comprehensions allow us to select elements of an existing set that have some specified property. The Axiom Schema of Comprehension says that such selections define sets.
There is very little restriction on the properties we may use in comprehensions, except that they must be specified with formulas in the language of set theory and formal logic.
We first define what we mean by a formula.
Definition A formula can contain variables of which we are allowed an unlimited supply, and constants, i.e. specific sets say, and must be built up using a finite number of the following:
Expressions of the form and are formulas, called atomic formulas, for all variables and constants and .
If and are formulas then , , , and are formulas.
If is a formula then and are formulas.
Here stands for logical or, is logical and, is logical negation, is implies and stands for if and only if, which we shall often abbreviate iff.
The expression is called a universal quantifier. It means for all sets . The expression is an existential quantifier. It means there exists a set .
Example Given a set the expression is an example of a formula.
Although symbols , , etc., and for there exists a unique, are not part of the formal language, we can define them in terms of the existing language of set theory.
For example, can be written . Similarly, can be written .
Definition In a formula, any variable inside an expression of the form or of the form is said to be bound. All other variables in a formula are said to be free, or arguments of the formula.
We are now in a position to state the Axiom Schema of Comprehension.
Axiom Schema (Comprehension)
For a set and a property there exists a set consisting of the for which holds.
Note that this is not just one axiom, but an axiom for each possible property. We call a collection of axioms like this an axiom schema.
Technically the formula can have finitely many free variables, so is sometimes denoted where the are free variables. But we suppress this technicality for now and just write .
Theorem The set of elements of a set for which a property holds is unique.
Proof This follows by noting that if there were two such sets and then iff and holds. However, this is the case iff . Thus iff and the result follows by extensionality.
Definition The set of elements of a set for which holds is denoted .
We can read the vertical bar as such that.
Example If then .
The Axiom Schema of Comprehension is sometimes called the Subset Axiom Scheme or Axiom Schema of Specification, since it guarantees that any subset of a set specified by a formula, is a set.