Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity

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; set variables and class variables are as in Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations §symbols, and sets and classes are assigned to them as in Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations §reading.

¶ Let $\varphi$ be a predicative formula built by the rules of Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations §formula, its abbreviations $\vee$, $\Rightarrow$, $\Leftrightarrow$, $\forall$ and $\notin$ read as the strings they abbreviate there. Let $k\ge0$ be a metatheoretic number, let $v_{1},\dots,v_{k}$ be distinct set variables, and let $y_{1},\dots,y_{k}$ be variables of either kind, not necessarily distinct; $\varphi$ may have further free variables of either kind, which may be among $y_{1},\dots,y_{k}$. Let $\varphi[y/v]$ be the formula obtained from $\varphi$ by first replacing each part $\exists s\,\psi$ of $\varphi$ with $s$ among $y_{1},\dots,y_{k}$ by $\exists s'\,\psi'$, where $s'$ is a set variable occurring neither in $\varphi$ nor among $y_{1},\dots,y_{k}$, distinct for distinct occurrences of such parts, and $\psi'$ is $\psi$ with the free occurrences of $s$ replaced by $s'$; and then replacing, simultaneously for $i=1,\dots,k$, each free occurrence of $v_{i}$ by $y_{i}$. Then $\varphi[y/v]$ is predicative. Moreover, for every assignment to the free variables of $\varphi[y/v]$ and to $y_{1},\dots,y_{k}$ in which a set is assigned to each class variable among $y_{1},\dots,y_{k}$, $\varphi[y/v]$ holds if and only if $\varphi$ holds when each $v_{i}$ is assigned the value of $y_{i}$ and every other free variable of $\varphi$ keeps its value.

In the clauses pair-equality, pair-membership and operation-membership, $s$ is a variable of either kind, $t'_{1}$, $t'_{2}$ and $t'_{3}$ are distinct set variables other than $s$, and $\pi_{1}$, $\pi_{2}$ and $\pi_{3}$ are the formulas obtained, as in Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations §defined-symbols, by eliminating the ordered pairs, used as defined set symbols, from $s=(t'_{1},t'_{2})$, $(t'_{1},t'_{2})\in s$ and $((t'_{1},t'_{2}),t'_{3})\in s$. For variables $t_{1}$, $t_{2}$, $t_{3}$ of either kind, not necessarily distinct and possibly equal to $s$, the formulas $s=(t_{1},t_{2})$, $(t_{1},t_{2})\in s$ and $((t_{1},t_{2}),t_{3})\in s$ are $\pi_{1}[t/t']$, $\pi_{2}[t/t']$ and $\pi_{3}[t/t']$, formed as in the clause renaming with $t'_{i}$ for $v_{i}$ and $t_{i}$ for $y_{i}$ ($k=2$, $2$ and $3$ respectively).

¶ The formula $s=(t_{1},t_{2})$ is predicative; and when sets are assigned to $t_{1}$ and $t_{2}$, it holds if and only if the value of $s$ is the ordered pair of the values of $t_{1}$ and $t_{2}$.

¶ The formula $(t_{1},t_{2})\in s$ is predicative; and when sets are assigned to $t_{1}$ and $t_{2}$, it holds if and only if the ordered pair of the values of $t_{1}$ and $t_{2}$ is an element of the value of $s$.

¶ The formula $((t_{1},t_{2}),t_{3})\in s$ is predicative; and when sets are assigned to $t_{1}$, $t_{2}$ and $t_{3}$, it holds if and only if the ordered pair of the ordered pair of the values of $t_{1}$ and $t_{2}$ and the value of $t_{3}$ is an element of the value of $s$.

In the remaining clauses, $F$, $A$, $B$, $p$, $u$, $u'$, $v$ and $v'$ are pairwise distinct variables, $p$, $u$, $u'$, $v$ and $v'$ being set variables and $F$, $A$ and $B$ variables of either kind, and $(u,v)$ is the ordered pair, used as a defined set symbol. The free variables of each displayed formula are exactly the displayed letters among $F$, $A$ and $B$.

¶ Let $\rho(F)$ be the formula $\forall p\,(p\in F\Rightarrow\exists u\,\exists v\,(p=(u,v)))$. It is predicative, and a class $F$ is a relation if and only if $\rho(F)$.

¶ Let $\Phi(F)$ be the formula $\rho(F)\wedge\forall u\,\forall v\,\forall v'\,(((u,v)\in F\wedge(u,v')\in F)\Rightarrow v=v')$. It is predicative, and a class $F$ is a function if and only if $\Phi(F)$.

¶ Let $\mu(F,A,B)$ be the formula $\Phi(F)\wedge\forall u\,(u\in A\Leftrightarrow\exists v\,((u,v)\in F))\wedge\forall u\,\forall v\,((u,v)\in F\Rightarrow v\in B)$. It is predicative, and for classes $F$, $A$ and $B$, $F$ is a map $F:A\to B$ if and only if $\mu(F,A,B)$.

¶ Let $\iota(F)$ be the formula $\forall u\,\forall u'\,\forall v\,(((u,v)\in F\wedge(u',v)\in F)\Rightarrow u=u')$. It is predicative, and for classes $A$ and $B$ and a map $F:A\to B$, $F$ is injective if and only if $\iota(F)$.

¶ Let $\sigma(F,B)$ be the formula $\forall v\,(v\in B\Rightarrow\exists u\,((u,v)\in F))$. It is predicative, and for classes $A$ and $B$ and a map $F:A\to B$, $F$ is surjective if and only if $\sigma(F,B)$.

¶ The formula $\mu(F,A,B)\wedge\iota(F)\wedge\sigma(F,B)$ is predicative, and for classes $F$, $A$ and $B$, $F$ is a bijection from $A$ to $B$ if and only if this formula holds.