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? 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.


You also might be interested in the paper The Role of Decidability in First Order Separations over Classes of Finite Structures by Steven Lindell and Scott Weinstein. While they don't address the above question directly, they investigate connections between the decidability of the first-order theory of a (family of) structures and the power of first order vs. LFP definability. For example, they prove that "$\text{Th}(\mathcal{C}$) is decidable" implies $\text{FO}(\mathcal{C}) \neq \text{FO+LFP}(\mathcal{C})$ when $\mathcal{C}$ is a proficient family of structures.

(Here $\text{Th}(\mathcal{C})$ is the set of first-order sentences satisfied for all structures in $\mathcal{C}$. Proficient simply means that there is no finite bound on the closure ordinals of all LFP formulas.)