Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols

In the setting of Class Theory NBG: the Axioms, Standing Conventions and Basic Notation, formulas may be written with abbreviations, and predicative is then meant as in Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations §defined-symbols. In each clause below, distinct letters denote distinct variables, and a variable displayed in a clause occurs in the formulas of that clause only where displayed. The letters $u$, $v$, $w$, $x$, $z$, $p$ and $t$ denote set variables. The formulas may have further free variables of either kind, their parameters; every hypothesis and every conclusion is meant for all values of the parameters, sets being assigned to set variables and classes to class variables.

¶ This clause is a statement of the metatheory about expressions. Every expression written with abbreviations as in Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations §defined-symbols in which no quantifier is applied to a class variable, counting the quantifiers inside the formulas of the class abstractions written in it and counting $\forall X$ as a quantifier applied to $X$, is predicative.

¶ Let $k\ge0$ be a metatheoretic number, let $v_{1},\dots,v_{k}$ be set variables, and let $\theta(z,v_{1},\dots,v_{k})$ and $\gamma(v_{1},\dots,v_{k})$ be predicative formulas such that, for all sets $v_{1},\dots,v_{k}$ satisfying $\gamma$, exactly one set $z$ satisfies $\theta(z,v_{1},\dots,v_{k})$; write $\tau(v_{1},\dots,v_{k})$ for it. Let $\varphi(z,v_{1},\dots,v_{k})$ be a predicative formula; $\gamma$, $\theta$ and $\varphi$ share their parameters, and a condition on the parameters belongs in $\gamma$. Below, $\varphi(\tau(v_{1},\dots,v_{k}),v_{1},\dots,v_{k})$ is $\varphi(z,v_{1},\dots,v_{k})$ for the set $z=\tau(v_{1},\dots,v_{k})$. Then for all sets $v_{1},\dots,v_{k}$ satisfying $\gamma$,

$$\varphi(\tau(v_{1},\dots,v_{k}),v_{1},\dots,v_{k})\iff\exists z\,(\theta\wedge\varphi)\iff\forall z\,(\theta\Rightarrow\varphi),$$

and the formulas $\gamma\wedge\exists z\,(\theta\wedge\varphi)$ and $\gamma\Rightarrow\forall z\,(\theta\Rightarrow\varphi)$ are predicative.

¶ For every set $z$: $z=\emptyset$, the empty set, if and only if $\forall w\,(w\notin z)$.

¶ For all sets $u$, $v$ and $z$: $z=\{u,v\}$, the unordered pair, if and only if $\forall w\,(w\in z\Leftrightarrow(w=u\vee w=v))$; and $z=\{u\}$, the singleton, if and only if $\forall w\,(w\in z\Leftrightarrow w=u)$.

¶ For all sets $u$, $v$ and $z$: $z=(u,v)$, the ordered pair, if and only if

$$\forall w\,\bigl(w\in z\Leftrightarrow(\forall t\,(t\in w\Leftrightarrow t=u)\vee\forall t\,(t\in w\Leftrightarrow(t=u\vee t=v)))\bigr).$$

¶ For all sets $u$ and $v$ and every class $A$, a set $A$ included: $(u,v)\in A$ if and only if $\exists p\,(p=(u,v)\wedge p\in A)$, where $p=(u,v)$ has the form given by the clause ordered-pair. In particular, for a relation $R$, $u\,R\,v$ if and only if $\exists p\,(p=(u,v)\wedge p\in R)$.

¶ For all sets $u$ and $z$: $z=\bigcup u$, the union, if and only if $\forall w\,(w\in z\Leftrightarrow\exists v\,(w\in v\wedge v\in u))$; and $z=\mathcal{P}(u)$, the power set, if and only if $\forall w\,(w\in z\Leftrightarrow\forall v\,(v\in w\Rightarrow v\in u))$.

¶ Let $m\ge0$ be a metatheoretic number, let $\psi(x,Y_{1},\dots,Y_{m})$ be a predicative formula with parameters $Y_{1},\dots,Y_{m}$ of either kind, and let $T$ be the class abstraction $\{x:\psi(x,Y_{1},\dots,Y_{m})\}$. For every set $u$ and every class $A$: $u\in T$ if and only if $\psi(u,Y_{1},\dots,Y_{m})$; $A=T$ if and only if $\forall w\,(w\in A\Leftrightarrow\psi(w,Y_{1},\dots,Y_{m}))$; and $A\in T$ if and only if $\exists z\,(\forall w\,(w\in z\Leftrightarrow w\in A)\wedge\psi(z,Y_{1},\dots,Y_{m}))$.

¶ For all sets $u$, $v$ and $z$, with the intersection, union and difference: $z=u\cap v$ if and only if $\forall w\,(w\in z\Leftrightarrow(w\in u\wedge w\in v))$; $z=u\cup v$ if and only if $\forall w\,(w\in z\Leftrightarrow(w\in u\vee w\in v))$; and $z=u\setminus v$ if and only if $\forall w\,(w\in z\Leftrightarrow(w\in u\wedge w\notin v))$.

¶ Let $F$ be a function. For all sets $u$ and $z$: $u$ lies in the domain $\operatorname{dom}F$ and $z$ is the value $F(u)$ if and only if $(u,z)\in F$.

¶ Let $a$ be a set and $\ast$ a binary operation on $a$. For all sets $u$, $v$ and $z$: $u\in a$, $v\in a$ and $z=u\ast v$, in the notation for its values, if and only if $((u,v),z)\in\ast$.