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.


3 Answers 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).


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.

  • 5
    $\begingroup$ 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. $\endgroup$ Apr 17 at 6:13
  • $\begingroup$ (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.) $\endgroup$ Apr 17 at 8:34
  • $\begingroup$ What would you call the property of e.g., having a decidable syntax? $\endgroup$
    – Siddharth
    Apr 25 at 20:12
  • $\begingroup$ 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? $\endgroup$ Apr 26 at 5:32
  • 1
    $\begingroup$ 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). $\endgroup$ Apr 26 at 7:06

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


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.