Past exam of the mathematics course of the University of Cambridge / 2002 / iii / Paper 23 / 8 / a / Solution

Fix a partial fixed-point logic formula $\varphi (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 $\varphi$ true at a given tuple, enumerate all these strings and evaluate $\varphi$ 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 thatTo 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.