There is a relation such that

Six sentences from two quantifiers worked with sentences that quantify over the points of a structure — “for every $x$ there is a $y$ such that…”. It ended by pointing at a larger kind of quantifier: “there is a relation $S$ such that…”, which chooses not a point but a whole set of points, or of pairs of points, and then asks something of it. That is second-order logic, and it closed with a sentence it did not prove: that on finite structures, one block of such quantifiers in front of a first-order sentence describes exactly the problems in NP.

This essay is about that theorem. The clearest way into it is a single example, a problem everyone who has coloured a map has met.

“This graph can be coloured with three colours so that no edge joins two points of the same colour” is a claim about a graph. Written in logic, it says: there exist three sets of points $R$, $G$ and $B$ such that

• every point is in exactly one of $R$, $G$, $B$, and
• no edge has both its ends in the same set.

The first line after “such that” is a first-order statement about points; so is the second. The whole sentence is existential second-order: a block of “there exist relations” followed by a first-order sentence. And its two halves do different jobs. The sets are a guess. The conditions are a check, and the check is easy: for the Petersen graph, ten tests on points and fifteen on edges, all of which the figure runs and passes.

Guessing is expensive, checking is cheap #

The difference between the two halves is the whole content of the theorem, and it can be counted.

A graph with $n$ points has $3^n$ ways to assign three colours: at sixteen points, over forty million. Checking one assignment takes one test per point and one per edge, a number that grows only like the size of the graph. So verifying a proposed answer is cheap and finding one may not be, and the figure shows the gap opening: the line for colourings climbs by a factor of nine every two points; the line for checks barely moves. A search that backtracks as soon as an edge fails tries far fewer colourings than all of them, but no method is known that avoids exponential work on the hardest graphs.

When the answer is no, the situation reverses. A graph that cannot be three-coloured has no colouring to exhibit, and convincing someone of that seems to require showing that every one of the $3^n$ candidates fails — a certificate of absence, which a failed search is a proof discussed as the kind of proof an exhaustive search provides. Non-colourability is described by a sentence beginning “for all sets $R$, $G$, $B$…”, a universal second-order sentence, and whether every such property also has short certificates is the question whether NP equals co-NP.

That shape — a certificate that may be hard to find and is easy to check — defines the class NP. Deciding three-colourability is in NP because a colouring is a certificate. Richard Karp showed in 1972 that it is as hard as anything in NP, the property the instance that has to be guessed followed through the satisfiability problem.

Fagin’s theorem #

Ronald Fagin proved in 1974 that the match between sentences and problems is exact. On finite structures — graphs, finite sets with relations on them —

a property can be expressed by an existential second-order sentence if and only if it can be decided in NP.

One direction is the example above in general form. Given a sentence “there exist relations $S_1, \ldots, S_k$ such that $\varphi$”, a machine can guess the relations — polynomially many bits, since a relation on $n$ points has at most $n^r$ entries — and then check $\varphi$, which, being first-order, needs only polynomial time. So every such property is in NP.

The other direction is the surprising one. Every problem in NP — every property decided by a machine that guesses a certificate and checks it in polynomial time — can be written as such a sentence. The proof writes the machine’s entire run as relations: which cell of the tape holds which symbol at which step, which state the machine is in at which step, laid out in a grid of time against position indexed by tuples of points. “There exist relations” guesses the whole run; the first-order part checks that each step follows from the one before by the machine’s rules, and that the run accepts. The guess is the computation, and the sentence is its specification.

Two colours are easy, three are not #

The same sentence with two sets instead of three says “the graph can be coloured with two colours”, and that property is easy: a graph is two-colourable exactly when it has no cycle of odd length, and a search that colours one point and then forces the colour of every neighbour decides it in time proportional to the graph’s size. So “there exist two sets such that…” describes a problem in P, while “there exist three sets such that…” describes one that is NP-complete.

