Past exam of the mathematics course of the University of Cambridge / 2002 / iii / Paper 23 / 7 / a / Solution

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 $\psi$ 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.