September Edition
Usually we think of the class NP as either languages accepted in
polynomial-time by a nondeterministic Turing machine or languages with
polynomial-time verifiable witnesses. Ronald Fagin gives a
characterization of NP based on logic without references to Turing
machines or polynomial time.
Ronald Fagin, Generalized
first-order spectra and polynomial-time recognizable sets. Complexity
of Computation, ed. R. Karp, SIAM-AMS Proceedings 7, 1974, pp. 43-73.
In this paper Fagin shows that NP consists of exactly the languages
expressible with existential second-order formulas. For example
consider a graph G described by an edge relation E(i,j) and we can
define whether G is k-colorable by
∃C ∀i,j (1≤C(i)≤k ∧
(E(i,j)→C(i)≠C(j)))
With some more work you can use binary predicates. In general every
language in NP has an existential second-order characterization with
binary predicates and a universal first-order part.
Stockmeyer generalizes
Fagin's result to characterize the polynomial-time
hierarchy with second-order formulas.
Fagin's result started the area of descriptive
complexity that characterized many common complexity classes in
various logics and has connections to the complexity of database
queries. Neil Immerman's work in descriptive complexity led him to his
proof
that nondeterministic space is closed under complement. Robert
Szelecpsényi independently came up with a similar proof through
a different approach.
Papadimitriou and Yannakakis use Fagin's result to characterize
the class MAX-SNP of optimization problems. One of the first
corollaries of the PCP Theorem is to
show the MAX-SNP hard problems cannot be approximated within an
arbitrary constant unless P=NP. In fact the concept of
probabilistically checkable proof itself originally comes from a
second-order view of NP that originated from Fagin's paper.
Update 10/12: Fagin adds an addendum.
Thanks to Lance and Siva for the kind words about my theorem. Let me
clarify the story on the arity of the existentially quantified relations.
An existential second-order formula about, say, graphs, is a formula of the
form
∃ Q1 ... ∃ Qk S( E, Q1, ...,
Qk)
where E represents the edge relation, Q1, ..., Qk are
existentially quantified predicates of arbitrary arity, and S(E,
Q1, ..., Qk) is a first-order formula that involves
only E, Q1, ..., Qk. As an example, 3-colorability
of the graph can be expressed by an existential second-order formula
∃ Q1 ∃ Q2 ∃ Q3 S(E,
Q1, Q2, Q3),
where Q1, Q2, and Q3 are unary predicates
(that represent the 3 colors), and S(E, Q1, Q2,
Q3) is a first-order formula that says "Each point has exactly
one color, and no two points with the same color are connected by an
edge''.
In the case of graphs, my theorem says that if T is a class of graphs that
is closed under isomorphism (that is, whenever T contains a graph G, then
it contains every graph isomorphic to G) , then T is in NP if and only if T
is defined by an existential second-order formula. In the case of graphs,
it is an open problem as to whether we really need to allow existentially
quantified predicates of arbitrary arity. On the one hand, it is
conceivable that there are NP properties of graphs that require
existentially quantified predicates of arbitrarily large arity. On the
other hand, it is conceivable that we can capture every NP property of
graphs by allowing only a single existentially quantified binary predicate.
If we consider NP properties not just of graphs, but of arbitrary
structures (such as structures with, say, two ternary relations and five
7-ary relations), then the characterization of NP in my theorem continues
to hold, but in this case, it is known that existentially quantified binary
predicates do not suffice. In particular, Ajtai proved (in the same
amazingly rich 1983 paper [Σ11-formulae on
finite structures, Annals of Pure and Applied Logic 24, 1983, pp. 1-48]
where, among other things, he proved the Furst-Saxe-Sipser theorem
independently of Furst, Saxe and Sipser), that if we consider structures
consisting of a single m-ary relation, then the statement "The number of
m-tuples in the relation is even" cannot be captured in existential
second-order logic with any number of existentially quantified predicates
of arity less than m.
A gentle introduction to the work I've mentioned in this note and to some
other work in finite model theory appears in my survey paper
Finite
model theory-a personal perspective.