Fagin's theorem
Encyclopedia
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.
.
A key idea from the proof is that we can encode a linear order of length nk as a 2k-ary relation R on a universe A of size n. To achieve this, we choose a linear ordering L of A and then define R to be the lexicographical order
ing of k-tuples from A with respect to L.
Descriptive complexity
Descriptive complexity is a branch of computational complexity theory and of finite model theory that characterizes complexity classes by the type of logic needed to express the languages in them. For example, PH, the union of all complexity classes in the polynomial hierarchy, is precisely the...
that states that the set of all properties expressible in existential second-order logic
Second-order logic
In logic and mathematics second-order logic is an extension of first-order logic, which itself is an extension of propositional logic. Second-order logic is in turn extended by higher-order logic and type theory....
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
Turing machine
A Turing machine is a theoretical device that manipulates symbols on a strip of tape according to a table of rules. Despite its simplicity, a Turing machine can be adapted to simulate the logic of any computer algorithm, and is particularly useful in explaining the functions of a CPU inside a...
.
It was proven by Ronald Fagin
Ronald Fagin
Ronald Fagin is the Manager of the Foundations of Computer Science group at the IBM Almaden Research Center. He is best known for his pioneering work in database theory, finite model theory, and reasoning about knowledge...
in 1974 (strictly, in 1973 in his doctoral thesis). The arity
Arity
In logic, mathematics, and computer science, the arity of a function or operation is the number of arguments or operands that the function takes. The arity of a relation is the dimension of the domain in the corresponding Cartesian product...
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.
Proof
Immerman 1999 provides a detailed proof of the theorem. Essentially, we use second-order existential quantifiers to arbitrarily choose a computation tableau. For every timestep, we arbitrarily choose the finite state control's state, the contents of every tape cell, and which nondeterministic choice we must make. Verifying that each timestep follows from each previous timestep can then be done with a first-order formulaFirst-order logic
First-order logic is a formal logical system used in mathematics, philosophy, linguistics, and computer science. It goes by many names, including: first-order predicate calculus, the lower predicate calculus, quantification theory, and predicate logic...
.
A key idea from the proof is that we can encode a linear order of length nk as a 2k-ary relation R on a universe A of size n. To achieve this, we choose a linear ordering L of A and then define R to be the lexicographical order
Lexicographical order
In mathematics, the lexicographic or lexicographical order, , is a generalization of the way the alphabetical order of words is based on the alphabetical order of letters.-Definition:Given two partially ordered sets A and B, the lexicographical order on...
ing of k-tuples from A with respect to L.