Can an axiom in FOL have recursion? 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.
 A: 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.)
