Логика с двумя переменными

В математической логике и информатике двухпеременная логика — это фрагмент логики первого порядка , в котором формулы могут быть записаны с использованием только двух различных переменных . ^[1] Этот фрагмент обычно изучается без функциональных символов .

Разрешимость

Некоторые важные проблемы двухпеременной логики, такие как выполнимость и конечная выполнимость , разрешимы . ^[2] Этот результат обобщает результаты о разрешимости фрагментов двухпеременной логики, таких как некоторые дескриптивные логики ; однако некоторые фрагменты двухпеременной логики обладают гораздо меньшей вычислительной сложностью для своих проблем выполнимости.

Напротив, для трехпеременного фрагмента логики первого порядка без функциональных символов выполнимость неразрешима. ^[3]

Подсчет квантификаторов

Известно, что двухпеременный фрагмент логики первого порядка без функциональных символов разрешим даже с добавлением квантификаторов подсчета ^[4] и, таким образом, квантификации уникальности . Это более мощный результат, поскольку квантификаторы подсчета для высоких числовых значений невыразимы в этой логике.

Подсчет квантификаторов фактически улучшает выразительность логик с конечным числом переменных, поскольку они позволяют сказать, что существует узел с соседями, а именно . Без подсчета квантификаторов переменные необходимы для той же формулы. ${\displaystyle n}$ ${\displaystyle \Phi =\exists x\exists ^{\geq n}yE(x,y)}$ ${\displaystyle n+1}$

Подключение к алгоритму Вайсфейлера-Лемана

Существует сильная связь между двухпеременной логикой и алгоритмом Вайсфейлера-Лемана (или уточнения цвета ). Если даны два графа, то любые два узла имеют одинаковый устойчивый цвет в уточнении цвета тогда и только тогда, когда они имеют одинаковый тип, то есть они удовлетворяют тем же формулам в двухпеременной логике с подсчетом. ^[5] ${\displaystyle C^{2}}$

Ссылки

1. Л. Хенкин. Логические системы, содержащие только конечное число символов , Отчет, Кафедра математики, Монреальский университет, 1967
2. Э. Грэдель, П. Г. Колайтис и М. Варди, О проблеме принятия решений для двухпеременной логики первого порядка , Бюллетень символической логики, т. 3, № 1 (март, 1997), стр. 53-69.
3. AS Kahr, Edward F. Moore и Hao Wang. Entscheidungsproblem Reduced to the ∀ ∃ ∀ Case , 1962, отмечая, что их формулы ∀ ∃ ∀ используют только три переменные.
4. Э. Грэдель, М. Отто и Э. Розен. Двумерная логика с подсчетом разрешима. Труды двенадцатого ежегодного симпозиума IEEE по логике в компьютерных науках, 1997.
5. Гроэ, Мартин. «Конечные переменные логики в дескриптивной теории сложности». Bulletin of Symbolic Logic 4.4 (1998): 345-398.