Fagin's theorem is the oldest result of descriptive complexity theory, a branch of computational complexity theory that characterizes complexity classes in terms of logic-based descriptions of their problems rather than by the behavior of algorithms for solving those problems. 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]