Immerman (1999, p. 61) describes Theorem 4.3 as “increas[ing] our intuition that polynomial time is a class whose fundamental nature goes beyond the machine models with which it is usually defined”.  Taken in conjunction with Theorem 4.2 it also provides a logical reformulation of the \(\textbf{P} \neq \textbf{NP}?\) problem itself – i.e. \(\textbf{P} \neq \textbf{NP}\) if and only if there exists a class of ordered structures definable in existential second-order logic which is not definable by a formula of \(\textsf{FO}(\texttt{LFP})\).