Teorema de Fagin

Teorema de Fagin é um resultado da teoria da complexidade descritiva, que afirma que o conjunto de todas as propriedades que podem ser expressas na lógica de segunda ordem existencial, é precisamente a classe de complexidade NP. É notável, pois é uma caracterização da classe NP que não invoca um modelo de computação, tal como uma máquina de Turing.

Foi provado por Ronald Fagin em 1973, em sua tese de doutorado. A aridade exigida pela fórmula de segunda ordem foi melhorada (em uma direção) no teorema de  Lynch, e vários resultados de Grandjean forneceram limitantes mais próximos em máquinas de acesso aleatório não determinísticas .

Immerman em 1999, fornece uma prova detalhada do teorema. É simples, para mostrar que toda fórmula existencial de segunda ordem pode ser reconhecida em NP, escolhendo não deterministicamente o valor de todas as variáveis existencialmente qualificadas, de modo que a parte principal da prova é mostrar que cada linguagem em NP pode ser descrita por uma fórmula existencial de segunda ordem. Para fazer isso, pode-se usar de quantificadores existenciais de segunda ordem para escolher arbitrariamente uma tableau de computação. Em mais detalhe, para cada iteração de uma história de execução de uma máquina de Turing não determinística, este tableau codifica o estado da máquina de Turing, a sua posição na fita, o conteúdo de cada célula da fita, e cuja escolha não determinística a máquina faz nessa etapa. Restringindo esta informação codificada de forma que ela descreve uma história de execução válida em que o conteúdo da fita e o estado da máquina de Turing  e sua posição em cada iteração da iteração anterior pode ser feita com uma fórmula de primeira ordem.

Um lema chave utilizado na prova disso é que é possível codificar uma ordem linear de comprimento n^k (tais como as ordens lineares de iterações e conteúdo da fita, a qualquer tempo) como uma relação 2k-ária R em um universo A de tamanho n. Uma forma de conseguir isto, é escolher uma ordenação linear L de A e, em seguida, definir  R  para ser a ordenação lexicográfica de k-tuplas de A com relação a L.

• O espectro de uma frase

• R. Fagin. Generalizada de Primeira Ordem Espectros e em Tempo Polinomial Reconhecível Conjuntos. A complexidade de Computação, ed. R. Karp, o SIAM-AMS Processo 7, pp. 27–41. 1974.
• Immerman, Neil (1999). Descriptive Complexity. New York: Springer-Verlag. pp. 113–119. ISBN 0-387-98600-6 

• Grädel, Erich; Kolaitis, Phokion G.; Libkin, Leonid; Marx, Maarten; Spencer, Joel; Vardi, Moshe Y.; Venema, Yde; Weinstein, Scott (2007). Finite model theory and its applications. Col: Texts in Theoretical Computer Science. An EATCS Series. Berlin: Springer-Verlag. ISBN 978-3-540-00428-8. Zbl 1133.03001