<blockquote>
<p>But what would be the issue if we extended IFP to just have an order
and made it that a structure satisfies a formula if it satisfies for
an arbitrary order?</p>
</blockquote>
<p>If done this way, it is difficult to see why the data complexity of the resulting logic would be in PTIME. Indeed, there are exponentially many linear orders and a naïve brute force algorithm would also take an exponential amount of time to verify that a given IFP formula is satisfied for all linear orders.</p>
<p>Instead of doing the above, another natural option would be to extend IFP with a linear order and restrict the syntax of the resulting logic as follows: we only take sentences which are order-invariant. The problem here is that the resulting logic will have an undecidable syntax (this is proved in e.g. the Finite Model Theory book of Ebbinghaus and Flum).</p>

CC BY-SA 4.0
2024-04-21T14:20:57.030Z
2024-04-21T14:20:57.030Z
Reijo Jaakkola
<p>My interpretation of your question is something along the lines of, &quot;why <em>should</em> we care whether there is a logic that captures PTIME?&quot; This is a fair question: there are good reasons for caring about a logic for PTIME, but often papers or talks in finite model theory will take interest in it as given. I will try to avoid <em>a posteriori</em> justifications like &quot;if we find a logic for PTIME then such-and-such will happen&quot; and focus on why we might care from first principles.</p>
<p>PTIME is, of course, a family of queries, i.e., a set of sets of objects (sometimes called a <em>pointclass</em>). Once we have a robust family of queries, that alone is enough motivation (for some) to characterize it logically, i.e., in terms of definability by some syntactic objects.
However, in my opinion, what makes this problem really interesting is that there are two things we might want out of a &quot;logical characterization,&quot; and while we can get one or the other we can't seem to get both simultaneously.</p>
<p>One, we want a logic to be <em>parameterized by an arbitrary signature.</em> For example, the first-order theory of arithmetic is not a totally different beast from the first-order theory of graphs, but is a single instance of &quot;first order logic&quot; parameterized by two different signatures.</p>
<p>Secondly, we want to have a logic to be syntactically well-behaved, i.e., have at the minimum a decidable syntax, and ideally something much simpler, e.g., a context-free syntax with a nice, compositional semantics.</p>
<p>If we drop the requirement that logical characterization be parameterized by an arbitrary signature, we recover logical characterizations of PTIME, e.g., by LFP queries. But these only capture PTIME queries over ordered structures. There are more sophisticated approaches (e.g., &quot;choiceless PTIME&quot;), but even these fail to capture PTIME over all classes of finite structures. If we drop the requirement of syntactic good behavior, we recover logical chacterizations of PTIME, e.g., by order-invariant LFP queries. But these no longer have a decidable syntax.</p>
<p>I think that the inability to satisfy these two desiderata simultaneously is actually what makes the &quot;logic for PTIME&quot; question so interesting---the problem really does fight back, in other words.</p>

CC BY-SA 4.0
2024-04-17T06:13:06.033Z
*No* logic over finite structures has a "reasonable proof theory" (which, as a bare minimum, I take to mean that the proof system is recursively axiomatized). Already the baseline logic FO is $\Pi_1$-complete over finite structures.
Emil Jeřábek
CC BY-SA 4.0
2024-04-17T08:34:12.773Z
(Note that it gets even worse for proper extensions of FO, as they either do not have a reasonable generalization to infinite structures at all, or if they do, they normally do not have a complete proof system for validity in all structures. For a general statement to that effect, Lindström’s theorem guarantees that no proper extension of FO satisfying the countable downward Löwenheim–Skolem theorem is recursively axiomatizable.)
Emil Jeřábek
CC BY-SA 4.0
2024-04-25T20:12:47.890Z
What would you call the property of e.g., having a decidable syntax?
Siddharth
CC BY-SA 4.0
2024-04-26T05:32:41.977Z
I’m sorry, but I don’t understand your question. What do you mean by how would I call it? I’d call it “decidable syntax”, shouldn’t I?
Emil Jeřábek
CC BY-SA 4.0
2024-04-26T07:06:24.060Z
If you are somehow suggesting that the “decidable syntax” property makes proof theory, then no, not at all. This is just a basic property of the *language*, that we can recognize whether something is a *formula*. It does not in any way involve a proof system that would characterize the formulas that are *logically valid* (= theorems, as you put it).
Emil Jeřábek
CC BY-SA 4.0
2024-04-26T07:14:19.270Z
Your claim in the answer that one of the requirements for a logic for polynomial time is that the set of theorems should be recursively enumerable is explicitly false. No reasonable logic can have this property as it fails already for FO.
Emil Jeřábek
CC BY-SA 4.0
2024-04-26T09:06:06.033Z
(Scratch “reasonable”. Any logic for PTIME has a $\Pi_1$-complete set of theorems, period. This does not require translation from FO or Trakhtenbrot’s theorem at all: it follows easily directly from the fact that there is a poly-time predicate $P(x,y)$ such that $\forall y\,P(x,y)$ is $\Pi_1$-complete.)
Emil Jeřábek
CC BY-SA 4.0
2024-05-02T02:41:53.710Z
Thanks for this. I'll think about this, edit or delete my answer, and at least remove language concerning "reasonable proof theory."
Siddharth
CC BY-SA 4.0
2024-04-17T04:05:04.737Z
2024-05-22T18:23:02.663Z
2024-05-22T18:23:02.663Z
Siddharth
<p>If you treat an integer in terms of, say, it's binary expansion, and the FO structure you use for that is a single unary relation on a set of size n (indicating which bits of your length-n string are 1), the order on [n] affects what number you're talking about and therefore the output of the problem. Eg primality. An issue here is how the order interacts with other predicates (in this case multiplication of binary-encoded integers).</p>
<p>(I agree that most &quot;natural&quot; graph problems are invariant under change of order, or equivalently, isomorphism.)</p>

