Сколемская нормальная форма

Формализм логики первого порядка

В математической логике формула логики первого порядка находится в нормальной форме Скулема , если она находится в предваренной нормальной форме только с универсальными кванторами первого порядка .

Каждая формула первого порядка может быть преобразована в нормальную форму Скулема, не меняя при этом ее выполнимость с помощью процесса, называемого Скулемизацией (иногда пишется как Сколемнизация ). Полученная формула не обязательно эквивалентна исходной, но равновыполнима с ней: она выполнима тогда и только тогда, когда исходная выполнима. ^[1]

Приведение к нормальной форме Скулема — это метод удаления кванторов существования из утверждений формальной логики , часто выполняемый в качестве первого шага в автоматизированном доказательстве теорем .

Примеры

Самая простая форма скулемизации — для экзистенциально квантифицированных переменных, которые не входят в область действия универсального квантификатора. Их можно заменить, просто создав новые константы. Например, можно изменить на , где — новая константа (больше нигде в формуле не встречается). ${\displaystyle \exists xP(x)}$ ${\displaystyle P(c)}$ ${\displaystyle c}$

В более общем смысле, скулемизация выполняется путем замены каждой экзистенциально квантифицированной переменной на термин , функциональный символ которого является новым. Переменные этого термина следующие. Если формула находится в пренексной нормальной форме , то — это переменные, которые универсально квантифицированы и чьи квантификаторы предшествуют квантификатору . В общем случае это переменные, которые универсально квантифицированы (мы предполагаем, что мы избавляемся от экзистенциальных квантификаторов по порядку, поэтому все экзистенциальные квантификаторы до этого были удалены) и такие, что встречается в области действия их квантификаторов. Функция , введенная в этом процессе, называется функцией Скулема (или константой Скулема, если она имеет нулевую арность ), а термин называется термином Скулема . ${\displaystyle y}$ ${\displaystyle f(x_{1},\ldots ,x_{n})}$ ${\displaystyle f}$ ${\displaystyle x_{1},\ldots ,x_{n}}$ ${\displaystyle y}$ ${\displaystyle \exists y}$ ${\displaystyle \exists y}$ ${\displaystyle f}$

Например, формула не находится в нормальной форме Сколема, поскольку содержит квантор существования . Сколемизация заменяется на , где — новый символ функции, и удаляет квантификацию по . Результирующая формула — . Термин Сколема содержит , но не , поскольку удаляемый квантор находится в области действия , но не в области действия ; поскольку эта формула находится в нормальной форме предшествования, это эквивалентно утверждению, что в списке кванторов предшествует , а не нет. Формула, полученная в результате этого преобразования, выполнима тогда и только тогда, когда исходная формула является. ${\displaystyle \forall x\exists y\forall zP(x,y,z)}$ ${\displaystyle \exists y}$ ${\displaystyle y}$ ${\displaystyle f(x)}$ ${\displaystyle f}$ ${\displaystyle y}$ ${\displaystyle \forall x\forall zP(x,f(x),z)}$ ${\displaystyle f(x)}$ ${\displaystyle x}$ ${\displaystyle z}$ ${\displaystyle \exists y}$ ${\displaystyle \forall x}$ ${\displaystyle \forall z}$ ${\displaystyle x}$ ${\displaystyle y}$ ${\displaystyle z}$

Как работает сколемизация

Сколемизация работает, применяя эквивалентность второго порядка вместе с определением выполнимости первого порядка. Эквивалентность обеспечивает способ «перемещения» квантора существования перед квантором всеобщности.

${\displaystyle \forall x\exists yR(x,y)\iff \exists f\forall xR(x,f(x))}$

где

${\displaystyle f(x)}$— это функция, которая отображается на . ${\displaystyle x}$ ${\displaystyle y}$

Интуитивно предложение «для каждого существует такое , что » преобразуется в эквивалентную форму «существует функция, отображающая каждое в такое, что для каждого выполняется следующее ». ${\displaystyle x}$ ${\displaystyle y}$ ${\displaystyle R(x,y)}$ ${\displaystyle f}$ ${\displaystyle x}$ ${\displaystyle y}$ ${\displaystyle x}$ ${\displaystyle R(x,f(x))}$

Эта эквивалентность полезна, поскольку определение выполнимости первого порядка неявно экзистенциально квантифицирует по функциям, интерпретирующим символы функций. В частности, формула первого порядка выполнима, если существует модель и оценка свободных переменных формулы, которые оценивают формулу как истинную . Модель содержит интерпретацию всех символов функций; поэтому функции Скулема неявно экзистенциально квантифицируются. В приведенном выше примере выполнима тогда и только тогда, когда существует модель , которая содержит интерпретацию для , такую, что является истинной для некоторой оценки ее свободных переменных (ни одной в данном случае). Это может быть выражено во втором порядке как . Согласно приведенной выше эквивалентности это то же самое, что и выполнимость . ${\displaystyle \Phi }$ ${\displaystyle M}$ ${\displaystyle \mu }$ ${\displaystyle \forall xR(x,f(x))}$ ${\displaystyle M}$ ${\displaystyle f}$ ${\displaystyle \forall xR(x,f(x))}$ ${\displaystyle \exists f\forall xR(x,f(x))}$ ${\displaystyle \forall x\exists yR(x,y)}$