Nothing in the shape of the sentences distinguishes them. Both are existential second-order with monadic guesses and the same first-order check. The difference is in what the guess can be forced to be: with two colours, each choice determines its neighbours, and there is nothing to search; with three, a choice leaves options open, and the options multiply. Fagin’s theorem says which problems are guessable, not which guesses are hard. The finer question — which existential sentences describe problems that can be decided without guessing — is exactly the P versus NP question in another form, and for the whole family of problems shaped like colourings — assign each point one of finitely many labels, subject to fixed local constraints — it was settled only in 2017, when Andrei Bulatov and Dmitriy Zhuk independently proved that every such constraint problem is either in P or NP-complete, with nothing in between.

A tour as a relation #

Colourings are sets of points. Other certificates are relations between points, and the theorem covers them the same way.

A Hamiltonian cycle visits every point of a graph once and returns to its start. “This graph has one” becomes: there is a relation $S$ — “the point after $x$ on the tour is $y$” — such that every pair in $S$ is an edge, every point has exactly one successor and exactly one predecessor, and following successors from any point visits every point. The figure draws $S$ for a tour of the cube as dots inside the grid of edges: each row and each column has exactly one dot, and every dot sits on a light square.

The last condition needs care. “Following successors visits every point” is not first-order on its own, since it talks about paths of unbounded length. The standard fix guesses one more relation, a linear order on the points, and asks that the successor relation follow it — first-order conditions again. So Hamiltonian cycles are in NP, as they should be: the tour is the certificate, and checking it is a matter of looking at each point and each edge.

Saying something first-order logic cannot #

The theorem also shows that second-order quantifiers add real power, and the smallest example is counting.

“The set has an even number of points” cannot be said by any first-order sentence. A game that decides what can be said proved this with the games of Ehrenfeucht and Fraïssé: for any first-order sentence, large enough sets of size six and seven — or $2k$ and $2k+1$ — cannot be told apart by it, because a player can always match the other’s moves. But with one guessed relation the property is easy: “there is a relation $M$ that pairs every point with exactly one other”, a perfect matching. A set has one exactly when its size is even, and checking a proposed $M$ is first-order.

Parity is therefore in NP — in fact it is trivially computable — and expressible with one existential second-order quantifier, while no first-order sentence expresses it. Second-order existential quantifiers can say what first-order logic cannot, and the things they can say are exactly the things a guess-and-check machine can decide.

The table of logics and classes #

Fagin’s theorem was the first of a family of results matching kinds of sentences to kinds of computation, and together they form a dictionary.

First-order sentences capture properties checkable by very shallow circuits — constant parallel time. Adding a least fixed point operator, which lets a formula define a relation by iterating a rule until nothing changes, captures polynomial time — on structures that come with a built-in order on their points, as Neil Immerman and Moshe Vardi proved independently in 1982. Universal second-order sentences capture co-NP, the complements of NP problems. Full second-order logic, with quantifiers over relations in any pattern, captures the polynomial hierarchy, as Larry Stockmeyer showed in 1977.

Each row trades a resource for a kind of sentence: time for the depth of an iteration, guessing for an existential quantifier over relations, alternation of guesses for alternation of quantifiers. The dictionary turns the P versus NP question into logic. On ordered finite structures, P equals NP exactly when every existential second-order sentence can be rewritten as a first-order sentence with a least fixed point. The machines disappear, and the question becomes whether a guess can always be replaced by an iteration. A machine that carries one bit met the same trade in a gentler setting: there, the guessing that a quantifier introduces could always be removed by a construction that tracks every possible guess at once, at a cost in size; here, removing it in general would collapse NP into P. Descriptive complexity is the name for this way of doing complexity theory, and its appeal is that the logical side never mentions time, space or machines at all.

Satisfiability is the sentence itself #

Fagin’s theorem and the Cook–Levin theorem of 1971, which made satisfiability of Boolean formulas the first NP-complete problem, are two views of the same construction. Cook and Levin wrote a machine’s run as a Boolean formula whose variables say which symbol is where at which step; Fagin wrote the same run as relations quantified at the front of a sentence. Guessing the relations and guessing the truth values of the variables are the same guess.

