Доклады Российской академии наук. Математика, информатика, процессы управления, 2022, T. 507, № 1, стр. 61-65

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

Известно, что классическая логика бинарного предиката неразрешима [4, глава 21]. Отметим, что соответствующее доказательство [4] использует бесконечно много предметных переменных; в то же время для доказательства неразрешимости логики предикатов достаточно трех предметных переменных, если ее язык содержит, помимо бинарной предикатной буквы, бесконечно много унарных букв [5]. Понижение числа переменных до двух [6, 7], использование лишь унарных букв и равенства [4, глава 21] или охраняемых фрагментов, где бинарные буквы допускаются в формулах ограниченно [8], приводит к разрешимости. Возникает естественный вопрос о разрешимости логики и теорий бинарного предиката в языке с конечным числом переменных, начиная с трех.

Аналогичная ситуация наблюдается и при обогащении языка логики предикатов различными дополнительными средствами, важными для приложений. Так, логика предикатов с равенством, обогащенная оператором транзитивного замыкания, $\Pi _{1}^{1}$-трудна в языке с двумя переменными, но доказательство использует несколько бинарных букв и бесконечно много унарных [9]; и здесь тоже возникает вопрос об алгоритмической сложности теорий бинарного предиката в языке с конечным числом переменных, но уже начиная с двух.

Ответ на вопрос о разрешимости логики бинарного предиката в языке с числом переменных не менее трех (и без дополнительных операторов) следует из [10]: такая логика неразрешима (см. [10, пункт (ii) раздела 4.8]). Аналогичные результаты для классической логики бинарного предиката в языке с двумя переменными, обогащенном дополнительными операторами, автору неизвестны.

Ниже будет описано построение, дающее короткое доказательство, во-первых, неразрешимости многих теорий бинарного предиката в языке с тремя предметными переменными (в частности, $\Sigma _{1}^{0}$-полноты логики бинарного предиката и $\Pi _{1}^{0}$-полноты теории конечных моделей бинарного предиката), а во-вторых, $\Pi _{1}^{1}$-трудности проблемы общезначимости формул в языке с бинарной предикатной буквой, равенством и двумя предметными переменными, обогащенном операторами композиции и транзитивного замыкания. Построение будет состоять в моделировании проблем укладки домино [11, 12]; отметим, что такой метод хорошо известен, и примеры применения теории замощений можно найти как в алгебре [13, 14], так и в логике [1, 15–18].

Неразрешимая проблема домино. Плитки домино имеют квадратную форму одинакового размера; тип t плитки определяется цветами $lt$, $rt$, $ut$ и $dt$ ее граней. Следующая проблема укладки $\Pi _{1}^{0}$-полна [11]: по набору $T = \{ {{t}_{0}}, \ldots ,{{t}_{n}}\} $ типов плиток нужно выяснить, существует ли T-укладка, т.е. такая  функция $f:\mathbb{N} \times \mathbb{N} \to T$, что для любых i, $j\, \in \,\mathbb{N}$ выполняются равенства $rf(i,j)\, = \,lf(i + 1,j)$ и $uf(i,j)\, = \,df(i,j + 1)$.

Моделирование укладки. Зафиксируем бинарную предикатную P. Введем сокращения. Пусть $rx = xPx$, $\bar {r}x = \neg rx$, $gx = \exists y{\kern 1pt} (ry \wedge xPy)$, $\bar {g}x = \neg gx$, а также

Если выполнено $rx$, то $x$ является рефлексивным, а если $\bar {r}x$, то иррефлексивным; $gx$ понимаем как то, что $x$ – элемент сетки $\mathbb{N} \times \mathbb{N}$, т.е. место для плитки, $E$ задает конгруэнтность, $S$ – смещение на $P$-шаг, $H$ и $V$ понимаем как смещения вправо и вверх. Чтобы определить $xSz$, в определении для $xSy$ одновременно заменяем $y$ на $z$ и $z$ на $y$; аналогично для $ySz$, $zSy$, $xEz$ и т.д. Если $u$ – свойство, то ${{\forall }_{u}}x{\kern 1pt} A = \forall x{\kern 1pt} (ux \to A)$, ${{\exists }_{u}}x{\kern 1pt} A = \exists x{\kern 1pt} (ux \wedge A)$.

