Lately, I've been interested in playing around with seeing how powerful a set theory can be with a single axiom. A while, ago I made this naive axiom schema; dubbed the axiom schema of propagation (ASP).
$$\forall X \forall Y \exists Z(\Lambda(X,Y,Z))$$
Where $\Lambda$ is a logical condition recursively defined (informally) as
$$\Lambda(X,Y,Z):=(X=\emptyset\iff Z=\{Y\})\wedge\forall x\bigg[\Big(x\in X \implies \exists y(y\in Z \wedge\Lambda(x,Y,y))\Big) \wedge
\Big(x\in Z \implies \exists z(z\in X \implies\Lambda(z,Y,x))\Big)
\bigg]$$
Monstrosity aside, I've found that pairing this with extensionality & the empty set alone is quite powerful. Despite $\Lambda$ being in the definition of itself, evaluating $\Lambda$ for sets of finite rank eventually halts when the left side of implications are false; meaning the right sides (that include the recursive part) needn't be deduced.
Is such a recursive definition allowed/conventional?
If you're curious, essentially what I've attempted in this axiom schema is that for a given set $X$, for every point within all "levels" of $X$ where there is an empty set, I insert a given $Y$ 'inside' such empty sets. This new set is $Z$. Here is an example of the process, shown graphically as rooted identity trees.
Given $X$ and $Y$, this $Z$ is the unique set that satisfies $\Lambda(X,Y,Z)$
Note: I say schema because the version I was later working with replaces $(X=\emptyset)$ with an arbitrary condition $\phi(X)$, similar to that found in specification. Without that replacement this set theory only gives rise to singletons. I've left it out for brevity.
Best Answer
No, this sort of recursion is not allowed in first-order logic. Remember that in general a first-order formula, thought of as a query, has to "work" (= make sense and have an answer) on every element of every structure. Recursive formulas of the type in the OP run into ill-foundedness problems in general - e.g. supposing $a=\{a\}$, should we have $\Lambda(\{a\},\{a\},\{a\})$ be true or false? More relevantly, suppose $M$ is an illfounded model of $\mathsf{ZFC}$; for $a$ not in the illfounded part of $M$, how should we understand $\Lambda(a,-,-)$?
That said, in the presence of a weak fragment of $\mathsf{ZFC}$ we can make sense of your principle in a first-order way. Specifically, we first whip up a set-theoretic implementation of basic graph theory, with which we can easily talk about the result of substituting a given tree for each leaf in another tree. Note that this is totally recursion-free: basically, we talk about a particular graph on a subset of the Cartesian product of the vertex sets of two given graphs. Then we prove that we can conflate sets with certain types of trees, namely the (internally) well-founded extensional ones; this requires Replacement, since basically what we're doing is going through the transitive closure. Combining these we get a purely first-order sentence which - again, in the presence of this weak axiomatic background - expresses what you're looking for. (And in fact this sentence is outright provable in this fragment.)