 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.