Axiom Schema of Specification
We move onto our next axiom, known as either the axiom of specification, separation, or comprehension. The axiom states that given some set A, there exists some B such that for all x \in A, x \in B if and only if \phi(x) holds. Our choice of formula \phi is arbitrary, but first order logic does not allow us to quantify over formulas. Thus we instead have an infinite schema of axioms, one for each formula.
The axiom of specification tells us that any subset (which we will formally define later) of A which can be defined by a formula is a set. We commonly use specification to show that a set exists, by establishing a larger set and then a formula to specify only the elements we want in our desired set.
Restrictions on Specification
The requirement that our desired set B must be a subset of A is to avoid Russels’ paradox, and the problems with unrestricted comprehension discussed previously. Unfortunately this means that the axioms of Specification cannot be used to create larger sets. Whereas with unrestricted comprehension we could create the union of sets A \cup B, specification only allows us to create restricted smaller sets.
We must also notice that we can only prove the existence of some set B if there exists a formula \phi such that each member of B satisfies \phi. However we will later see that given some infinite sets, it is impossible to construct a formula such that each element of the set satisfies the formula; thus the axiom of specification cannot be used to prove the existence of those sets.
And the final restriction on specification is that although \phi can have any number of free variables t, B must not be free in our formula \phi. This is to prevent circularity, else we could take \phi to be x \not \in B and any set A to obtain the axiom
\exists B \forall x(x \in B \iff (x \in A \land x \not \in B)).
This creates a paradox, as x \in B if and only if x \not \in B. For this reason B must not appear free in our formula \phi. We now start to develop some set theory using only the axioms of extension and specification!