# About proofs in descriptive complexity

In descriptive complexity, we have theorems that look like $\mathrm{ESO} = \mathrm{NP}$ or "on linearly ordered structures, $FO(LFP) = P$", but I don't really understand the proofs of those.

For the latter, the intuitive equality really means that the statement "$\mathcal A\models \varphi$" can be verified to be true on a linearly ordered structure $\mathcal A$ in time $n^k$ iff $\varphi$ is expressible in some fixpoint logic. The right-to-left inclusion then reads $\forall M\; \mathrm{polytime \;TM}, \exists \varphi\in\mathrm{FO(LFP)} \quad \left[\mathcal A \models \varphi \Leftrightarrow M(\mathcal A) = 1\right]$.

The proof I have been taught in class for the right-to-left inclusion goes as follows: from a Turing machine M (with set of states $S$), we build a formula on the language $\{T_0,T_1\} \cup \{H_i : i\in S\}$, where all relations are of arity $2k$. This formula says that the structure it's being evaluated on is a correct computation of $M$ which ends in an accepting state. How does this prove the theorem? Of course, there is a bijection between accepting computations of $M$ and structures $\mathcal A$ s.t $M(\mathcal A) = 1$, but the statement of the theorem doesn't mention this bijection. In my opinion, the formula $\varphi$ that we create should really check properties of $\mathcal A$, and not properties of the computation of $M$ on $\mathcal A$... Where is my mistake? Am I overthinking this?

As for the proof, I think you're overthinking it. There's not just a bijection between accepting computations and structures $\cal{A}$ such that $M(\cal{A})=1$ — that's the definition of what it means for $M(\cal{A})$ to be $1$. The property of $\cal{A}$ that the formula verifies is "$\cal{A}$ is a structure accepted by $M$." There's really no difference between the statements (for example), "$\cal{A}$ is a connected graph", "$\cal{A}$ satisfies this formula that defines connectivity", "$\cal{A}$ is accepted by this Turing machine" and "this Turing machine accepts $\cal{A}$."
Perhaps it would help to give some intuition about how the proof works. The point about the linear order is that it lets us use the universe of the structure as digits, to write numbers in base $n=|\cal{A}|$. Since the machine we're dealing with runs in time $n^k$, we can index each time step of its computation by a $k$-digit number in base $n$ and likewise each used cell on its tape (in $n^k$ steps, it can't use more than $n^k$ tape cells). You can also use base-$n$ numbers (of fixed length) to represent the states of the Turing machine and the characters in its alphabet. You use this to build up relations that say things like, "At time $t$, cell $i$ of the tape contains character $c$", "At time $t$, the head is at position $p$", "At time $t$, the machine is in state $s$". Now, you write a formula that says:
• at time $0$, the tape contains the coding of $\cal{A}$, the head is at position $0$ (and the head is not anywhere else) and the machine is in its start state (and not in any other state) AND
• if, at time $t$, the machine is in some configuration, then the configuration at time $t+1$ is what the definition of the machine says it should be AND
• at some time $t$, the machine is in an accepting state.
Note that there are various different ways of coding the Turing machine's configuration in relations. For example, since there are only a fixed, finite number of machine states $s_1, \dots, s_\ell$, you could use $k$-ary relations $S_1, \dots, S_\ell$ such that each $S_i$ contains the times at which the machine is in state $s_i$. The tape symbols can be coded similarly.