Recursive formulae in logic? Given domain $A$ and variables $x,y,z$, we could define the following "recursive formula":
$$\phi(x,y): \psi(x,y) \lor \exists z,[\phi(x,z)\land\phi (z,y)]\tag {*}$$
Where $\psi(x,y)$ is a first-order formula.
Clearly, this formula is not logically equivalent to any formula in first order logic (defined over the same domain). However, if we include into the domain of discourse the set $S^A:\mathbb N\to A$ of sequences over $A$, then I think we can restate it as: 
$$\phi(x,y):\exists s:S^A,\exists N,\forall n,[0<n<N\to \psi(s_n,s_{n+1})]$$
What is the status of a formula like $(*)$ ? Are recursive formula like this accepted  as legitimate by logicians/mathematicians? Is every such formula equivalent to a formula in second order logic or in first order logic with an expanded domain?

First-order logic on its own is completely neutral about axioms that might be interpreted as recursive definitions: as a simple example, $\forall x(f(x) = f(x))$ is trivially true in any first-order theory even though it will lead to a non-terminating function if you treat it as a definition in a functional programming language.
In your example, if $\psi(x, y)$ is a formula in the language of a first-order theory $\cal T$, then there is no reason why we should not define a new theory $\cal T'$ that extends $\cal T$ by adding a new predicate symbol $\phi$ and a new axiom:
$$\forall x \forall y(\phi(x,y) \Leftrightarrow \psi(x,y) \lor \exists z[\phi(x,z)\land\phi (z,y)])$$
$\cal T'$ is consistent if $\cal T$ is: if you interpret $\phi(x, y)$ as identically true, you satisfy the new axiom.