Пусть $G$ – конъюнкция формул $\forall x\forall y\forall z{\kern 1pt} (xPy\, \wedge \,yPz$ → xPz), ${{\forall }_{g}}x{{\exists }_{g}}y{\kern 1pt} xHy$, ${{\forall }_{g}}x{{\exists }_{g}}y{\kern 1pt} xVy$, ${{\forall }_{g}}x{{\forall }_{g}}y{\kern 1pt} (\exists z{\kern 1pt} (xHz\, \wedge \,zVy)$ $ \leftrightarrow $ $\exists z{\kern 1pt} (xVz$ $ \wedge $ $zHy))$ и ${{\exists }_{g}}x{\kern 1pt} \bar {r}x$. Тогда если $G$ истинна в некоторой модели $M$, то $M$ содержит сетку вида $\mathbb{N} \times \mathbb{N}$, горизонтальные ряды которой задает $H$, а вертикальные $V$, причем элементы первого горизонтального ряда являются иррефлексивными, второго – рефлексивными, третьего – иррефлексивными и т.д.

Пусть ${{h}^{y}}x = \neg \exists y{\kern 1pt} xPy$, $t_{0}^{y}x = {{\exists }_{{\bar {g}}}}y{\kern 1pt} (xSy \wedge {{h}^{x}}y)$, $t_{{k + 1}}^{y}x = {{\exists }_{{\bar {g}}}}y{\kern 1pt} (xSy \wedge t_{k}^{x}y)$, где $k \in \mathbb{N}$. Формула $t_{m}^{y}x$ выражает следующее: $x$ видит своего $S$-последователя вне сетки, который видит последний элемент за $m$ $S$-шагов. Ниже вместо $t_{m}^{y}x$ и $t_{m}^{x}y$ пишем ${{t}_{m}}x$ и ${{t}_{m}}y$. Содержательно ${{t}_{m}}x$ означает, что на месте $x$ лежит плитка типа ${{t}_{m}}$.

Пусть ${{t}_{T}}$ – конъюнкция следующих формул:

Лемма 1. $G \wedge {{t}_{T}}$ выполнима $ \Leftrightarrow $ существует $T$‑укладка.

Отметим, что в построениях можно обойтись лишь позитивными формулами, заменив формулу $G \wedge {{t}_{T}}$ на ее отрицание, проблему выполнимости – на проблему опровержимости, а затем все вхождения отрицания – на импликацию к формуле $\forall x\forall y{\kern 1pt} xPy$.

Теории бинарного предиката. Из леммы 1, с учетом замечания о позитивных формулах, получаем следующее уточнение теоремы Чёрча [19]:

• позитивный фрагмент классической логики предикатов $\Sigma _{1}^{0}$-полон в языке с бинарной предикатной буквой и тремя предметными переменными.

Этот факт можно обобщить на различные теории бинарного предиката: достаточно внести незначительные изменения в описанное выше моделирование. Для класса моделей $C$ бинарного предиката элементарную теорию этого класса обозначим $Th(C)$. Пусть $F$, $If$, $R$, $Ir$, $S$, $As$, $T$ и $It$ – классы всех, соответственно, конечных, бесконечных, рефлексивных, иррефлексивных, симметричных, антисимметричных, транзитивных и интранзитивных моделей бинарного предиката. Если $X$ и $Y$ – классы моделей, то вместо $X \cap Y$ будем писать $XY$. Так, $IfRST$ – класс всех бесконечных моделей, являющихся одновременно рефлексивными, симметричными и транзитивными.

Теорема 1. Пусть $C$ – класс моделей бинарного предиката, содержащий хотя бы один из следующих классов: $IfIrT$, $IfIt$, $IfRS$, $IfIrS$. Тогда позитивный фрагмент теории $Th(C)$ в языке с тремя переменными является $\Sigma _{1}^{0}$-трудным.

Получаем, в частности, что теории классов If, $R$, $Ir$, $S$, $As$, $T$ и It неразрешимы в языке с тремя предметными переменными.

Используя сходную аргументацию, можно получить следующее уточнение теоремы Трахтенброта [20, 21]:

