Let us consider the first-order logic extended with the least fixed point operator (FO+LFP). That is, together with the usual first-order formulas, we also have formulas of the form:


$$\mu X[\overline{y}] . \phi(X, \overline{y})$$


where $X$ (must occur positively in $\phi$) is a "predicate" variable of arity equal to the length of sequence of "parameters" $\overline{y}$. The semantic of this formula (in a given algebraic structure) is the least set $X^\*$ such that:


$$X^\*(\overline{y}) \Leftrightarrow \phi(X^\*, \overline{y})$$


For example, if $R$ is a binary relation symbol, then:


$$\mu X[y\_1, y\_2] . R(y\_1, y\_2) \vee (\exists\_z R(y\_1, z) \wedge X(z, y\_2))$$


defines the transitive closure of $R$.


If $A$ is an algebraic structure, let us write $\mathit{Th\_{lfp}}(A)$ for the first-order theory of $A$ extended with the least fixed point operator (i.e. the set of all FO+LFP sentences that are true in $A$).


Does there exist an algebraic structure $A$ such that both of the following hold:


* $\mathit{Th\_{lfp}}(A)$ is decidable
* FO+LFP is strictly more expressive than FO over $A$ (i.e. there is a FO+LFP formula that is not equivalent to FO formula over $A$)?


An example of a structure that satisfies the first property (but does not satisfy the second) is the structure of rational numbers with the natural ordering $\langle\mathcal{Q}, \leq\rangle$.


An example of a structure that satisfies the second property (but does not satisfy the first) is the structure of natural numbers with the natural ordering $\langle\mathcal{N}, \leq\rangle$.


One intuition is that there should be no such structure $A$ --- if $A$ defines arbitrary long well-founded orders, then the theory of $A$ should be undecidable; and if it does not define, then LFP seems to be pretty useless. 


Another intuition is that there might be such a structure, because the above intuition is difficult to formalize, thus may contain essential holes.



Expressive power of FO with $\mu$
Your intuition is right, and the way to formalize it is by Moschovakis's stage comparison theorem. 


Suppose $\psi$ is an (FO+LFP)-formula which starts with a $\mu$ operator. So $\psi$ has the form $\mu X[y].\phi(X,y)$. We can define the semantics of $\psi$ in a structure $M$ by transfinite induction. Set $X^\*\_0 = \emptyset$. Given $X^\*\_\alpha$, define $b\in X^\*\_{\alpha+1}$ if and only if $M\models \phi(X^\*\_\alpha,b)$. And for a limit ordinal $\beta$, define $X^\*\_\beta = \bigcup\_{\alpha<\beta} X^\*\_\alpha$. Then there is some ordinal $\xi$ such that $X^\*\_\xi = X^\*\_{\xi+1}$, and we can set $X^\* = X^\*\_\xi$. The least such $\xi$ is called the *closure ordinal* of $\psi$ in $M$. 


For $b\in X^\*$, we define the *$\psi$-stage* of $b$, $|b|\_\psi$, to be the least ordinal $\alpha$ such that $b\in X^\*\_\alpha$. Then the stage comparison theorem says that the relation $|b|\_\psi \leq |c|\_\psi$ is itself (FO+LFP)-definable.


Now for any structure $M$, we have two possibilities: 


* Case 1: For every (FO+LFP) formula $\psi$ which starts with a $\mu$ operator, there is a finite bound on the $\psi$-stages of elements of $X^\*$ in $M$. Equivalently, the closure ordinal of $\psi$ is finite. Then by unraveling the meaning of $\psi$, the $\mu X[y]$ operator can be removed. By induction on the complexity of the uses of $\mu$ in formulas, $\psi$ is equivalent to a first-order formula, and (FO+LFP) is no more expressive than FO on $M$.
* Case 2: There is an (FO+LFP) formula $\psi$ which starts with a $\mu$ operator, such that the closure ordinal $\xi$ of $\psi$ is infinite. Then, by stage comparison, the (FO+LFP)-theory of $M$ interprets $(\xi,\leq)$, and it's not hard to see that it interprets $(\mathbb{N},\leq,S)$ (defining the successor function $S$ from $\leq$ and defining the finite ordinals in $\xi$ as the closure of $0$ under $S$) and then $(\mathbb{N},\leq,S,+,\*)$ (carrying out the usual inductive definitions of $+$ from $S$ and $\*$ from $+$), and hence is undecidable.


You might be interested in the influential paper *[When is arithmetic possible?](https://doi.org/10.1016/0168-0072(90)90053-5)* by Gregory McColm. McColm conjectured that for any structure in Case 2 (which contains a formula $\psi$ with infinite closure ordinal), (FO+LFP) is strictly more expressive than FO. This conjecture was later refuted by Gurevich, Immerman, and Shelah in their paper *[McColm's conjecture](https://arxiv.org/abs/math/9411235)*.


