The theorem states that the set of all properties expressible in existential second-order logic is precisely the complexity class NP.
It was proven by Ronald Fagin in 1973 in his doctoral thesis, and appears in his 1974 paper.
[1] The arity required by the second-order formula was improved (in one direction) by James Lynch in 1981,[2] and several results of Étienne Grandjean have provided tighter bounds on nondeterministic random-access machines.
[3] In addition to Fagin's 1974 paper,[1] the 1999 textbook by Immerman provides a detailed proof of the theorem.
[4] It is straightforward to show that every existential second-order formula can be recognized in NP, by nondeterministically choosing the value of all existentially-qualified variables, so the main part of the proof is to show that every language in NP can be described by an existential second-order formula.
A first-order formula can constrain this encoded information so that it describes a valid execution trace, one in which the tape contents and Turing machine state and position at each timestep follow from the previous timestep.
A key lemma used in the proof is that it is possible to encode a linear order of length