• позитивный фрагмент теории конечных моделей $\Pi _{1}^{0}$-полон в языке, содержащем бинарную предикатную букву и три предметные переменные.

Для обоснования этого факта достаточно учесть, что с помощью проблемы укладки кодируется проблема неостановки машин Тьюринга на пустой ленте, а затем изменить формулы выше так, чтобы они утверждали, что первый ряд укладки описывает начальную конфигурацию с пустой лентой, а в имеющемся начальном фрагменте укладки не встречается плитка, тип которой соответствует заключительному состоянию машины Тьюринга; отметим, что другой возможный путь состоит в использовании эффективной неотделимости [22] и теоремы 1.

Справедливо и более общее утверждение.

Теорема 2. Пусть C – класс конечных моделей бинарного предиката, содержащий $FR$ или $FIrAsT$. Тогда позитивный фрагмент теории $Th(C)$ в языке с тремя переменными является $\Pi _{1}^{0}$-трудным.

Обогащение языка. Покажем, что обогащение языка может привести к сильной неразрешимости, причем иногда даже при наличии в языке лишь двух переменных. Рассмотрим проблему укладки плиток домино, когда для $T$-укладки f дополнительно требуется, чтобы множество $\{ j \in \mathbb{N}:f(0,j) = {{t}_{0}}\} $ было бесконечным. Известно, что эта проблема $\Sigma _{1}^{1}$-полна [12, теорема 6.4].

