Fagin's theorem
/ FAY-gin /
Imagine learning that the entire class NP — every problem whose solutions are easy to check — can be described purely in logic, with no clock, no Turing machine, and no notion of running time anywhere in sight. Fagin's theorem is that astonishing bridge. It says NP equals exactly the set of properties expressible in existential second-order logic, the very first result that gave a complexity class a clean, machine-free logical identity, and the founding theorem of descriptive complexity.
Unpacking the logic: ordinary (first-order) logic lets you quantify over individual elements — 'there exists a vertex x such that...'. Second-order logic adds the power to quantify over whole relations or sets — 'there exists a set S of vertices...' or 'there exists a colouring...'. The 'existential' part means you only get to say 'there EXISTS such a relation' at the outermost level, then describe a first-order condition it must satisfy. Fagin's theorem states: a property of finite structures is in NP if and only if it can be written in this form. The intuition lines up beautifully with NP's verifier picture — the existentially quantified relation is precisely the certificate, the guessed solution, and the first-order condition is the polynomial-time check that the certificate is valid.
This is a landmark because it reveals that 'efficiently checkable' and 'expressible by guessing a structure plus a simple condition' are the same notion, seen from two directions. It launched the whole program of capturing complexity classes by logics and reframed P vs NP as a question about logical expressiveness (does adding a fixed-point recursion operator to first-order logic suffice to express everything existential second-order logic can?). Honest caveat: these elegant correspondences are stated for finite structures and typically assume an ordering on the elements for the lower classes; they are a genuine, deep equivalence, not a loose analogy.
Graph 3-colourability is in NP, and Fagin's form makes this transparent: the property says 'there exist three sets R, G, B of vertices (an existential second-order quantifier) such that every vertex is in exactly one set and no edge joins two vertices of the same set (a first-order condition)'. The guessed sets are the certificate; the first-order part is the easy verification.
Fagin: NP = existential second-order logic — the guessed relation is the certificate, the rest is the check.
Fagin's theorem characterizes NP with NO reference to time or machines — that machine-independence is the whole point. The 'existential' restriction matters: full second-order logic captures the much larger polynomial hierarchy, not just NP.