About proofs in descriptive complexity
Your intuition is correct, though it's probably more useful to think of the statement "[Logic] = [Complexity Class]" as "A property of relational structures can be decided in [Complexity Class] if, and only if, it is definable in [Logic]."

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$ &mdash; that's the definition of what it means for $M(\cal{A})$ to be&nbsp;$1$. The property of $\cal{A}$ that the formula verifies is "$\cal{A}$ is a structure accepted by&nbsp;$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&nbsp;$n^k$, we can index each time step of its computation by a $k$-digit number in base&nbsp;$n$ and likewise each used cell on its tape (in $n^k$&nbsp;steps, it can't use more than $n^k$&nbsp;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&nbsp;$t$, cell&nbsp;$i$ of the tape contains character&nbsp;$c$", "At time&nbsp;$t$, the head is at position&nbsp;$p$", "At time&nbsp;$t$, the machine is in state&nbsp;$s$". Now, you write a formula that says:


at time&nbsp;$0$, the tape contains the coding of&nbsp;$\cal{A}$, the head is at position&nbsp;$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&nbsp;$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&nbsp;$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&nbsp;$S_i$ contains the times at which the machine is in state&nbsp;$s_i$. The tape symbols can be coded similarly.