Введение
Множество всех свойств в экзистенциальной логике второго порядка является классом сложности NP. Теорема Фагина — старейший результат описательной теории сложности, области теории вычислительной сложности, которая характеризует классы сложности в терминах логических описаний задач, а не поведения алгоритмов, решающих эти задачи. Теорема утверждает, что множество всех свойств, выразимых в экзистенциальной логике второго порядка, точно соответствует классу сложности NP. Она была доказана Рональдом Фагином в 1973 году в его докторской диссертации и опубликована в его статье 1974 года. Требования к арности формулы второго порядка были улучшены (в одном направлении) Джеймсом Линчем в 1981 году, а несколько результатов Этьена Гранжана предоставили более точные оценки для недетерминированных машин с произвольным доступом к памяти.
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. The arity required by the second order formula was improved (in one direction) by James Lynch in 1981, and several results of Étienne Grandjean have provided tighter bounds on nondeterministic random access machines.
Доказательство
В дополнение к статье Фагина 1974 года, учебник Иммермана 1999 года содержит подробное доказательство теоремы. Легко показать, что любая экзистенциальная формула второго порядка может быть распознана в NP, недетерминированно выбирая значения всех переменных, связанных экзистенциальными кванторами. Таким образом, основная часть доказательства заключается в том, чтобы показать, что любой язык из NP может быть описан экзистенциальной формулой второго порядка. Для этого можно использовать экзистенциальные кванторы второго порядка для произвольного выбора таблицы вычислений. Более конкретно, для каждого момента времени в траектории выполнения недетерминированной машины Тьюринга эта таблица кодирует состояние машины Тьюринга, её позицию на ленте, содержимое каждой ячейки ленты и выбор, который машина делает на этом шаге. Формула первого порядка может ограничить эту закодированную информацию таким образом, чтобы она описывала допустимую траекторию выполнения, в которой содержимое ленты, состояние и позиция машины Тьюринга на каждом шаге времени следуют из предыдущего шага. Ключевая лемма, используемая в доказательстве, заключается в том, что можно закодировать линейный порядок длины (например, линейные порядки моментов времени и содержимого ленты на любом моменте времени) как n-арную реляцию на множестве размера m. Один из способов добиться этого – выбрать линейный порядок для m элементов, а затем определить реляцию как лексикографический порядок кортежей из m относительно этого порядка.