Шолем нормальная форма

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

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

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

Примеры

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

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

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

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

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

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

где

$f(x)$ это функция, которая отображает $x$ к $y$.

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

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

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

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

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

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

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

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

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

Теории Шолема

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

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

История

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

См. также

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

Ссылки

• Ходжес, Уилфрид (1997), Более короткая теория моделей , издательство Кембриджского университета , ISBN  978-0-521-58713-6

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

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