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

As usual, a class of structures here is closed under isomorphism and uses standard finite-structure encodings. First suppose $K$ is defined by $\exists R\varphi$, with $\varphi$ in partial fixed-point logic. Deterministically enumerate the polynomial-length encodings of $R$ and evaluate $\varphi$ on each expansion. PFP evaluation is in PSPACE even without a supplied order: a relation of fixed arity requires polynomially many bits, iteration has at most exponentially many states, and a polynomial-length counter suffices to stop after that many stages. If no consecutive stages agree before a repeat must have occurred, the partial fixed point is empty. Nested fixed points have fixed syntactic depth and can be evaluated with reused polynomial storage. Thus the encoding language of $K$ is in PSPACE.

Conversely, suppose that encoding language is decidable in PSPACE. Expand each structure by a freely chosen linear order $R$. On such ordered expansions, the assumed characterization gives a PFP sentence $\psi (R)$ deciding whether the reduct belongs to $K$. Since $K$ is isomorphism-invariant, the answer is independent of the particular chosen order. HenceThe expression inside the second-order quantifier is PFP, since the assertion that $R$ is a linear order is first-order. Every finite universe has a linear order. This proves both directions, using an existentially supplied order when the original signature has none. The construction is also the order-independent consequence of part (a), which shows that existential relation quantification does not increase PFP's power on an already ordered structure.