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?
 A: 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.
A: In many such cases, at least in general mathematics (not in first-order logic, as you observed), such constructions come up often in practice.  In this case, it would typically be stated something like: let $\psi(x, y)$ be a relation on the universe $U$ of discourse.  Then we define $\phi(x, y)$ to be the smallest relation on $U$ such that $\psi(x, y) \rightarrow \phi(x, y)$ for all $x, y$, and such that $\phi(x, z) \wedge \phi(z, y) \rightarrow \phi(x, y)$ for all $x, y, z$.  (In this particular case, what you get is exactly what's called the transitive closure of $\psi$.)
One common way to define this $\phi$ is to take the intersection $\Phi_0$ of all subsets of $U \times U$ which contain $\{ (x, y) \mid \psi(x, y) \}$ and which are transitive, and then define $\phi(x, y)$ to mean $(x, y) \in \Phi_0$.  Another way to state this in a second-order logic type of language is: $$\phi(x, y) := \forall R, [(\forall a, b, \psi(a, b) \rightarrow R(a, b)) \wedge (\forall a, b, c, R(a, c) \wedge R(c, b) \rightarrow R(a, b))] \rightarrow R(x, y).$$
(Here $R$ ranges over all binary relations on the universe of discourse $U$.)
It might be interesting to note that the foundational system of Coq, Calculus of Constructions, treats "constructions" like this as being a fundamental object of the system.  For example, in Coq, you can define the transitive closure of a relation by:
Section TC.

Variables (A : Type) (R : A -> A -> Prop).

Inductive TC : A -> A -> Prop :=
| TC_base : forall x y : A, R x y -> TC x y
| TC_trans : forall x y z : A, TC x z -> TC z y -> TC x y.

End TC.


Do note, however, that there must be some restrictions on the types of such "recursive" definitions that are allowed, or you can easily run into contradictions.  For example, if you tried to recursively define $\phi$ as meaning $\lnot \phi$, then the only way $\phi$ could be true is if $\lnot \phi$ is true, so $\phi$ is also false and you get a contradiction.  On the other hand, if $\phi$ were false, then $\lnot \phi$ would be true, so by the recursive definition, this would imply $\phi$ would be true, again giving a contradiction.  (This example is very closely related to the "liar paradox".)
Usually, the cases where you can get a "recursive" definition like this to be valid and to act as expected would be where the conditions are of the type of specifying "generators" (e.g. $\psi(x, y) \rightarrow \phi(x, y)$) and "closure conditions" (e.g. $\phi(x, z) \wedge \phi(z, y) \rightarrow \phi(x, y)$).  And in some treatments, the "generators" type of condition will be treated as a special case of the "closure condition" type of condition but where there are no "input" hypotheses involving the condition you're defining, only the "output" involves it.
(In the case of Calculus of Constructions, the restriction which maintains consistency is a "strict positivity" syntactic restriction on where the object being defined is allowed to appear in the "input hypotheses".)
