Formula Trees with Values: Syntax, Two Readings, and Definedness

Formulas are read as in Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations (iv). A formula with $n$ set variables reads them as $x_0, \dots, x_{n-1}$, which are assigned sets. A term is a set variable $x_i$ or a parameter, a fixed class.

(i) Formula trees. Let $s, t, u, v, w, F, A, B, \ast$ be terms. The formula trees with $n$ set variables are built as follows. The atoms are $s \in t$, $s = t$, $(u, v) \in A$ and $((u, v), w) \in A$, with ordered pairs; the atom $F : A \to B$, a map; and any condition on $x_0, \dots, x_{n-1}$, called an atom of its own. If $\varphi$ and $\psi$ are trees with $n$ set variables, so are $\neg \varphi$, $\varphi \wedge \psi$, $\varphi \vee \psi$ and $\varphi \Rightarrow \psi$. If $\varphi$ is a tree with $n + 1$ set variables, then $\forall x_n\, \varphi$ and $\exists x_n\, \varphi$ are trees with $n$ set variables, and so are the trees that name a value as $x_n$ before $\varphi$ uses it:

$$x_n = F(u), \qquad x_n = u \ast v, \qquad x_n = \tau \text{ with } \theta.$$

Here $F(u)$ is the value of $F$ at $u$, and $u \ast v$ is the value of the term $\ast$ at the pair $(u, v)$, in the notation of Binary Operations on a Set (ii), used here for any function $\ast$. In the third form, $\tau$ is a class depending on $x_0, \dots, x_{n-1}$, and $\theta$ is a condition on $x_0, \dots, x_n$. Every parameter that stands inside an ordered pair, or as an argument $u$ or $v$ of a named value, is a set.

(ii) Scope. A tree is well scoped if three conditions hold. Every set variable $x_k$ it mentions occurs at an atom or a named value with more than $k$ set variables. No $F$ or $\ast$ that names a value is the same set variable as one of its arguments. The three terms of a map atom $F : A \to B$ are pairwise not the same set variable.

(iii) Side conditions. The side conditions of a tree are: the parameters that (i) requires to be sets are sets; each atom of its own is the reading of a predicative formula whose free variables are among the set variables at its place and class variables standing for parameters; and each condition $\theta$ that names a value as $x_n$ is the reading of such a formula, with $x_0, \dots, x_n$ as its set variables.

(iv) Reading. The reading of a tree is taken under an assignment of sets at which every value of the tree is used properly, as in (vi); the two notions are defined together, by recursion on the tree. Quantifiers range over sets, and each named variable is assigned the value itself: $F(u)$, $u \ast v$ or $\tau$. In a compound, the second part $\psi$ is read only where (vi) asks it to use its values properly, and elsewhere the first part $\varphi$ decides: $\varphi \wedge \psi$ fails where $\varphi$ fails, $\varphi \Rightarrow \psi$ holds where $\varphi$ fails, and $\varphi \vee \psi$ holds where $\varphi$ holds.

(v) Graph reading. The graph reading of a tree, under any assignment of sets, reads every part as itself, connectives and quantifiers (over sets) included, except that each named value is replaced by its graph:

$$\begin{aligned} x_n = F(u) \text{ before } \varphi &\quad\text{reads}\quad \text{for every set } x_n \text{ with } (u, x_n) \in F,\ \varphi;\\ x_n = u \ast v \text{ before } \varphi &\quad\text{reads}\quad \text{for every set } x_n \text{ with } ((u, v), x_n) \in \ast,\ \varphi;\\ x_n = \tau \text{ with } \theta \text{ before } \varphi &\quad\text{reads}\quad \text{for every set } x_n \text{ satisfying } \theta,\ \varphi. \end{aligned}$$

(vi) Proper use. Whether a tree uses its values properly under an assignment of sets is defined by recursion. An atom uses no value, so it always does. $\neg \varphi$ does when $\varphi$ does. $\varphi \wedge \psi$ and $\varphi \Rightarrow \psi$ do when $\varphi$ does and, wherever the reading of $\varphi$ holds, $\psi$ does; $\varphi \vee \psi$ likewise, with "fails" in place of "holds". $\forall x_n\, \varphi$ and $\exists x_n\, \varphi$ do when $\varphi$ does at every set assigned to $x_n$. A tree naming a value does when the value exists and $\varphi$ uses its values properly with $x_n$ assigned that value. For $F(u)$, existence means that $F$ is a function and $u$ lies in its domain. For $u \ast v$, it means that $\ast$ is a function and $(u, v)$ lies in its domain. For $\tau$ with $\theta$, it means that $\tau$ is a set satisfying $\theta$ and every set satisfying $\theta$ equals $\tau$.