= Solution
Fix a <partial fixed-point logic> formula $\phi(R,\mathbf x)$, with $R$ of arity $k$. On a finite ordered structure, an interpretation of $R$ is a bit string of length $n^k$. To decide whether some interpretation makes $\phi$ true at a given tuple, enumerate all these strings and evaluate $\phi$ for each. Evaluation uses <polynomial space> by the permitted characterization of PFP, and the enumerating counter also has polynomial length. Storage is reused between interpretations. Thus the resulting pointed-structure property is decidable in <PSPACE>.
Apply the assumed PFP characterization of PSPACE on ordered structures to this property. It gives a PFP formula $\psi(\mathbf x)$ such that
$$
\boxed{\psi(\mathbf x)\equiv\exists R\,\phi(R,\mathbf x)\quad\text{on finite ordered structures}.}
$$
To justify the formula version from a sentence characterization, temporarily name the tuple by finitely many new constants, apply the characterization in that expanded finite signature, and replace those constants by the free variables, renaming bound variables to avoid capture. This does not introduce a new order assumption: the input already interprets $<$ as a <linear order>. Multiple quantified relations are handled by repeated application.
Back to article page
