Fagin's theorem states that, for a finite relational signature, an isomorphism-invariant class of finite structures has its standard encoding language in NP if and only if it is definable by an existential second-order logic sentencewhere is first-order and the relation variables have fixed finite arities. The forward implication includes the substantive encoding of a polynomially bounded accepting computation by relations. In the reverse implication the relations are polynomial-length certificates and the fixed first-order sentence can be checked in polynomial time. This is a finite-structure characterization; no order need be named in the input signature.
Here equivalence means equivalence on all finite structures of the chosen signature, and an existential sentence means an existential second-order sentence. Suppose, towards a contradiction, that P equals NP. We use that P is closed under complementation, that fixed first-order model checking is polynomial-time, and that guessing a polynomial-length string followed by a polynomial-time test is in NP.
Under this equality, evaluating any fixed second-order logic sentence is in P. Prove this by induction through its quantifiers and Boolean operations. The first-order part is already polynomial-time. If an inner formula can be evaluated in P, existentially quantifying a relation of fixed arity guesses at most bits and then performs the inner polynomial-time test. This gives an NP procedure and hence, under the assumption, a P procedure. A universal relation quantifier is handled by complementing the corresponding existential test. Boolean combinations remain polynomial-time as well. A fixed formula has only finitely many such steps and fixed arities, so the resulting time bound is polynomial.
Consequently every second-order definable class lies in P, hence in NP. By Fagin's theorem it has an equivalent existential second-order sentence. This contradicts the posited second-order sentence with no such equivalent. ThereforeThe proof uses the equality assumption to collapse quantifier alternation; it does not assume an unproved strictness statement about the polynomial hierarchy.
Every fixed second-order logic sentence is evaluable in PSPACE. On a universe of size , a relation of arity is stored using 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 , 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, : 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.
Articles by others on the same topic
There are currently no matching articles.