  The schema of separation allows us to form a subset of a given set whose elements satisfy a given property (expressed by a formula in the language of set theory). Given a set \(B\) and a formula \(\phi(X)\), separation allows us to construct a new set, the set of those elements \(X\) of \(B\) for which \(\phi\) holds. This is usually informally represented as: \(\{X \in B : \phi(X)\}\). Separation may lead to impredicativity in case the formula \(\phi\) contains unbounded quantifiers ranging over the whole universe of sets; in fact, in defining the new set by separation we may thus refer to this very set, contradicting Russell’s VCP. For example, if we define a set \(C\) by separation as \(\{X\in B : \forall Y \psi(X,Y)\}\), then \(C\) is among the \(Y\)’s that need to be checked for the property \(\psi\).  This form of impredicativity is avoided in constructive set theory by restricting the separation schema: by requiring that all quantifiers occurring in the formula \(\phi\) range only over “previously constructed” sets. Syntactically, this means that given a set \(B\), we can form a new set \(\{X \in B : \phi(X)\}\) by separation only if all quantifiers in \(\phi\) are bounded; that is, only if all quantifiers in \(\phi\) are of the form \(\forall X (X\in Y \rightarrow \ldots)\) or \(\exists X(X\in Y \wedge \ldots)\), for some set \(Y\).