Исключение кванторов существования

В формуле , которую можно интерпретировать, например, как «для всех x существует такой y, что для x не больше y», квантор $y находится внутри области действия квантора "x. Поэтому y, который «существует», может зависеть от x. Эту зависимость в явной форме можно определить функцией g(x), отображающей каждое значение x в y. Такая функция называется функцией Сколема. Используя её, можно исключить квантор существования. Для обозначения функции Сколема не должны использоваться функциональные буквы, которые уже имеются в формуле. Если квантор существования находится в области действия двух и более кванторов общности, то функция Сколема будет зависеть соответственно от двух аргументов и более.

Если исключаемый квантор существования не принадлежит ни к одному квантору общности, то функция Сколема не содержит аргумента, т.е. является константой. Так, формула при исключении квантора существования преобразуется в формулу F(a), где а – константа, при которой известно, что формула F(a) «существует».

Операция исключения квантора существования называется ещё сколемизацией.