Proof of The Graph Reading of a Formula Tree Is Predicative and Agrees with Its Reading, So the Reading Is Predicative

(i) and (ii) are proved by induction on the tree $\varphi$ (Formula Trees with Values: Syntax, Two Readings, and Definedness (i)), for all $n$ at once; (iii) follows from them.

(i). Throughout, each occurrence of a parameter is written as a class variable of its own, standing for it, and the set variable a quantifier or a named value binds is chosen apart from the variables in scope. The free set variables of the formula built for a tree with $n$ set variables are then among $x_0, \dots, x_{n-1}$: at an atom or a named value, the terms it mentions lie in that range by well-scopedness, and each quantifier or named value binds the variable $x_n$ it introduces. Negation, conjunction and the set quantifier $\exists$ preserve predicativity, and $\vee$, $\Rightarrow$ and $\forall$ abbreviate predicative formulas, by Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations (ii) and Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations (v). Well-scopedness and the side conditions pass to subtrees, so it suffices to treat the atoms and the named values.

The atoms $s \in t$ and $s = t$ are predicative formulas by Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations (ii). The atoms $(u, v) \in A$ and $((u, v), w) \in A$, with ordered pairs, are predicative and say what the atom says by Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity (iii) and Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity (iv), which allow variables of either kind, not necessarily distinct, and need only that the terms inside the pairs are sets. In the map atom $F : A \to B$, the three terms are pairwise distinct variables: set variables among them are distinct by well-scopedness, and each occurrence of a parameter is a class variable of its own. So the formula $\mu(F, A, B)$ of Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity (vii), with its bound variables renamed apart as in Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations (vi), is predicative and says that the value of $F$ is a map from the value of $A$ to the value of $B$. An atom of its own is the reading of a predicative formula by its side condition.

For a named value $x_n = F(u)$, the graph reading is $\forall x_n\,((u, x_n) \in F \Rightarrow \varphi)$, where $\varphi$ is predicative by induction. The atom $(u, x_n) \in F$ is predicative and says what it says by Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity (iii), as $u$ is a set (a set variable, or a parameter the syntax requires to be a set). For $x_n = u \ast v$ the graph reading is $\forall x_n\,(((u, v), x_n) \in \ast \Rightarrow \varphi)$, and the atom is handled by Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity (iv) in the same way. For $x_n = \tau$ with $\theta$, the graph reading is $\forall x_n\,(\theta \Rightarrow \varphi)$, and $\theta$ is the reading of a predicative formula by its side condition.

(ii). For atoms, the two readings are the same condition. For the connectives and quantifiers, the claim follows from the induction hypothesis and Formula Trees with Values: Syntax, Two Readings, and Definedness (vi). For $\varphi \wedge \psi$ and $\varphi \Rightarrow \psi$, both readings agree on $\varphi$, and wherever $\varphi$ holds they agree on $\psi$. For $\varphi \vee \psi$, they agree on $\psi$ wherever $\varphi$ fails. Under a quantifier, an assignment of sets extended by a set is again one. For a named value $x_n = F(u)$: since $F$ is a function and $u$ lies in its domain, the value $F(u)$ is the only set $z$ with $(u, z) \in F$. So "for every set $x_n$ with $(u, x_n) \in F$, $\varphi$" says $\varphi$ at $x_n = F(u)$, which by induction is the reading. The same holds for $u \ast v$, written as in Binary Operations on a Set (ii): it is the value of the function $\ast$ at the pair $(u, v)$ in its domain, so by Functions, Values of a Function, and Functions from One Class to Another (ii) it is the only set $z$ with $((u, v), z) \in \ast$. It also holds for $\tau$ with $\theta$, since $\tau$ is a set satisfying $\theta$ and the only one.

(iii). By (i), the graph reading of $\varphi$ is the reading of a predicative formula in $x_0, \dots, x_{n-1}$ and the parameters of $\varphi$. By hypothesis $\varphi$ uses its values properly under every assignment of sets to $x_0, \dots, x_{n-1}$. So by (ii), its graph reading and its reading hold under the same such assignments, and its reading is the reading of the same predicative formula.