В математической логике , формула из логики первого порядка в сколемовской нормальной форме , если она находится в предваренной нормальной форме с только кванторами всеобщности первого порядка .
Каждая формула первого порядка может быть преобразована в нормальную форму Сколема без изменения ее выполнимости с помощью процесса, называемого Сколемизация (иногда пишется Сколемнизация ). Результирующая формула не обязательно эквивалентна исходной, но равносильна ей: она выполнима тогда и только тогда, когда выполнима исходная формула. [1]
Приведение к нормальной форме Сколема - это метод удаления кванторов существования из утверждений формальной логики , часто выполняемый в качестве первого шага в автоматическом средстве доказательства теорем .
Примеры
Простейшая форма сколемизации предназначена для экзистенциально количественно определяемых переменных, которые не входят в область действия универсального квантора. Их можно заменить, просто создав новые константы. Например, может быть изменен на , где - новая константа (больше нигде в формуле не встречается).
В более общем смысле, сколемизация выполняется путем замены каждой экзистенциально количественно определяемой переменной. со сроком чей функциональный символ новый. Переменные этого члена следующие. Если формула находится в предваренной нормальной форме , то являются переменными, которые универсально количественно определены и чьи кванторы предшествуют кванторам . В общем, это переменные, которые количественно оцениваются универсально (мы предполагаем, что мы избавляемся от экзистенциальных кванторов по порядку, поэтому все экзистенциальные кванторы до были удалены) и такие, что происходит в рамках их кванторов. Функциявведенный в этом процессе, называется функцией Сколема (или константой Сколема, если она имеет нулевую арность ), а термин называется термином Сколема .
Например, формула не в сколемской нормальной форме, потому что содержит квантор существования . Сколемизация заменяет с участием , где является новым функциональным символом и удаляет количественную оценку . Результирующая формула. Сколемский термин содержит , но нет , потому что квантор, который нужно удалить входит в сферу , но не в том ; поскольку эта формула находится в предваренной нормальной форме, это эквивалентно тому, что в списке кванторов предшествует пока не. Формула, полученная этим преобразованием, выполнима тогда и только тогда, когда исходная формула.
Как работает сколемизация
Сколемизация работает, применяя эквивалентность второго порядка в сочетании с определением выполнимости первого порядка. Эквивалентность дает возможность «переместить» квантор существования перед универсальным.
где
- это функция, которая отображает к .
Интуитивно понятно, что предложение «для каждого существует такой, что "преобразуется в эквивалентную форму" существует функция отображение каждого в так что для каждого он держит ".
Эта эквивалентность полезна, потому что определение выполнимости первого порядка неявно экзистенциально дает количественную оценку по сравнению с оценкой функциональных символов. В частности, формула первого порядка выполнимо, если существует модель и оценка свободных переменных формулы, которые оценивают формулу как истинную . Модель содержит оценку всех функциональных символов; следовательно, сколемские функции неявно количественно оцениваются экзистенциально. В приведенном выше примере выполнимо тогда и только тогда, когда существует модель , который содержит оценку для , так что верно для некоторой оценки его свободных переменных (в данном случае нет). Это может быть выражено во втором порядке как. По указанной выше эквивалентности это то же самое, что выполнимость.
На мета-уровне выполнимость первого порядка формулы может быть записан с небольшим злоупотреблением обозначениями как , где модель, оценка свободных переменных, и Значит это верно в под . Поскольку модели первого порядка содержат вычисление всех функциональных символов, любая функция Сколема, которая содержит неявно экзистенциально количественно оценивается . В результате, после замены кванторов существования над переменными кванторами существования над функциями в начале формулы, формула по-прежнему может рассматриваться как формула первого порядка путем удаления этих кванторов существования. Этот последний шаг лечения в виде может быть завершено, потому что функции неявно экзистенциально оцениваются количественно в определении выполнимости первого порядка.
Правильность сколемизации можно показать на примере формулы следующим образом. Этой формуле удовлетворяет модель тогда и только тогда, когда для каждого возможного значения для в области модели существует значение для в области модели, которая делает правда. По выбранной аксиоме существует функция такой, что . В результате формула является выполнимым, потому что у него есть модель, полученная путем добавления оценки к . Это показывает, что выполнимо, только если также выполнимо. Наоборот, если выполнимо, то существует модель это его удовлетворяет; эта модель включает оценку функции так что для каждого значения , формула держит. Как результат, удовлетворяется той же моделью, потому что можно выбрать для каждого значения , Значение , где оценивается в соответствии с .
Использование сколемизации
Одно из применений сколемизации - автоматическое доказательство теорем . Например, в методе аналитических таблиц всякий раз, когда встречается формула, чей ведущий квантор является экзистенциальным, может быть сгенерирована формула, полученная путем удаления этого квантора посредством сколемизации. Например, если встречается в таблице, где свободные переменные , тогда может быть добавлен в ту же ветку таблицы. Это добавление не меняет выполнимости таблицы: каждая модель старой формулы может быть расширена путем добавления подходящей оценки, к модели новой формулы.
Эта форма сколемизации является усовершенствованием по сравнению с «классической» сколемизацией в том смысле, что только переменные, которые свободны в формуле, помещаются в термин «сколем». Это улучшение, потому что семантика tableau может неявно помещать формулу в область действия некоторых универсально количественно определяемых переменных, которых нет в самой формуле; эти переменные не входят в термин «сколем», хотя они должны присутствовать в соответствии с исходным определением «сколемизации». Другое улучшение, которое можно использовать, - это применение того же символа функции Сколема для формул, которые идентичны до переименования переменных. [2]
Другое использование - метод разрешения для логики первого порядка , где формулы представлены в виде наборов предложений, которые понимаются как универсальные количественные. (Например, см. Парадокс пьющего .)
Сколемские теории
В общем, если является теорией и для каждой формулы со свободными переменными есть символ функции что доказуемо является функцией Сколема для , тогда называется сколемской теорией . [3]
Каждая теория Сколема является завершенной моделью , т.е. каждая подструктура модели является элементарной подструктурой . Учитывая модель M из сколемовской теории Т , наименьшему подструктуры , содержащей определенный набор называется Skolem корпус из A . Skolem корпус А представляет собой атомную простая модель над A .
История
Нормальная форма Сколема названа в честь покойного норвежского математика Торальфа Сколема .
Смотрите также
- Гербрандизация , двойник сколемизации
- Логика предикатного функтора
Заметки
- ^ «Нормальные формы и сколемизация» (PDF) . Макс Планк Институт информатики . Проверено 15 декабря 2012 года .
- ^ Р. Хенле. Таблицы и родственные методы. Справочник по автоматическому мышлению .
- ^ «Множества, модели и доказательства» (3.3) И. Мурдейка и Дж. Ван Остена
Рекомендации
- Ходжес, Уилфрид (1997), теория более короткой модели , Cambridge University Press , ISBN 978-0-521-58713-6
Внешние ссылки
- "Сколемская функция" , Математическая энциклопедия , EMS Press , 2001 [1994]
- Сколемизация на PlanetMath.org
- Сколемизация Гектором Зенилом, Демонстрационный проект Вольфрама .
- Вайсштейн, Эрик В. "СколемизедФорм" . MathWorld .