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.