Fagin's theorem

The set of Fagin is a proven 1973 by Ronald Fagin set of descriptive complexity theory, which says that the set of all writable using the existential second-order logic predicate sentences is exactly the complexity class NP.

The existential predicate logic second stage contains sentences, in which existentially quantified over the predicate of a sentence from the first order predicate logic. More specifically, it is sentences of the form

Where the term only quantification over the individual variables but contains no quantification of the predicate variables. The class NP is the class of those decision problems that can be decided by a nondeterministic Turing machine in polynomial time. The remarkable thing about this set is that it characterizes a complexity class only on the basis of logic, without resorting to a calculation model like Turing machines. He founded the descriptive complexity theory.

Larry J. Stockmeyer generalized the result and showed that the Polynomialzeithierarchie is described by the general second-order logic predicate ( with universal quantifiers ).