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

Метод исключения предложил логик Сколем. В его честь процесс исключения квантора назвали "сколемизацией".

Правила "сколемизации":

1. Если переменная х связана квантором существования х, который сам не находиться в области действия никакого квантора всеобщности, то х стирается, а все вхождения х, которые были связаны этим квантором, заменяются на новую "сколемовскую константу". Ее имя должно быть отлично от всех других.
х Q(x) Þ Q(a) х P(x, y) Þ P(a, y)
Константа а представляет собой некоторое (неизвестное) значения, для которого наше утверждение истинно. Важно то, что мы подставляем одно и то же неизвестное значение на все места, где используется х.

2. Если х находится в области действия кванторов всеобщности yхP(x,y), то а функционально зависит от y – a=f(y). В этом случае х стирается, а все вхождения х, которые были связаны этим квантором, заменяются на "сколемовскую функцию" f(y), тоже неизвестную, но везде одну и ту же.
yхP(x,y) Þ P(f(y), y)

Для конечного множества области определения y можно записать

yхP(x,y) = хP(x,y₁) & х P(x,y)... & х P(x,y_n) =

P(a₁, y₁) & P(a₂, y₂)... & P(a_n, y_n).

Константа а функционально зависит от y – a=f(y).

Пример

z P(z) & (y) ((x) Eq(y, plus(x, 1)) & x less(x, plus(x, y)))

1-ый шаг z убираем и заменяем z на а.

2-ой шаг x заменяем x на функцию f(y)

3-ой шаг x заменяем на x функцию g(y)

P(a) & (y) ((x) Eq(y, plus(f(y), 1)) & x less(g(y), plus(g(y), y)))

Дата добавления: 2014-01-07