What are some primary mathematical utilities of the axiom schema of separation?

Question

I read a discussion concerning the axiom schema of specification, which I yet take as saying that for every set and a class-defining condition, those elements of the set satisfying this condition extensionally comprise another set, given no antinomies are incurred therein.

First: Does my summary capture the semantic intention of the expression of the axiom in formal logic?

Second: Can you give me some insight into the significance of this statement, and explain why it is granted axiomatic status?

---

Additional Info:

Is it true that the axiom schema of specification is thought primarily to resolve the antinomies derivable from the Frege-an schema of unrestricted comprehension for classes, and more broadly as a tool with which to confide in the true existence of certain sets smaller than known sets as elements of which the elements of the former exist?

Answer 1

We have to make a distinction, e.g., between a set and a predicate which describes a class of sets. Because of Russell's paradox not every predicate is a set, or better said, not every predicate has an extension, which is a set of all sets satisfying the predicate. The solution to this paradox in set theory is that sets are small and that the class of all sets satisfying a predicate may be too large. The axiom of separation expresses an important part of this.

Maybe this does not answer your question. I cannot tell until you clarify what the question is.

Answer 2

Your summary does not contain all the power of the subset axiom schema. It is not only intersection, it is also union, difference, as well quantified formulas.

To be more accurate for any formula in the language of set theory if we fix parameters so the formula has only one free variable $x$, then the collection of all those which are members of a particular set and satisfy this formula is a set.

Formally this means that if $\varphi(x,y_1,\ldots,y_k)$ is a formula in the language of set theory we have the following axiom: $$\forall p_1\ldots\forall p_k\forall A\exists B\bigg(u\in B\leftrightarrow\Big(u\in A\land\varphi(u,p_1,\ldots,p_k)\Big)\bigg)$$ which says that once we fix the parameters then for every set $A$ there is a set $B$ which is exactly the subset of $A$ consisting of those satisfying $\varphi$ (with the chosen parameters).

The importance of this axiom schema is to allow us and generate new sets. This is not only the union and the intersection of sets. The formulas can get increasing complicated which will then allow us to generate more and more sets. The parameters can vary greatly and increase the complexity.

For example, one example would be $\varphi(x,p_1)$ holds if and only if $p_1$ is $\omega+1$ (the natural numbers+a point at infinity) and $x$ is a set such that there exists $R\subseteq x\times x$ and $f\subseteq x\times p_1$ a bijection such that $f$ witnesses an order isomorphism between $(x,R)$ and $(p_1,\in)$.

If we apply this formula on $A=\mathcal P(\mathbb R)$ we will have all those sets of real numbers which are well-ordered with order type $\omega+1$. This is not "merely" an intersection of two sets. This is something I may use in an actual proof.

The last line, too, should hint that this is useful for proofs. The universe is big and contains a lot of things we don't know about in details. However it also known not to contain things we which do know about in details. The axiom schema of subset (or the stronger one, replacement) allow us to ensure the existence of sets when we need them (e.g. during proofs).

Answer 3

A few comments to supplement Asaf's answer:

If you're working in an NBG-style formalization of set theory, the separation axiom does indeed simply say that the intersection of a set and a class is a set. But that's just a superficial technicality, since classes in NBG are just proxies for properties and not really meant to be "objects of thought" in themselves like sets are. With this intuition, what the NBG separation axiom actually claims is that any definable subset of a set is a set, just like the ZF one.

You probably shouldn't think of the Separation axiom as something intended to do one particular very important thing -- rather its the Swiss knife we use to do almost everything with. Historically, it arose not as some principled extension of some weaker system, but as all that is left of Cantor's bold universal comprehension scheme $$ \forall x_1\cdots\forall x_n. \exists z. \forall y. y\in z \Leftrightarrow \phi(y,x_1,\ldots,x_n)$$ after it was reduced in scope such that it (hopefully) avoids paradoxes such as Russell's or Buralli-Forti's pardoxes. It is the standard tool for defining new sets.

Since Separation creates only sets that are smaller than some set we already know, we also have a small selection of carefully chosen axioms for creating larger sets: Paring, Union, Power set, Infinity, and Replacement. These, in contrast to Separation, have fairly specific roles.

In some presentations of axiomatic set theory, Replacement is phrased such that it subsumes Separation. However, it seems to be more common to let Separation be its own axiom and then word all of the larger-set axioms including Replacement such that they just claim that "there is a set containing at least such-and-such elements". One then always needs to combine each of them with Separation in order to get a set that is known to contain exactly such-and-such elements.

Answer 4

The axiom schema of separation does not bestow sethood on any describable set; it bestows sethood on any describable subset (provided the selection criteria makes no reference to the subset itself).

Suppose, for example, you have a set $U$. Then you can legitimately select a subset $r$ from $U$ such that:

$\forall a (a\in r \leftrightarrow (a\in U \wedge a\notin a))$

(Note that the selection criteria $a\notin a$ makes no reference to $r$.)

Because $r\subset U$, the existence of $r$ doesn't seem to lead to a contradiction as in Russell's Paradox.

Edit: While a contradiction has not been proven impossible, after over a century of extensive research in this area (starting with E. Zermelo's 1908 paper), one seems highly unlikely.

You can prove that $r\notin r$ and $r\notin U$. See formal proof at http://www.dcproof.com/SeparationAxiom.htm