Сколемизация. 
Дискретный анализ. 
Формальные системы и алгоритмы

Теорема 3.69 показывает, что достаточно проверять выполнимость предварённых нормальных форм.

Следующий шаг состоит в том, чтобы упростить кванторную часть предварённой нормальной формы.

В общем случае кванторная часть содержит оба квантора V и 3- Мы хотим ограничиться случаем формул, в которых кванторная часть состоит из одинаковых кванторов. Этого невозможно добиться, если искать эквивалентные формулы в той же сигнатуре.

Пример 3.72. Докажем, что для формулы УхЗ уА (х, у) нет такой эквивалентной нормальной формы в сигнатуре {Л}, A G V-2, все кванторы которой одинаковы.

Для интерпретации формулы в сигнатуре {Л} нужно указать интерпретацию предикатного символа А как бинарного отношения на множестве М. Бинарное отношение можно представить наглядно, как ориентированный граф без кратных рёбер с множеством вершин М. Из вершины х в вершину у ведёт ребро тогда и только тогда, когда Л (х, у).

Формула /хЗуА (х, у) выражает такое свойство графа: «из каждой вершины выходит по крайней мере одно ребро». Любая формула с кванторами одного вида выражает некоторое свойство подграфов графа, количество вершин в которых фиксировано (оно равно количеству переменных в формуле).

Пусть формула Ф говорит о подграфах с числом вершин п. У ориентированного цикла на (п + 2)-х вершинах и ориентированного пути длины п (граф на п + 1 вершине) одинаковый набор подграфов с числом вершин п: путь длины п — 1 и несвязные объединения путей длин к и п — к — 2.

Формула Ф утверждает либо существование подграфа с каким-то свойством, либо выполнение некоторого свойства для всех подграфов. Поэтому она принимает одинаковое значение на двух указанных графах.

Так как формула /ж 3 уА (х, у) принимает разные значения на этих графах, она неэквивалентна Ф.

Определение 3.73. Предварённая нормальная форма, которая содержит только кванторы всеобщности, называется II] -формулой.

Чтобы перейти к Щ-формулам, будем расширять сигнатуру формулы, добавляя новые функциональные символы. Рассмотрим основной пример.

Пример 3.74. Выполнимость формулы S = V ж 3 уА (х, у) равносильна выполнимости формулы F = ЦхА (х, f (x)), где.

14 В.

/ — «новый» унарный функциональный символ, т. е. функциональный символ, который ПС входит в формулу А.

Действительно, пусть есть интерпретация М. с областью интерпретации М, в которой истинна формула S. Построим интерпретацию М с той же областью, в которой истинна формула F. Предикатный символ А интерпретируем так же, как в М. Интерпретацию символа / зададим следующим образом: для каждого элемента mi € М выберем такой элемент m2 € М, что [A](mi, m2), и определим [f](mi) как m2- Поскольку S истинна в интерпретации Л4, такой выбор возможен для любого mi.

В обратную сторону утверждение очевидно: если в интерпретации М. истинна формула F, то в той же интерпретации истинна и формула S.

Обобщая пример, сформулируем процедуру сколемизации формулы^[1]^. Пусть А замкнутая формула в предварённой нормальной форме, причём в кванторной части содержится квантор существования. Рассмотрим самый левый квантор существования Зу, обозначим количество кванторов всеобщности перед ним через к. Таким образом формула имеет вид.

последний случай отвечает к = 0.

Введём новый функциональный символ / арности к. Удалим из формулы квантор 3 х и заменим в бескванторной части формулы В все вхождения у на f (x 1,…, х^) или на / при к = 0. Получим новую замкнутую формулу С.

Будем повторять описанную выше процедуру до тех пор, пока не получим (замкнутую) Щ-формулу F. Она и называется сколемизацией исходной формулы.

Теорема 3.75 (Сколем). Выполнимость замкнутой формулы равносильна выполнимости её сколелшзации.

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

Повторим рассуждения из примера 3.74. Пусть есть интерпретация М с областью интерпретации А/, в которой истинна формула А. Построим интерпретацию М! с той же областью, в которой истинна формула С, построение которой из формулы А описано выше. Все предикатные и функциональные символы, входящие в А, интерпретируем точно так же, как в АЛ. Интерпретацию символа / зададим следующим образом: для каждого набора mi,…, € М

выберем такой mo € М, что [В] истинно на наборе свободных переменных, в котором х = mi, …, = rrik-

Поскольку А истинна в интерпретации Л4, такой выбор возможен для любого набора тх,…, т*. Определим теперь [f](mi,…, то*) как то-

В обратную сторону утверждение очевидно: если в интерпретации М истинна формула С, то в той же интерпретации истинна и формула А. ?

Иногда сколемизация формулы вообще не содержит переменных.

Пример 3.76. Пусть В = 3#(^4(#)—"Л (ж)). Сколемизацией формулы В является формула (А (с) —>Л (с)), где с — константа.

В общем случае сколемизация замкнутой формулы содержит столько переменных, сколько было кванторов всеобщности в исходной формуле. Это ясно из определения процедуры: каждая переменная, связанная квантором существования в исходной формуле, заменяется на новый функциональный символ.

• [1] Процедура названа в честь известного логика Т. Л. Сколема.