Пусть в языке имеется оператор транзитивного замыкания и ${{P}^{ + }}$ соответствует транзитивному замыканию $P$. Для формулы $A$ определим $A{\kern 1pt} '$ как формулу, получающуюся из $A$ заменой $P$ на ${{P}^{ + }}$. Пусть $lx\, = \,\neg \exists y{\kern 1pt} yH{\kern 1pt} 'x$. Пусть G* – конъюнкция формул $\forall x\forall y{\kern 1pt} (xPy \wedge \neg yPx \to xS{\kern 1pt} 'z)$, ${{\forall }_{{g{\kern 1pt} '}}}x{{\exists }_{{g{\kern 1pt} '}}}y{\kern 1pt} xH{\kern 1pt} 'y$, ${{\forall }_{{g{\kern 1pt} '}}}x{{\exists }_{{g{\kern 1pt} '}}}y{\kern 1pt} xV{\kern 1pt} 'y$, ${{\forall }_{{g{\kern 1pt} '}}}x{{\exists }_{{g{\kern 1pt} '}}}y{\kern 1pt} (\exists z{\kern 1pt} (xH{\kern 1pt} 'z \wedge zV{\kern 1pt} 'y)$ ↔ $\exists z{\kern 1pt} (xV{\kern 1pt} 'z \wedge zH{\kern 1pt} 'y))$, ${{\exists }_{{g{\kern 1pt} '}}}x{\kern 1pt} (\bar {r}x \wedge lx)$ и ${{\forall }_{{g{\kern 1pt} '}}}x{\kern 1pt} (lx$ $ \to $ $ \to $ ${{\forall }_{{g{\kern 1pt} '}}}y{\kern 1pt} (xVy \to ly))$, а $t_{T}^{*}$ – конъюнкция $t_{T}^{'}$ и формулы ${{\forall }_{{g{\kern 1pt} '}}}x{\kern 1pt} (lx \to {{\exists }_{{g{\kern 1pt} '}}}y{\kern 1pt} (\neg xE{\kern 1pt} 'y \wedge x{{P}^{ + }}y \wedge ly \wedge t_{0}^{'}y))$. Тогда выполнимость формулы $G{\kern 1pt} * \wedge \,t_{T}^{*}$ эквивалентна существованию $T$-укладки с дополнительным условием. Это дает $\Pi _{1}^{1}$-трудность теорий в языке с бинарной предикатной буквой и тремя переменными; отметим, что оператор транзитивного замыкания применялся лишь к атомарным формулам.

При добавлении равенства и композиции, используя идеи, изложенные в [9], можно описать эту же проблему укладки домино, задействуя всего две переменные и одну бинарную предикатную букву. Третья переменная входит в определения для $E$ и $S$, а также в один из конъюнктивных членов формулы $G$. Заменяем $E$ равенством. Используя равенство и транзитивное замыкание, можно выразить условие функциональности бинарного отношения с дополнительными требованием сюръективности и отсутствия общих элементов в области определения и прибытия, см. [9]. Это позволяет “разбить” движение по $H$ и $V$ на “четные” и “нечетные” шаги ${{H}_{0}}$, ${{H}_{1}}$, ${{V}_{0}}$, ${{V}_{1}}$; в формулах вида ${{t}_{m}}x$ вместо $S$ можно использовать $P$; как итог, $S$ больше не требуется. Конъюнктивный член в $G$ с тремя переменными заменяем на ${{\forall }_{{g{\kern 1pt} '}}}x{\kern 1pt} {{\exists }_{{g{\kern 1pt} '}}}y{\kern 1pt} (x[H\, \circ \,V]y\, \wedge \,x[V\, \circ \,H]y)$, где xHy = xH₀y $ \vee $ $ \vee $ $x{{H}_{1}}y$ и $xVy = x{{V}_{0}}y \vee x{{V}_{1}}y$. Снова получаем $\Pi _{1}^{1}$‑трудность теорий, но при двух переменных.

Получаем следующую теорему.

Теорема 3. Проблема общезначимости формул языка логики предикатов с двумя предметными переменными, бинарной предикатной буквой и равенством, обогащенного операторами транзитивного замыкания и композиции, $\Pi _{1}^{1}$-трудна.

Отметим, что проблема истинности формул такого языка в классе всех конечных моделей не выходит за границы класса $\Pi _{1}^{0}$, поскольку можно эффективно перечислить как все формулы, так и все конечные модели (с точностью до изоморфизма), что позволяет построить эффективное перечисление множества опровержимых формул.

Обсуждение. Отметим, что незначительно ослабленные варианты теорем 1 и 2 могут быть получены из [10] с учетом результатов, представленных в [2, 3, 22] и др. (см. также, например, работы [23] и [24, приложение]). Так, в [10] доказана неразрешимость логики бинарного предиката в языке с тремя предметными переменными, а используя переводы, описанные в [2, 3], можно получить неразрешимость (с учетом [22], $\Sigma _{1}^{0}$-трудность или $\Pi _{1}^{0}$-трудность) различных теорий бинарного предиката в языке с конечным (иногда, возможно, довольно большим) числом предметных переменных; идея, в первом приближении, состоит в том, чтобы в переводах элиминировать некоторые переменные при появлении в формулах вложенных кванторов, поступая примерно так, как это было сделано в определении формул вида ${{t}_{m}}(x)$, данном выше, когда в рекурсивном описании вместо очередной новой переменной берется уже использовавшаяся, но не имеющая свободных вхождений в ранее построенных формулах.

Также отметим, что в исследованиях (см., например, [1, 3]) уделяется большое внимание разрешимости фрагментов классической логики предикатов, определяемых кванторными префиксами из некоторого регулярного множества; если такое множество бесконечно, то в нем существуют сколь угодно длинные кванторные префиксы, а значит, соотвествующий фрагмент языка предполагает наличие бесконечного множества предметных переменных. Множества кванторных префиксов, для которых известна неразрешимость определяемых ими фрагментов логики бинарного предиката, бесконечны. Поэтому возникает естественный вопрос: можно ли извлечь из приведенного выше построения доказательство неразрешимости какого-либо фрагмента логики бинарного предиката, определяемого конечным множеством кванторных префиксов? Ответ здесь отрицательный: формулы вида $t_{m}^{y}(x)$ используют цепочки вложенных кванторов по переменным $x$ и $y$, причем длина этих цепочек зависит от $m$, поэтому, преобразуя формулы вида ${{t}_{T}}$ к префиксной нормальной форме, при росте числа элементов в T мы получим рост длины кванторной приставки, а значит, и рост числа переменных в получающейся формуле.

БЛАГОДАРНОСТИ

Автор выражает искреннюю благодарность анонимным рецензентам за их замечания и предложения, а также за обсуждение темы работы и результатов.

ИСТОЧНИК ФИНАНСИРОВАНИЯ

Исследования выполнены в ИППИ РАН при финансовой поддержке Российского научного фонда, грант 21-18-00195.