El teorema de Fagin es el resultado más antiguo de la teoría descriptiva de la complejidad , una rama de la teoría de la complejidad computacional que caracteriza las clases de complejidad en términos de descripciones basadas en la lógica de sus problemas en lugar de por el comportamiento de los algoritmos para resolver esos problemas. El teorema establece que el conjunto de todas las propiedades expresables en la lógica existencial de segundo orden es precisamente la clase de complejidad NP .
Ronald Fagin lo demostró en 1973 en su tesis doctoral y aparece en su artículo de 1974. [1] James Lynch mejoró (en una dirección) la aridad requerida por la fórmula de segundo orden en 1981, [2] y varios resultados de Étienne Grandjean han proporcionado límites más estrictos a las máquinas de acceso aleatorio no deterministas . [3]
Además del artículo de Fagin de 1974, [1] el libro de texto de 1999 de Immerman proporciona una demostración detallada del teorema. [4] Es sencillo demostrar que cada fórmula existencial de segundo orden puede reconocerse en NP, eligiendo de manera no determinista el valor de todas las variables existencialmente calificadas, por lo que la parte principal de la prueba es mostrar que cada lenguaje en NP puede ser reconocido. descrito por una fórmula existencial de segundo orden. Para hacerlo, se pueden utilizar cuantificadores existenciales de segundo orden para elegir arbitrariamente una tabla de cálculo. Con más detalle, para cada paso de tiempo de una traza de ejecución de una máquina de Turing no determinista , este cuadro codifica el estado de la máquina de Turing, su posición en la cinta, el contenido de cada celda de la cinta y qué elección no determinista hace la máquina en ese paso. Una fórmula de primer orden puede restringir esta información codificada para que describa un seguimiento de ejecución válido, uno en el que el contenido de la cinta y el estado y la posición de la máquina de Turing en cada paso de tiempo siguen al paso de tiempo anterior.
Un lema clave utilizado en la prueba es que es posible codificar un orden lineal de longitud (como los órdenes lineales de pasos de tiempo y contenidos de cinta en cualquier paso de tiempo) como una relación aria en un universo de tamaño . Una forma de lograr esto es elegir un orden lineal de y luego definirlo como el orden lexicográfico de -tuplas desde con respecto a .