CC BY-SA 4.0
2024-04-17T01:11:12.330Z
2024-04-17T01:11:12.330Z
Joshua Grochow
<p>As I'm reading on the question of a logic for PTIME and in particular about CPT and its variants, whilst things make sense and I follow along, I came to realise that I don't fundamentally understand why choice/order causes an issue. It's been repeated in the expositions of many papers on the topic that a logic for PTIME should be choiceless (over arbitrary sets) and, morally, sure, for all intents and purposes an order over the input structure is an externality and one would hope not to rely on it, but what if you do?</p>
<p>PTIME algorithms make us of choice all the time and can do so do to the inherent order within the encoding. But these don't care what the order is (as if they depended on a specific order the algorithm would be incorrect for that decision problem). Of course, by Immerman-Vardi we have that IFP captures PTIME on structures that already come with an order. But what would be the issue if we extended IFP to just have an order and made it that a structure satisfies a formula if it satisfies for an arbitrary order? Or indeed just adding arbitrary choice to CPT.</p>
<p>My best guess is that my base assumption that all decision problems are order-invariant (and that function problems produce isomorphic outputs on isomorphic inputs) is wrong, but this feels very counter-intuitive if it were the case.</p>

<cc.complexity-theory><lo.logic><time-complexity><descriptive-complexity><finite-model-theory>
Why is order/choice an issue for a logic for PTIME
Matei Chesa
# Why is order/choice an issue for a logic for PTIME

(Asked by: username_0 on 2024-04-17)

As I'm reading on the question of a logic for PTIME and in particular about CPT and its variants, whilst things make sense and I follow along, I came to realise that I don't fundamentally understand why choice/order causes an issue. It's been repeated in the expositions of many papers on the topic that a logic for PTIME should be choiceless (over arbitrary sets) and, morally, sure, for all intents and purposes an order over the input structure is an externality and one would hope not to rely on it, but what if you do?

PTIME algorithms make us of choice all the time and can do so do to the inherent order within the encoding. But these don't care what the order is (as if they depended on a specific order the algorithm would be incorrect for that decision problem). Of course, by Immerman-Vardi we have that IFP captures PTIME on structures that already come with an order. But what would be the issue if we extended IFP to just have an order and made it that a structure satisfies a formula if it satisfies for an arbitrary order? Or indeed just adding arbitrary choice to CPT.

My best guess is that my base assumption that all decision problems are order-invariant (and that function problems produce isomorphic outputs on isomorphic inputs) is wrong, but this feels very counter-intuitive if it were the case.

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


---

## 3 answers

### Answer by username_1 on 2024-04-21. Score: 3

> But what would be the issue if we extended IFP to just have an order
> and made it that a structure satisfies a formula if it satisfies for
> an arbitrary order?

If done this way, it is difficult to see why the data complexity of the resulting logic would be in PTIME. Indeed, there are exponentially many linear orders and a naïve brute force algorithm would also take an exponential amount of time to verify that a given IFP formula is satisfied for all linear orders.

