# Are recursive Horn clauses first order?

My understanding is that recursive definitions are considered second-order since they require the fixpoint operator in order to be formulated as "true" definitions. This is even though they contain no higher order quantifiers eg.

times(x,s(y)) = plus(x,times(x,y))
times(x,0) = 0


needs to be written as times = \mu x. F(x) for some F, and the fixpoint operator is second order. I believe the same is true for recursive Horn clauses. But then why is a Prolog program considered first order, since it typically contains many recursive rules?

times(_, 0, 0).

is not the definition of a recursive function, but just two logical formulas, written fully as $$\begin{gather*} \forall x .\, \mathtt{times}(x, 0, 0), \\ \forall x, y, w, z .\, \mathtt{times}(x,y,z) \land \mathtt{plus}(x,z,w) \Rightarrow \mathtt{times}(x,S(y),w). \end{gather*}$$ Here $$\mathtt{times}$$ and $$\mathtt{plus}$$ are ternary relation symbols, $$0$$ is a constant, and $$\mathtt{S}$$ is a unary function symbol.
As for the necessity of using the fixpoint $$\mu$$ operator for recursive definitions, there is no such necessity. We can directly define first-order functions using a schema that allows self reference. Such a schema may be translated to an application of $$\mu$$, but it does not have to be. One can explain it directly. For instance, primitive recursive functions are defined such a schema, without any fixed point operator.