That is why the conclusion is what survives the erasing found the satisfiability problem so hard to escape: any existential second-order sentence, applied to a particular finite structure, unfolds into a satisfiability question about that structure, with one Boolean variable for each entry of each guessed relation. A method that solved satisfiability quickly would decide every such sentence quickly, and so every problem in NP.

Monadic guesses, and what they cannot do #

The guessed relations in the colouring example are sets of points — monadic relations. The tour needed a binary relation. Is that difference essential?

Fagin showed in 1975 that it is. “The graph is connected” can be expressed with a guessed binary relation, but not with any number of guessed sets of points followed by a first-order sentence: monadic NP cannot express connectivity. Yet the complement, “the graph is disconnected”, is easy in monadic NP — guess a set of points that is closed under edges and neither empty nor everything. So monadic NP is not closed under complement, a separation that the full classes NP and co-NP are only conjectured to have.

This is one of the few places where logic has proved a separation that complexity theory cannot yet prove in general: monadic NP differs from monadic co-NP, by a game argument of the kind the distance a sentence can see used, while whether NP differs from co-NP is open. The restricted version is provable because restricting the guesses to sets makes the logic weak enough for the games to reach.

The sizes a sentence allows #

The oldest question in this area predates Fagin by twenty years. Heinrich Scholz asked in 1952: given a first-order sentence, what are the sizes of the finite structures that satisfy it? The set of those sizes is the sentence’s spectrum. The sentence “there is a relation pairing every point with exactly one other” — now read as part of the sentence rather than guessed — has the even numbers as its spectrum; a sentence describing a field has the prime powers.

Neil Jones and Alan Selman, and Fagin independently, showed in 1974 that the spectra are exactly the sets of numbers recognisable in nondeterministic exponential time, measured in the number of digits. Günter Asser asked whether the complement of a spectrum is always a spectrum — whether “the sizes where the sentence fails” is itself the set of sizes of some other sentence. Asser’s question is still open, and by the Jones–Selman theorem it is equivalent to whether nondeterministic exponential time is closed under complement, a relative of the NP versus co-NP question one exponential up.

What the figures can and cannot show #

Every witness is checked. The colouring of the Petersen graph, the tour of the cube and the matching of six points are each verified against the first-order conditions the sentence lists, and the figures report the checks.

The search counts are for particular random graphs. They show the gap between the number of candidates and the cost of checking one on a handful of examples; that no method closes the gap on the hardest graphs is the P versus NP question, not a measurement.

The table of logics is quoted. Each row is a theorem with a long proof; the figure records which logic matches which class, and the essay explains the middle row.

Still open: a logic for polynomial time #

The Immerman–Vardi theorem needs an order on the points. Without one, least-fixed-point logic cannot even say “the set has an even number of points”, which is decidable in polynomial time. So on unordered structures — graphs as they really are, with no preferred labelling of their points — least-fixed-point logic falls short of P.

Whether any logic captures polynomial time on unordered structures is open. Yuri Gurevich conjectured in 1988 that none does, and the question has driven decades of work: logics with counting come close and fail on specially built graphs, and every proposed extension so far has either failed to capture all of P or has not been shown to stay inside it. The counting logics fail on pairs of graphs built by Jin-Yi Cai, Martin Fürer and Neil Immerman in 1992, which one gadget defeats every refinement drew as the graphs that defeat every dimension of colour refinement. And since Gurevich’s conjecture implies that P is not equal to NP — existential second-order logic captures NP on every structure, ordered or not, so a failure for P would separate them — the question sits at the junction of logic and complexity where neither side has yet found a way through.

A guess with a checkable shape #

The habit worth keeping is to separate what is guessed from what is checked.

A colouring, a tour, a matching — each is a relation that, once written down, can be verified by looking at points and edges one at a time. Finding it is another matter. Fagin’s theorem says that this distinction, between the relations that must be guessed and the first-order conditions that check them, is exactly the distinction between NP and the problems solvable without guessing. The hardest problems in computing are the properties whose sentences begin with a guess, and whether the guess can always be avoided is the question nobody has answered.