Fagin's Theorem

Fagin's theorem is a result in descriptive complexity theory that states that the set of all properties expressible in existential second-order logic is precisely the complexity class NP. It is remarkable since it is a characterization of the class NP that does not invoke a model of computation such as a Turing machine.

It was proven by Ronald Fagin in 1974 (strictly, in 1973 in his doctoral thesis). The arity required by the second-order formula was improved (in one direction) in Lynch's theorem, and several results of Grandjean have provided tighter bounds on nondeterministic random-access machines.