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?

  • 2
    $\begingroup$ 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. $\endgroup$
    – Kaveh
    Commented Nov 21, 2012 at 16:24
  • 1
    $\begingroup$ 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. $\endgroup$
    – Kaveh
    Commented Nov 21, 2012 at 16:28
  • $\begingroup$ 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? $\endgroup$
    – Joachim
    Commented Nov 21, 2012 at 18:53
  • 1
    $\begingroup$ 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. $\endgroup$
    – Kaveh
    Commented Nov 22, 2012 at 5:09
  • $\begingroup$ 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. $\endgroup$
    – Joachim
    Commented Nov 22, 2012 at 18:58

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

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


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.