Fagin's theorem
{{short description|Set of all properties in existential 2nd order logic is the complexity class NP}}
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.{{sfn|Fagin|1974}} The arity required by the second-order formula was improved (in one direction) by James Lynch in 1981,{{sfn|Lynch|1981}} and several results of Étienne Grandjean have provided tighter bounds on nondeterministic random-access machines.{{harvnb|Grandjean|1985}}; {{harvnb|Grandjean|Olive|1998}}
Proof
In addition to Fagin's 1974 paper,{{sfn|Fagin|1974}} the 1999 textbook by Immerman provides a detailed proof of the theorem.{{sfn|Immerman|1999}} 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. To do so, one can use second-order existential quantifiers to arbitrarily choose a computation tableau. In more detail, for every timestep of an execution trace of a non-deterministic Turing machine, this tableau encodes the state of the Turing machine, its position in the tape, the contents of every tape cell, and which nondeterministic choice the machine makes at that step. 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 (such as the linear orders of timesteps and tape contents at any timestep) as a {{nowrap|-ary}} relation on a universe of {{nowrap|size .}} One way to achieve this is to choose a linear ordering of and then define to be the lexicographical ordering of {{nowrap|-tuples}} from with respect {{nowrap|to .}}
See also
Notes
{{reflist}}
References
- {{cite conference
| last = Fagin | first = Ronald | author-link = Ronald Fagin
| editor-last = Karp | editor-first = Richard M. | editor-link = Richard M. Karp
| contribution = Generalized first-order spectra and polynomial-time recognizable sets
| contribution-url = https://books.google.com/books?id=004anbcFjnwC&pg=PA43
| isbn = 978-0-8218-1327-0
| mr = 0371622
| pages = 43–73
| publisher = American Mathematical Society
| series = SIAM–AMS Proceedings
| title = Complexity of Computation: Proceedings of a Symposium in Applied Mathematics of the American Mathematical Society and the Society for industrial and Applied Mathematics held in New York City, April 18–19, 1973
| volume = 7
| year = 1974}}
- {{cite journal
| last = Grandjean | first = Étienne
| doi = 10.1007/BF01699468
| issue = 2
| journal = Mathematical Systems Theory
| mr = 797194
| pages = 171–187
| title = Universal quantifiers and time complexity of random access machines
| volume = 18
| year = 1985}}
- {{cite journal
| last1 = Grandjean | first1 = Étienne
| last2 = Olive | first2 = Frédéric
| doi = 10.1007/PL00001594
| issue = 1
| journal = Computational Complexity
| mr = 1628153
| pages = 54–97
| title = Monadic logical definability of nondeterministic linear time
| volume = 7
| year = 1998}}
- {{cite book | last = Immerman | first = Neil | authorlink = Neil Immerman | title = Descriptive Complexity|title-link= Descriptive Complexity | year = 1999 | publisher = Springer-Verlag | location = New York | isbn = 0-387-98600-6 | pages = 113–119}}
- {{cite journal | last1 = Lynch | first1 = James | date = December 1981 | title = Complexity classes and theories of finite models | url = https://link.springer.com/article/10.1007/BF01786976 | journal = Mathematical Systems Theory | volume = 15 | pages = 127–144 | doi = 10.1007/BF01786976 | s2cid = 496247 }}
- {{cite book | last1=Grädel | first1=Erich | last2=Kolaitis | first2=Phokion G. | last3=Libkin | first3=Leonid | author3-link=Leonid Libkin | first4=Maarten | last4=Marx | last5=Spencer | first5=Joel | author5-link=Joel Spencer | last6=Vardi | first6=Moshe Y. | author6-link=Moshe Y. Vardi | last7=Venema | first7=Yde | last8=Weinstein | first8=Scott | title=Finite model theory and its applications | zbl=1133.03001 | series=Texts in Theoretical Computer Science. An EATCS Series | location=Berlin | publisher=Springer-Verlag | isbn=978-3-540-00428-8 | year=2007 }}