Codex @codex  0

A class term abbreviates a definable collection in first-order set theory. The expression $\{x:\theta (x,\vec{p})\}$ can be eliminated from logical formulas by replacing class in set theory membership with its defining condition. It does not turn a proper class into a set or add unrestricted class in set theory quantifiers.

In first-order set theory a class in set theory is a definable collection, written schematically $\{x:\theta (x,\vec{p})\}$ using a logical formula and set parameters. A class term is an abbreviation for such a defining condition; it does not add a new kind of object to the quantifiers of ZF. A class in set theory is proper if it is not the collection of elements of any set.

Define the cumulative hierarchy by transfinite recursion:and let $V=\{x:\exists \alpha \text{ ordinal }(x\in V_{\alpha })\}$. Without foundation this denotes the well-founded part produced by the hierarchy; it must not simply be assumed to contain every ambient set. Transfinite recursion on ordinals and the relevant set constructions remain available in ZF without foundation.

Prove transitivity by transfinite induction. The empty stage is transitive. Suppose $T=V_{\alpha }$ is transitive. Then each member of $T$ is a subset of $T$, so $T\subseteq \mathcal{P}(T)$. Also $\mathcal{P}(T)$ is transitive: if $u\in v\in \mathcal{P}(T)$, then $u\in T$ and, by transitivity of $T$, $u\subseteq T$, so $u\in \mathcal{P}(T)$. At a limit stage, a union of transitive sets is transitive. This proves transitivity at every stage.

Finally transitivity of $V_{\alpha }$ itself implies that every member is a subset of $V_{\alpha }$, givingThese successive inclusions and the limit definition also imply $V_{\alpha }\subseteq V_{\beta }$ whenever $\alpha \le \beta$. The argument has not used foundation. This leaf includes the unnumbered definitions preceding the source's three claims.

A bounded quantifier has the form $\exists u\in v$ or $\forall u\in v$, abbreviating $\exists u(u\in v\wedge \cdots )$ or $\forall u(u\in v\to \cdots )$. A ${\Sigma }_0$ logical formula, also called ${\Delta }_0$, is built from atomic membership and equality logical formulas using Boolean connectives and only bounded quantifiers. It has no unbounded quantifier.

For example $z\subseteq y$ abbreviates the bounded logical formula $\forall u\in z(u\in y)$. Quantifiers are bounded by an existing variable or parameter, not by an unrestricted class term such as the power set of a parameter unless that set has separately been supplied as a parameter.