Instead of doing the above, another natural option would be to extend IFP with a linear order and restrict the syntax of the resulting logic as follows: we only take sentences which are order-invariant. The problem here is that the resulting logic will have an undecidable syntax (this is proved in e.g. the Finite Model Theory book of Ebbinghaus and Flum).


---

### Answer by username_2 on 2024-04-17. Score: 2

My interpretation of your question is something along the lines of, "why *should* we care whether there is a logic that captures PTIME?" This is a fair question: there are good reasons for caring about a logic for PTIME, but often papers or talks in finite model theory will take interest in it as given. I will try to avoid *a posteriori* justifications like "if we find a logic for PTIME then such-and-such will happen" and focus on why we might care from first principles.

PTIME is, of course, a family of queries, i.e., a set of sets of objects (sometimes called a *pointclass*). Once we have a robust family of queries, that alone is enough motivation (for some) to characterize it logically, i.e., in terms of definability by some syntactic objects.
However, in my opinion, what makes this problem really interesting is that there are two things we might want out of a "logical characterization," and while we can get one or the other we can't seem to get both simultaneously.

One, we want a logic to be *parameterized by an arbitrary signature.* For example, the first-order theory of arithmetic is not a totally different beast from the first-order theory of graphs, but is a single instance of "first order logic" parameterized by two different signatures.

Secondly, we want to have a logic to be syntactically well-behaved, i.e., have at the minimum a decidable syntax, and ideally something much simpler, e.g., a context-free syntax with a nice, compositional semantics.

If we drop the requirement that logical characterization be parameterized by an arbitrary signature, we recover logical characterizations of PTIME, e.g., by LFP queries. But these only capture PTIME queries over ordered structures. There are more sophisticated approaches (e.g., "choiceless PTIME"), but even these fail to capture PTIME over all classes of finite structures. If we drop the requirement of syntactic good behavior, we recover logical chacterizations of PTIME, e.g., by order-invariant LFP queries. But these no longer have a decidable syntax.

I think that the inability to satisfy these two desiderata simultaneously is actually what makes the "logic for PTIME" question so interesting---the problem really does fight back, in other words.

> **Comments:**
> **username_3**: *No* logic over finite structures has a "reasonable proof theory" (which, as a bare minimum, I take to mean that the proof system is recursively axiomatized). Already the baseline logic FO is $\Pi_1$-complete over finite structures.  
> **username_3**: (Note that it gets even worse for proper extensions of FO, as they either do not have a reasonable generalization to infinite structures at all, or if they do, they normally do not have a complete proof system for validity in all structures. For a general statement to that effect, Lindström’s theorem guarantees that no proper extension of FO satisfying the countable downward Löwenheim–Skolem theorem is recursively axiomatizable.)  
> **username_2**: What would you call the property of e.g., having a decidable syntax?  
> **username_3**: I’m sorry, but I don’t understand your question. What do you mean by how would I call it? I’d call it “decidable syntax”, shouldn’t I?  
> **username_3**: If you are somehow suggesting that the “decidable syntax” property makes proof theory, then no, not at all. This is just a basic property of the *language*, that we can recognize whether something is a *formula*. It does not in any way involve a proof system that would characterize the formulas that are *logically valid* (= theorems, as you put it).  
> **username_3**: Your claim in the answer that one of the requirements for a logic for polynomial time is that the set of theorems should be recursively enumerable is explicitly false. No reasonable logic can have this property as it fails already for FO.  
> **username_3**: (Scratch “reasonable”. Any logic for PTIME has a $\Pi_1$-complete set of theorems, period. This does not require translation from FO or Trakhtenbrot’s theorem at all: it follows easily directly from the fact that there is a poly-time predicate $P(x,y)$ such that $\forall y\,P(x,y)$ is $\Pi_1$-complete.)  
> **username_2**: Thanks for this. I'll think about this, edit or delete my answer, and at least remove language concerning "reasonable proof theory."  

---

### Answer by username_4 on 2024-04-17. Score: 1

If you treat an integer in terms of, say, it's binary expansion, and the FO structure you use for that is a single unary relation on a set of size n (indicating which bits of your length-n string are 1), the order on [n] affects what number you're talking about and therefore the output of the problem. Eg primality. An issue here is how the order interacts with other predicates (in this case multiplication of binary-encoded integers).

(I agree that most "natural" graph problems are invariant under change of order, or equivalently, isomorphism.)


---

