On Levy's formal definition of class terms I've been reading Levy's Basic Set Theory and it has recently been drawn to my attention a certain problem with Levy's definition of formulas and terms in his extended language (section I.4.1) (well, maybe not a problem, more like a gap). In particular, he defines atomic formulas as those formulas formed from class terms and class or set variables by means of equality and membership, and then defines class terms as terms of the form $\{x \; | \; \Phi(x)\}$, where $\Phi(x)$ is an arbitrary formula. But this means that we need the definition of formula in order to define terms and we need the definition of terms in order to define formulas. It seems that this can be solved by a simultaneous recursion on terms and formulas, but I can't quite see how to get it done. Any help?

In first-order logic, terms are defined inductively (recursively) as a variable or by concatenating function symbols and terms. E.g: if $f,g$ are functions of arity 1 and $x$ is a variable,  $gfx$ is a term, because $x$ is a term and so are the concatenations $fx$ and $gfx$.
Several axiomatic approaches to set theory emphasise the fact that their only non-logical symbol is the predicate $\in$. As it follows, in the notation $\{x \mid \phi\}$ (or $\phi(x)$ to stress that $\phi$ says something about $x$),  to build  the class formula $\phi$, variables and '$\in$' suffice; and you can build a number of classes such as:
$$\{x \mid x \not \in x \}$$
or
$$\{x \mid x \in y \}$$
Of course, once you have defined class terms, you could recursively use them in the definition of class formulae, for example:
$$\{x \mid x \in \{x \mid x\in z \} \}$$
Therefore, terms can be variables or class terms, and class formulae can have variables only or class terms too.
NB: I am not an expert/professional
