Logic capturing automorphism-invariant $\mathsf{AC^0}$ properties

Q1. Is there a logic that is computable in polynomial-time which contains all order-invariant properties computable in smaller classes like $\mathsf{AC^0}$ (or $\mathsf{TC^0}$)?

Motivation

As you probably know, finding a logic that captures order-invariant polynomial-time computable properties of graphs is one of the open problems (maybe the open problem) in descriptive complexity. A negative answer would imply $mathsf{P} \neq \mathsf{NP}$. On the other hand, a positive answer has interesting consequences also, the one that I find most interesting is existence of an optimal proof system. Roughly, we want to enumerate all polynomial-time computable properties of graphs using only polynomial-time machines that depends only on the graph (not on the labeling/coding, i.e. a machine in the enumeration returns the same answer for all automorphisms of the a graph)

It is conjectured that there is not such logic. (You can find a more precise formulation of the problem at the bottom of this post.)

It has been shown that some well-known logics that capture polynomial-time properties (not necessarily in an order invariant way) like $\mathsf{IFP}$ with order don't capture order-invariant polynomial-time computable properties (but they contain $\mathsf{P\text{-}complete}$ problems under $\mathsf{AC^0}$). More interestingly, $IFP$ cannot compute the parity of a graph. There are similar results for extensions of the logic like $IFP+Count$. On the other hand, we know that $\mathsf{\exists SO}$ captures order-invariant $\mathsf{NP}$ properties. It seem natural to first try to capture the $\mathsf{AC^0}$ properties of graphs before trying to capture graph properties in $\mathsf{P}$, specially in a situation that we know natural logics that contain $\mathsf{P\text{-}complete}$ problems w.r.t. usual $\mathsf{AC^0}$ reductions (which are not order-invariant) can not compute parity. (This might seem confusing at first, the problems are complete under reductions which are dependent on the particular labeling of the graph used. In fact, the question is equivalent to finding a problem which is $\mathsf{P\text{-}complete}$ under order-invariant reductions that are computable in polynomial time.)

A positive answer to original question implies a positive answer to Q1. Therefore a negative answer to Q1 implies a negative answer to the original question, which would imply $\mathsf{P} \neq \mathsf{NP}$.

Q2. Does a positive answer to Q1 have any interesting computational complexity implications?

Background:

(Yuri Gurevich, "Logic and the Challenge of Computer Science", 1988, pages 25-26)

Definition 1.14.

A logic $L$ is a pair $(SEN, SAT)$ satisfying the following requirements.

• $SEN$ is a function that associates with every finite signature $\sigma$ a recursive set $SEN(σ)$ whose elements are called $L$-sentences of signature $\sigma$.

• $SAT$ is a function that associates with every finite signature $\sigma$ a recursive subset $SAT(\sigma)$ of $$\{(S, \varphi): S \text{ is a finite first-order } \sigma\text{-structure and } \varphi \text{ is an } L \text{-sentence of signature } \sigma \}$$ such that if structures $S$ and $S'$ are isomorphic and $(S, \varphi)$ belongs to $SAT(\sigma)$ then $(S', \varphi)$ belongs to $SAT(\sigma)$ as well. If $(S, \varphi)$ belongs to some $SAT(\sigma)$, we say that $S$ satisfies $\varphi$.

Definition 1.15

If $L$ is a logic and $\varphi$ is an $L$-sentence of some signature $\sigma$, then $MOD(\varphi)$ be the set of $\sigma$-structures satisfying $\varphi$.

Definition 1.16

A logic $L$ captures polynomial time if:

1. For every $L$-sentence $\varphi$, the class $MOD(\varphi)$ is polynomial time recognizable; moreover, for every $\sigma$ there is a Turing machine $M$ that, given an $L$-sentence $\varphi$ of signature $\sigma$, produces a polynomial time bounded Turing machine $M(\varphi)$ that recognizes $MOD(\varphi)$.

2. For every polynomial time recognizable class $K$ of structures of some signature $\sigma$, if $K$ is closed under isomorphisms then there is an $L$-sentence $\varphi$ of signature $\sigma$ such that $MOD(\varphi) = K$.

Remark

In this section, a polynomial time bounded Turing machine can be viewed as a pair $(T,p)$ where $T$ is a Turing machine and $p$ is a polynomial with integer coefficients; $(T,p)$ accepts an input $w$ of $T$ if $T$ accepts $w$ within $p(|w|)$ steps.

Conjecture

There is no logic that captures polynomial time.

References:

For more information about the original about finding a logic for $\mathsf{P}$ check the slides of lectures by Anuj Dawar and references provided there.