El teorema de Fagin es el resultado más antiguo de la teoría de la complejidad descriptiva , 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 .
Fue demostrado por Ronald Fagin en 1973 en su tesis doctoral, y aparece en su artículo de 1974. [1] La aridad requerida por la fórmula de segundo orden fue mejorada (en una dirección) por James Lynch en 1981, [2] y varios resultados de Étienne Grandjean han proporcionado límites más estrictos en 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 prueba 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 calificadas existencialmente, por lo que la parte principal de la prueba es demostrar que cada lenguaje en NP puede describirse mediante una fórmula existencial de segundo orden. Para ello, se pueden utilizar cuantificadores existenciales de segundo orden para elegir arbitrariamente una tabla de cálculo. En más detalle, para cada paso de tiempo de un rastro de ejecución de una máquina de Turing no determinista , esta tabla 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 rastro de ejecución válido, 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 se derivan del 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 los pasos de tiempo y los contenidos de la 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 ordenamiento lineal de y luego definir como el ordenamiento lexicográfico de las -tuplas de con respecto a .
