Введение

Формализм логики первого порядка. В математической логике формула логики первого порядка находится в нормальной форме Сколема, если она представлена в пренексной нормальной форме и содержит только универсальные кванторы первого порядка. Любую формулу логики первого порядка можно преобразовать в нормальную форму Сколема, не изменяя её выполнимости, посредством процесса, называемого сколемизацией (иногда также сколемнизацией). Полученная формула не обязательно эквивалентна исходной, но эквиудовлетворима ей: она выполнима тогда и только тогда, когда выполнима исходная формула. Приведение к нормальной форме Сколема — это метод удаления экзистенциальных кванторов из формальных логических утверждений, часто выполняемый как первый шаг в автоматическом доказателе теорем.

Примеры

Простейшая форма сколемизации применяется к экзистенциально квантифицированным переменным, которые не находятся в области действия универсального квантора. Их можно заменить, просто вводя новые константы. Например, можно заменить на , где – новая константа (не встречающаяся больше нигде в формуле). В более общем случае, сколемизация выполняется путем замены каждой экзистенциально квантифицированной переменной на терм , символ функции которого является новым. Переменные этого терма определяются следующим образом. Если формула находится в пренексной нормальной форме, то – это переменные, которые универсально квантифицированы и кванторы которых предшествуют квантору . В общем случае, это переменные, которые квантифицированы универсально (мы предполагаем, что избавляемся от экзистенциальных кванторов последовательно, так что все экзистенциальные кванторы перед уже удалены) и такие, что встречается в области действия их кванторов. Функция, вводимая в этом процессе, называется функцией Сколема (или константой Сколема, если она имеет аритет 0), а терм – термом Сколема. Например, формула не находится в сколемизированной нормальной форме, поскольку содержит экзистенциальный квантор. Сколемизация заменяет на , где – новый символ функции, и удаляет квантификацию по . В результате получается формула . Терм Сколема содержит , но не , потому что квантор, который нужно удалить, находится в области действия , но не в области действия ; поскольку эта формула находится в пренексной нормальной форме, это эквивалентно тому, что в списке кванторов стоит перед , а – нет. Формула, полученная в результате этого преобразования, выполнима тогда и только тогда, когда исходная формула выполнима.

Использование школизации

Одно из применений сколемизации заключается в автоматическом доказательстве теорем. Например, в методе аналитических таблиц, когда встречается формула, ведущий квантор которой является экзистенциальным, может быть сгенерирована формула, полученная удалением этого квантора посредством сколемизации. Например, если встречается в таблице, где – свободные переменные , то можно добавить к той же ветви таблицы. Это добавление не изменяет выполнимость таблицы: каждая модель исходной формулы может быть расширена, добавив подходящую интерпретацию , до модели новой формулы. Эта форма сколемизации является улучшением по сравнению с «классической» сколемизацией, поскольку в сколемовский терм помещаются только переменные, свободные в формуле. Это улучшение обусловлено тем, что семантика таблиц может неявно поместить формулу в область действия некоторых всеобщих кванторов, которых нет в самой формуле; эти переменные не входят в сколемовский терм, в то время как они бы там оказались согласно исходному определению сколемизации. Другое улучшение, которое можно использовать, – применение одного и того же символа сколемовской функции к формулам, которые идентичны с точностью до переименования переменных. Еще одно применение – в методе резолюций для логики первого порядка, где формулы представляются в виде наборов клауз, понимаемых как всеобщие кванторы. (Пример – парадокс пьющего). Важным результатом в теории моделей является теорема Лёвенгейма — Сколема, которая может быть доказана посредством сколемизации теории и замыкания относительно полученных сколемовских функций.

Теории Сколема

В общем, если T – теория и для каждой формулы со свободными переменными существует n-арный символ функции f, который доказуемо является функцией Сколема для T, то T называется теорией Сколема. Каждая теория Сколема является полно-модельной, то есть каждая подструктура модели является элементарной подструктурой. Для модели M теории Сколема T, наименьшая подструктура, содержащая некоторое множество A, называется корпусом Сколема множества A. Корпус Сколема множества A является атомной простой моделью над A.

История

Нормальная форма Сколема названа в честь покойного норвежского математика Торальфа Сколема.