= Solution
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. Hence
$$
\boxed{NP\ne PSPACE.}
$$
For 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.
Back to article page