На метауровне выполнимость формулы первого порядка может быть записана с небольшим злоупотреблением обозначениями как , где — модель, — оценка свободных переменных, а означает, что истинно в под . Поскольку модели первого порядка содержат интерпретацию всех символов функций, любая функция Скулема, которая содержит , неявно экзистенциально квантифицируется с помощью . В результате, после замены квантификаторов существования по переменным на квантификаторы существования по функциям в начале формулы, формулу по-прежнему можно рассматривать как формулу первого порядка, удалив эти квантификаторы существования. Этот последний шаг рассмотрения как может быть завершен, поскольку функции неявно экзистенциально квантифицируются с помощью в определении выполнимости первого порядка. ${\displaystyle \Phi }$ ${\displaystyle \exists M\exists \mu (M,\mu \models \Phi )}$ ${\displaystyle M}$ ${\displaystyle \mu }$ ${\displaystyle \models }$ ${\displaystyle \Phi }$ ${\displaystyle M}$ ${\displaystyle \mu }$ ${\displaystyle \Phi }$ ${\displaystyle \exists M}$ ${\displaystyle \exists f\forall xR(x,f(x))}$ ${\displaystyle \forall xR(x,f(x))}$ ${\displaystyle \exists M}$

Корректность скулемизации может быть показана на примере формулы следующим образом. Эта формула удовлетворяется моделью тогда и только тогда, когда для каждого возможного значения для в области определения модели существует значение для в области определения модели, которое делает истинным. По аксиоме выбора существует функция такая, что . В результате формула выполнима, поскольку она имеет модель, полученную путем добавления интерпретации к . Это показывает, что выполнима, только если также выполнима. Наоборот, если выполнима, то существует модель , которая ее удовлетворяет; эта модель включает интерпретацию для функции, такую, что для каждого значения формула верна. В результате удовлетворяется той же моделью, поскольку для каждого значения можно выбрать значение , где оценивается согласно . ${\displaystyle F_{1}=\forall x_{1}\dots \forall x_{n}\exists yR(x_{1},\dots ,x_{n},y)}$ ${\displaystyle M}$ ${\displaystyle x_{1},\dots ,x_{n}}$ ${\displaystyle y}$ ${\displaystyle R(x_{1},\dots ,x_{n},y)}$ ${\displaystyle f}$ ${\displaystyle y=f(x_{1},\dots ,x_{n})}$ ${\displaystyle F_{2}=\forall x_{1}\dots \forall x_{n}R(x_{1},\dots ,x_{n},f(x_{1},\dots ,x_{n}))}$ ${\displaystyle f}$ ${\displaystyle M}$ ${\displaystyle F_{1}}$ ${\displaystyle F_{2}}$ ${\displaystyle F_{2}}$ ${\displaystyle M'}$ ${\displaystyle f}$ ${\displaystyle x_{1},\dots ,x_{n}}$ ${\displaystyle R(x_{1},\dots ,x_{n},f(x_{1},\dots ,x_{n}))}$ ${\displaystyle F_{1}}$ ${\displaystyle x_{1},\ldots ,x_{n}}$ ${\displaystyle y=f(x_{1},\dots ,x_{n})}$ ${\displaystyle f}$ ${\displaystyle M'}$

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

Одно из применений скулемизации — автоматическое доказательство теорем . Например, в методе аналитических таблиц всякий раз, когда встречается формула, ведущий квантификатор которой является экзистенциальным, может быть сгенерирована формула, полученная путем удаления этого квантификатора с помощью скулемизации. Например, если встречается в таблице, где — свободные переменные , то может быть добавлено к той же ветви таблицы. Это добавление не изменяет выполнимости таблицы: каждая модель старой формулы может быть расширена путем добавления подходящей интерпретации к модели новой формулы. ${\displaystyle \exists x\Phi (x,y_{1},\ldots ,y_{n})}$ ${\displaystyle x,y_{1},\ldots ,y_{n}}$ ${\displaystyle \Phi (x,y_{1},\ldots ,y_{n})}$ ${\displaystyle \Phi (f(y_{1},\ldots ,y_{n}),y_{1},\ldots ,y_{n})}$ ${\displaystyle f}$

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

Другое применение — метод разрешения для логики первого порядка , где формулы представлены как наборы предложений, которые считаются универсально квантифицированными. (Пример см. в парадоксе пьющего .)

Важным результатом в теории моделей является теорема Лёвенгейма–Скулема , которую можно доказать с помощью скулемизации теории и замыкания ее относительно полученных функций Скулема. ^[3]

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

В общем случае, если — теория и для каждой формулы со свободными переменными существует символ n -арной функции , который, как доказуемо, является функцией Скулема для , то это называется теорией Скулема . ^[4] ${\displaystyle T}$ ${\displaystyle x_{1},\dots ,x_{n},y}$ ${\displaystyle F}$ ${\displaystyle y}$ ${\displaystyle T}$

Каждая теория Скулема является модельно полной , т.е. каждая подструктура модели является элементарной подструктурой . Для модели M теории Скулема T наименьшая подструктура M , содержащая определенное множество A , называется оболочкой Скулема для A. Оболочка Скулема для A является атомарной простой моделью над A.

История

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

Смотрите также

• Гербрендизация , двойник сколемизации
• Логика предикатного функтора

Примечания

1. «Нормальные формы и сколемизация» (PDF) . Институт Макса Планка по информатике . Проверено 15 декабря 2012 г.
2. Райнер Хэнле. Таблицы и родственные методы. Справочник по автоматизированному рассуждению .
3. Скотт Вайнштейн, Теорема Левенгейма-Сколема, заметки к лекциям (2009). Доступ 6 января 2023 г.
4. «Наборы, модели и доказательства» (3.3) И. Мурдейка и Дж. ван Остена

Ссылки

• Ходжес, Уилфрид (1997), Теория более короткой модели , Cambridge University Press , ISBN 978-0-521-58713-6

Внешние ссылки

• «Функция Сколема», Энциклопедия математики , EMS Press , 2001 [1994]
• Сколемизация на PlanetMath.org
• Сколемизация Гектора Зенила, Демонстрационный проект Вольфрама .
• Вайсштейн, Эрик В. «Сколемизированная форма». Математический мир .