A syntactic characterization of NP-completeness

Fagin (1974) proved that NP is equal to the set of problems expressible in second-order existential logic (SO∃). We consider problems that are NP-complete via first-order projections (fops). These low-level reductions are known to have nice properties, including the fact that every pair of problems that are NP-complete via fops are isomorphic via a first-order definable isomorphism (E. Allender et al., 1993). However, before this paper, fewer than five natural problems had actually been shown to be NP-complete via fops. We give a necessary and sufficient syntactic condition for an SO∃ formula to represent a problem that is NP-complete via fops. Using this condition we prove syntactically that 29 natural NP-complete problems remain complete via fops