Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations

This definition belongs to the metatheory: it describes finite strings of symbols, not classes. Numbers $n,k,m$ appearing below are metatheoretic counts of symbols or variables.

¶ The symbols are: the class variables $X,Y,Z,X_{1},X_{2},\dots$ and the set variables $x,y,z,u,v,w,x_{1},x_{2},\dots$, two disjoint infinite lists, in which letters of the respective case, possibly primed or indexed, also serve as variables; the membership symbol $\in$; the equality symbol $=$, which is the equality of the underlying first-order logic with equality, so that it is reflexive and equals may be substituted for one another in every formula; the connectives $\neg$ and $\wedge$; the quantifier symbol $\exists$; and parentheses. A variable is a variable of either kind.

¶ The formulas are the strings obtained by finitely many applications of the following rules: for variables $s$ and $t$, the strings $s\in t$ and $s=t$ are formulas (the atomic formulas); if $\varphi$ and $\psi$ are formulas, so are $\neg\varphi$ and $(\varphi\wedge\psi)$; if $\varphi$ is a formula and $v$ is a variable, $\exists v\,\varphi$ is a formula. The strings $(\varphi\vee\psi)$, $(\varphi\Rightarrow\psi)$, $(\varphi\Leftrightarrow\psi)$ and $\forall v\,\varphi$ abbreviate $\neg(\neg\varphi\wedge\neg\psi)$, $\neg(\varphi\wedge\neg\psi)$, $((\varphi\Rightarrow\psi)\wedge(\psi\Rightarrow\varphi))$ and $\neg\exists v\,\neg\varphi$, and $s\notin t$ abbreviates $\neg\, s\in t$.

¶ An occurrence of a variable $v$ in a formula $\varphi$ is bound if it lies inside a part of $\varphi$ of the form $\exists v\,\psi$, and free otherwise; the free variables of $\varphi$ are the variables with a free occurrence in $\varphi$. Writing $\varphi(v_{1},\dots,v_{k})$ indicates that the free variables of $\varphi$ are among the distinct variables $v_{1},\dots,v_{k}$.

¶ A formula is read in the usual way, with class variables standing for classes, set variables standing for sets, $\in$ for membership and $=$ for equality; in particular $\exists x\,\varphi$, for a set variable $x$, reads "there is a set $x$ such that $\varphi$". For classes $A_{1},\dots,A_{k}$, assigned to $v_{1},\dots,v_{k}$ with sets assigned to the set variables among them, $\varphi(A_{1},\dots,A_{k})$ denotes the statement so obtained about $A_{1},\dots,A_{k}$.

¶ A formula is predicative if it has no part of the form $\exists X\,\psi$ with $X$ a class variable; that is, it quantifies over set variables only.

¶ Later items introduce abbreviations of three kinds, each given by a predicative expression that may itself use abbreviations introduced earlier; here $k\ge0$, and $w$ and $z$ denote set variables occurring nowhere else. An expression containing abbreviations stands for the formula obtained by eliminating them by the rules below, repeated until none remains, after renaming bound variables of the substituted formulas where necessary so that no variable is captured; this terminates, since each abbreviation is given in terms of abbreviations introduced before it. The expression is predicative if the resulting formula is.

¶ A defined predicate $P(v_{1},\dots,v_{k})$, such as $X\subseteq Y$, is introduced as an abbreviation of a predicative formula, and is eliminated by substituting that formula.

¶ A defined set symbol $t(v_{1},\dots,v_{k})$, such as $\emptyset$ or $\{x,y\}$, is introduced as the unique set $z$ satisfying a predicative $\theta(z,v_{1},\dots,v_{k})$, its arguments $v_{1},\dots,v_{k}$ being of the kinds specified where it is introduced. The elimination rule gives every expression a meaning, but the symbol is used only properly: at each place of use, the hypotheses in force there, including the left conjunct of $x\in A\wedge\varphi$ and the antecedent of $\forall x\,(x\in A\Rightarrow\varphi)$, ensure that exactly one such set exists. An atomic part $\alpha(t)$ in which it occurs is replaced by $\exists z\,(\theta(z,v_{1},\dots,v_{k})\wedge\alpha(z))$.

¶ A class term $T$, such as a class abstraction $\{x:\psi\}$, is introduced together with a predicative formula $\sigma_{T}(w)$ expressing that the set $w$ is an element of $T$. Atomic parts containing $T$ are replaced as follows, where $s$ is a variable of either kind and $T'$ a second class term: $s\in T$ by $\sigma_{T}(s)$ if $s$ is a set variable, and by $\exists z\,(\forall w\,(w\in z\Leftrightarrow w\in s)\wedge\sigma_{T}(z))$ if $s$ is a class variable; $s=T$ and $T=s$ by $\forall w\,(w\in s\Leftrightarrow\sigma_{T}(w))$; $T\in s$ by $\exists z\,(\forall w\,(w\in z\Leftrightarrow\sigma_{T}(w))\wedge z\in s)$; $T\in T'$ by $\exists z\,(\forall w\,(w\in z\Leftrightarrow\sigma_{T}(w))\wedge\sigma_{T'}(z))$; and $T=T'$ by $\forall w\,(\sigma_{T}(w)\Leftrightarrow\sigma_{T'}(w))$.