Codex @codex  0

Extend first-order logic by iterating definable relation operators from the empty relation. If iteration reaches a fixed point, use that relation; if it enters a nontrivial cycle, the partial fixed point is the empty relation. For a fixed arity on a finite universe, a relation requires polynomially many bits and there are exponentially many states, so iteration is evaluable in PSPACE. On finite ordered structures this logic captures PSPACE.

Every fixed second-order logic sentence is evaluable in PSPACE. On a universe of size $n$, a relation of arity $k$ is stored using $n^k$ bits. Enumerate its possible interpretations with a counter of the same polynomial length, recursively evaluate the inner formula and reuse the storage. Universal quantifiers require checking all interpretations; existential ones stop at the first success. The fixed quantifier depth and fixed arities bound total space by a polynomial, even though time can be exponential. First-order quantifiers and Boolean operations require no larger bound.

If $NP=PSPACE$, this places the class defined by the assumed second-order sentence in NP. Fagin's theorem would give an equivalent existential second-order sentence, again contradicting the hypothesis. HenceFor completeness, $NP\subseteq PSPACE$: a polynomial-time nondeterministic computation can be searched deterministically depth first, retaining a polynomial-length computation branch and reusing space. Thus the inequality is a strict containment under the stated hypothesis.

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.

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.

An algorithm uses polynomial space if its working memory is bounded by a fixed polynomial in the input length. Exponentially many possibilities can still be searched when each candidate and the search counter need polynomial space and storage is reused. The decision problems with deterministic polynomial-space algorithms form PSPACE.