Fagin's theorem

The set of Fagin is a 1973 by Ronald Fagin proven set of the descriptive complexity theory , stating that the amount of all with the aid of the existential second predicate logic stage the complexity class writeable sets exactly NP is.

The existential predicate logic of the second level contains sentences in which existence is quantified via the predicates of a sentence from the predicate logic of the first level . More precisely, they are sentences of the form

${\displaystyle \exists X_{1}\ldots \exists X_{k}\,\varphi (x_{1},\ldots ,x_{m},X_{1},\ldots ,X_{k})}$

whereby the expression only contains quantifications via the individual variables but no quantifications via 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 theorem is that it characterizes a complexity class only on the basis of a logic, without resorting to a computational model such as Turing machines . With this he founded the descriptive complexity theory. ${\displaystyle \varphi (x_{1},\ldots ,x_{m},X_{1},\ldots ,X_{k})}$ ${\displaystyle x_{1},\ldots ,x_{m}}$ ${\displaystyle X_{1},\ldots ,X_{k}}$

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

literature

• R. Fagin . Generalized First-Order Spectra and Polynomial-Time Recognizable Sets (PDF; 2.0 MB). Complexity of Computation , ed. R. Karp, SIAM-AMS Proceedings 7, pp. 27-41. 1974.
• Neil Immerman : Descriptive Complexity . Springer, 1999, ISBN 0-387-98600-6 , pp. 113-119 .
• Heinz-Dieter Ebbinghaus , Jörg Flum : Finite Model Theory . Springer, 1999, ISBN 3-540-28787-6 , pp. 119-164 .