 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. 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.