Least fixed point logic is efficiently $\operatorname{P}$-bounded for $\operatorname{P} \Leftrightarrow L_\leq$ is a logic for $\operatorname{P}$

Question

A least-fixed point (LFP) formula is $\leq m$-invariant iff f.a. structrues $\mathcal{A}$ with $|A| \leq m$ and all orderings $<_1,<_2$ on $A$

$$(\mathcal{A},<_1) \models_{LFP} \varphi \Leftrightarrow (\mathcal{A},<_2) \models_{LFP} \varphi.$$

The logic $L_\leq$ is defined such that the modelling-relation is

$$ \mathcal{A} \models_{L_\leq} \varphi \Leftrightarrow \varphi \textrm{ is $\leq |A|$-invariant and } (\mathcal{A},<)\models_{LFP}\varphi \textrm{ for some} <.$$

A logic $L$ is efficiently $\operatorname{P}$-bounded for $\operatorname{P}$ if

• for each $Q \in \operatorname{P}$ there is a $\varphi \in L$ which axiomatizes $Q$
• for each $\varphi \in L$ there is polynomial $p$ such that the modelling relation $\mathcal{A} \models_L \varphi$ can be decided by an algorithm in $\leq p(\|\mathcal{A}\|)$ steps

A known result is that LFP is an efficiently $\operatorname{P}$-bound logic for $\operatorname{P}$ on the class of ordered structures. A paper states that one can easily deduce from the result that $L_\leq$ is a logic for $\operatorname{P}$. Any ideas how?

Answer 1

People informally use the phrase "a logic for P" for the notion of a logic that captures P, which corresponds to Chen and Flum's definition of a "P-bounded logic for P". Essentially, this means that the logic defines exactly the polynomial-time properties of relational structures and formulae can be evaluated in polynomial time.¹ Specifically, it's no use if your logic defines exactly the polytime properties but it takes exponential time to figure out whether a formula's true.

I think the confusion has arisen because Chen and Flum use the phrase "a logic for P" to mean just any logic that defines exactly the polytime properties of structures, without the requirement that formulae can be evaluated in polytime. The logic $L_\leq$ is a logic for P in this specific sense. Every polytime property is definable by a formula $\phi\in L_\leq$ but the semantics of the logic requires testing whether $\phi$ is $|A|$-invariant and there is no known way to do that in polynomial time.

$L_\leq$ defines all polytime properties because, by the result of Immerman and Vardi cited by Chen and Flum, LFP captures P on the class of ordered structures. More specifically, any ordering of the structure's universe lets you use tuples in $A^k$ to represent $k$-digit numbers in base $|A|$, which you can use as both for timestamps and to say "the $i$th character on the tape is $c$. You can then use a fixed-point formula that says, "If the configuration at time $t$ is $C_t$, then the configuration at time $t+1$ is $C_{t+1}$. The resulting formula doesn't depend on which ordering is chosen, so it's order-invariant, as required. Choosing a different ordering is just permuting the meaning of the digits in your base $|A|$ numbers.

Note that order-invariance in general is not decidable, which is why Chen and Flum restrict to order-invariance only on structures up to the size of the one we're evaluating the formula on. That's decidable but not known to be in P. (But the formulas constructed above are, in fact, order-invariant across all structures.)

---

¹ More formally, for every formula $\phi$, there is a deterministic algorithm and a constant $k$ such that the algorithm decides whether $\cal{A}\vDash\phi$ in time at most $|A|^k$.