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

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

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

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

Простейшая форма сколемизации предназначена для экзистенциально квантифицированных переменных, которые не входят в область действия универсального квантификатора. Их можно заменить, просто создав новые константы. Например, может быть изменено на , где — новая константа (больше нигде в формуле не встречается). ${\ Displaystyle \ существует хР (х)}$ ${\ Displaystyle Р (с)}$ ${\ Displaystyle с}$

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