<p>People informally use the phrase "a logic for&nbsp;P" for the notion of a logic that captures&nbsp;P, which corresponds to Chen and Flum's definition of a "P-bounded logic for&nbsp;P". Essentially, this means that the logic defines exactly the polynomial-time properties of relational structures and formulae can be evaluated in polynomial time.<sup>1</sup> 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.</p>

<p>I think the confusion has arisen because Chen and Flum use the phrase "a logic for&nbsp;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&nbsp;$L_\leq$ is a logic for&nbsp;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$&nbsp;is $|A|$-invariant and there is no known way to do that in polynomial time.</p>

<p>$L_\leq$ defines all polytime properties because, by the result of Immerman and Vardi cited by Chen and Flum, LFP captures&nbsp;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&nbsp;$|A|$, which you can use as both for timestamps and to say "the $i$th character on the tape is&nbsp;$c$. You can then use a fixed-point formula that says, "If the configuration at time&nbsp;$t$ is&nbsp;$C_t$, then the configuration at time&nbsp;$t+1$ is&nbsp;$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&nbsp;$|A|$ numbers.</p>

<p>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&nbsp;P.  (But the formulas constructed above are, in fact, order-invariant across all structures.)</p>

<hr>

<p><sup>1</sup> More formally, for every formula&nbsp;$\phi$, there is a deterministic algorithm and a constant&nbsp;$k$ such that the algorithm decides whether $\cal{A}\vDash\phi$ in time at most&nbsp;$|A|^k$.</p>

CC BY-SA 3.0
2013-09-05T15:29:42.843Z
2013-09-05T15:29:42.843Z
David Richerby
<p>A least-fixed point (LFP) formula is $\leq m$-invariant iff f.a. structrues $\mathcal{A}$ with $|A| \leq m$ and all orderings $&lt;_1,&lt;_2$ on $A$ </p>

<p>$$(\mathcal{A},&lt;_1) \models_{LFP} \varphi \Leftrightarrow (\mathcal{A},&lt;_2) \models_{LFP} \varphi.$$</p>

<p>The logic $L_\leq$ is defined such that the modelling-relation is </p>

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

<p>A logic $L$ is efficiently $\operatorname{P}$-bounded for $\operatorname{P}$ if </p>

<ul>
<li>for each $Q \in \operatorname{P}$ there is a $\varphi \in L$ which axiomatizes $Q$</li>
<li>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</li>
</ul>

<p>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?</p>

CC BY-SA 3.0
2012-11-21T16:24:53.093Z
It seems to me that you are probably misreading the paper (Chen and Flum [2010](http://eccc.hpi-web.de/report/2010/008/) or [2011](http://doi.ieeecomputersociety.org/10.1109/LICS.2011.17)? 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
CC BY-SA 3.0
2012-11-21T16:28:04.137Z
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
CC BY-SA 3.0
2012-11-21T18:53:23.407Z
I'm refering to [ChenFlum2010 p. 325 bottom](http://eccc.hpi-web.de/report/2010/008/). Doesn't the paper state that LFP is a logic capturing $\operatorname{P}$ for the class of unordered structures?
Joachim
CC BY-SA 3.0
2012-11-22T05:09:27.577Z
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
CC BY-SA 3.0
2012-11-22T18:58:42.190Z
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
<cc.complexity-theory><lo.logic><descriptive-complexity>
Least fixed point logic is efficiently $\operatorname{P}$-bounded for $\operatorname{P} \Leftrightarrow L_\leq$ is a logic for $\operatorname{P}$
Joachim
# Least fixed point logic is efficiently $\operatorname{P}$-bounded for $\operatorname{P} \Leftrightarrow L_\leq$ is a logic for $\operatorname{P}$

(Asked by: username_0 on 2012-11-21)

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?

**Tags:** cc.complexity-theory, lo.logic, descriptive-complexity

> **Comments:**
> **username_1**: It seems to me that you are probably misreading the paper (Chen and Flum [2010](http://eccc.hpi-web.de/report/2010/008/) or [2011](http://doi.ieeecomputersociety.org/10.1109/LICS.2011.17)? 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.  
> **username_1**: 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.  
> **username_0**: I'm refering to [ChenFlum2010 p. 325 bottom](http://eccc.hpi-web.de/report/2010/008/). Doesn't the paper state that LFP is a logic capturing $\operatorname{P}$ for the class of unordered structures?  
> **username_1**: 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.  
> **username_0**: 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.  

---

## 1 answers

### Answer by username_2 on 2013-09-05. Score: 4 | Accepted answer

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


---

