Expressive power of FO with $\mu$

Question

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.

Answer 1

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.

Answer 2

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