# Why does IFP< not capture PTIME?

Consider the logic whose $\tau$-sentences are the sentences in $IFP(\tau \cup \{<\})$, and the satisfaction relation is given by $\mathfrak{A} \models^* \phi$ if $(\mathfrak{A}, <) \models \phi$ for every ordering $<$ of $\mathfrak{A}$. Why does this logic not capture PTIME? I suppose that it is because a machine cannot quickly determine whether whether all linear orderings satisfy the sentence, but is there a formal proof of this?

The definition of a logic $\mathcal{L}$ capturing a complexity class $\mathcal{C}$ requires that the problem of evaluating $\mathcal{L}$-formulas is itself in $\mathcal{C}$. However, evaluating formulas of the logic you suggest is coNP-complete (in fact, even without the fixed points).
• Membership. You can determine that $\mathfrak{A}\nvDash^* \varphi$ by guessing a linear order and checking that it makes the formula false.
• Completeness. A graph is non-3-colourable if, and only if, every linear order $\leq$ on its vertices satisfies the property that, for every pair $x$, $y$ of vertices, at least one of the the vertex sets $\{z\mid z<x\}$, $\{z\mid x\leq z<y\}$ and $\{z\mid y\leq z\}$ contains an edge. This property is definable without using the fixed point operator.
You could try to get around this by defining the formulas of the logic to be only the order-invariant $\mathrm{IFP}(\tau+<)$ formulas, i.e., those that are true for some linear order if, and only if, they are true for all. But it's an easy consequence of Trakhtenbrot's theorem that this class of formulas is undecidable.
This semantic is powerful enough to embed co-$NP$-complete problems. For instance, on an input graph $G$, you can design $\phi$ to say "the even elements according to $<$ do not form a clique".
Then, under your semantic, $G\models^* \phi$ iff $G$ does not have a clique which is half the size of $G$. It is not hard to verify that this is a co-$NP$-complete problem, so unless $P=NP$, your logic is more powerful than $P$.