= 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> sentence
$$
\exists R_1\cdots\exists R_m\,\psi,
$$
where $\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.
Back to article page
