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

Both claims are proved by induction on the tree $\varphi$, for all $n$ at once.

(i). 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), and the atoms with ordered pairs $(u, v) \in A$ and $((u, v), w) \in A$ and the map atom $F : A \to B$ 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), 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) 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 (vii); the side conditions give what these need (a parameter in a pair is a set), and well-scopedness gives the rest (the terms are bound, and the three terms of a map atom are distinct variables). An atom of its own is predicative by its side condition. Negation, conjunction and the set quantifier $\exists$ preserve predicativity by Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations (ii), and $\vee$, $\Rightarrow$ and $\forall$ are abbreviations of predicative formulas, also by Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations (ii). For a named value $z = F(x_i)$ the graph reading is $\forall z\,((x_i, z) \in F \Rightarrow \varphi)$, predicative by Predicative Substitution of Values of Functions and Binary Operations, and Predicative Formulas for Negatives, Differences, Absolute Values, Distances, Reciprocals and Quotients in an Ordered Field (i) since $\varphi$ is predicative by induction, $x_i$ is bound and $F$ is not $x_i$; for $z = x_i \ast x_j$ likewise by Predicative Substitution of Values of Functions and Binary Operations, and Predicative Formulas for Negatives, Differences, Absolute Values, Distances, Reciprocals and Quotients in an Ordered Field (ii); and for $z = \tau$ with $\theta$ it is $\forall z\,(\theta \Rightarrow \varphi)$, predicative since $\theta$ is (a side condition) and $\varphi$ is.

(ii). For atoms the two readings are the same condition. For the connectives and quantifiers the claim follows from the induction hypothesis: for $\varphi \wedge \psi$ and $\varphi \Rightarrow \psi$, both sides 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 $z = F(x_i)$: as $F$ is a function and $x_i$ lies in its domain, the value $F(x_i)$ is a set with $(x_i, F(x_i)) \in F$, and it is the only set $z$ with $(x_i, z) \in F$. So "for every set $z$ with $(x_i, z) \in F$, $\varphi$" says $\varphi$ at $z = F(x_i)$, which by induction is the reading. The same holds for $x_i \ast x_j$, which by Binary Operations on a Set (ii) is the value of the operation at the pair $(x_i, x_j)$, and for $\tau$ with $\theta$, which is a set satisfying $\theta$ and the only one.