Difference between impredicative and predicative version of separation axiom

Question

What is the difference between an impredicative and a predicative version of the separation axiom in ZFC:

$$\forall x \exists y \forall z ( z\in y \leftrightarrow (z \in x \wedge \phi (z)) $$

What are the philosophical concerns in adopting an impredicative version?

Answer 1

You have to refer to the so-called cumulative hierarchy :

One motivation for the $\mathsf {ZFC}$ axioms is the cumulative hierarchy of sets introduced by John von Neumann. In this viewpoint, the universe of set theory is built up in stages, with one stage for each ordinal number. At stage $0$ there are no sets yet. At each following stage, a set is added to the universe if all of its elements have been added at previous stages. Thus the empty set is added at stage $1$, and the set containing the empty set is added at stage $2$. The collection of all sets that are obtained in this way, over all the stages, is known as $\mathsf V$.

For example, suppose that a set $x$ is added at stage $\alpha$, which means that every element of $x$ was added at a stage earlier than $\alpha$. Then every subset of $x$ is also added at stage $\alpha$, because all elements of any subset of $x$ were also added before stage $\alpha$. This means that any subset of $x$ which the axiom of separation can construct is added at stage $\alpha$, and that the powerset of $x$ will be added at the next stage after $\alpha$.

It is possible to change the definition of $\mathsf V$ so that at each stage, instead of adding all the subsets of the union of the previous stages, subsets are only added if they are definable in a certain sense. This results in a more "narrow" hierarchy which gives the constructible universe $\mathsf L$, which also satisfies all the axioms of $\mathsf {ZFC}$, including the axiom of choice.

A possible "restriction" is through the Axiom schema of predicative separation where the formula $\varphi$ used to "separate" the set $y$ from the existing set $x$ must be restricted.

It only asserts the existence of a subset of a set if that subset can be defined without reference to the entire universe of sets.

The axiom appears in the systems of constructive set theory $\mathsf {CZF}$, as well as in the system of Kripke–Platek set theory.

The formal statement of this is the same as full separation schema, but with a restriction on the formulas that may be used.

The formula $\varphi$ contains only bounded quantifiers. That is, all quantifiers in $\varphi$ (if there are any) must appear in the form $(\exists x \in y )\psi(x)$ or $(\forall x \in y )\psi(x)$, for some sub-formula $\psi$.

The meaning of this is that, given any set $x$, and any predicate $\varphi$ there is a set $y$ whose elements are the elements of $x$ which satisfy $\varphi$, provided $\varphi$ only quantifies over existing sets, and never quantifies over all sets. This restriction is necessary from a predicative point of view, since the universe of all sets contains the set being defined. If it were referenced in the definition of the set, the definition would be circular.