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

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?

-
It seems to me that you are probably misreading the paper (Chen and Flum 2010 or 2011? it is always a good idea to include a link to the paper when asking a question about it). It is not known if there is a logic capturing invariant polynomial time queries, the result is a conditional result. –  Kaveh Nov 21 '12 at 16:24
Btw, your post is really difficult to parse, e.g. "$P$-bound for $P$" and "$Q \in P$". Please use fonts similar to those used in the paper to make the post more readable. –  Kaveh Nov 21 '12 at 16:28
I'm refering to ChenFlum2010 p. 325 bottom. Doesn't the paper state that LFP is a logic capturing $\operatorname{P}$ for the class of unordered structures? –  joachim Nov 21 '12 at 18:53
The linked paper and its revision don't have page 325. This is a major open problem in descriptive complexity as far as I know, their result is conditional. –  Kaveh Nov 22 '12 at 5:09
I'm sorry. I had different version of the paper. The reference is on page 5 in the upper half. Immerman, Vardi is used as a source. –  joachim Nov 22 '12 at 18:58

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.
1 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$.