Скулемизация

[nbyte]

Здравствуйте.
Хочу разобраться что такое скулемизация.
Пробовал искать по литературу, но как-то этот термин нигде не встречается.
Готовлюсь к экзамену и вижу что в экзамене прошлых лет есть вопрос

Цитата:

Скулемизируйте $\exists {x_1}\forall {y_1}\exists {x_2}\forall {y_2}P({x_1},{x_2},{x_3},{y_1},{y_2})$

Подскажите пожалуйста как его следует решать?
Где-бы я мог найти руководство к решению таких задач?
И как правильно набрать символ в TeX'е?

[AD]

\vdash $\vdash$.
См. также мою новую подпись

[nbyte]

Нашел в википедии http://en.wikipedia.org/wiki/Skolem_normal_form статью на английском языке, но а как тогда это дело на русском языке называться?
И как толком понять

это преобразование? Для чего оно нужно?

[AD]

Это преобразование формализует некий весьма часто встречающийся набор слов:

"итак, мы доказали, что для каждого $x$ существует такой $y$, что (...). Обозначим какой-нибудь из этих $y$ символом $f(x)$."

[nbyte]

Тогда опираясь на этот пример, я попробую как-то решить свой постепенно

Есть
$\vdash \exists {x_1}\forall {y_1}\exists {x_2}\forall {y_2}P({x_1},{x_2},{x_3},{y_1},{y_2})$
Сначала хочу понятно что именно я тут имею
Думаю, что в словесной форме будет так
Существует $x_1$ для каждого $y_1$ для которого в свою очередь существует $x_2$ для каждого $y_2$ предикат $\exists {x_1}\forall {y_1}\exists {x_2}\forall {y_2}P({x_1},{x_2},{x_3},{y_1},{y_2})$ который в свою очередь с ними истинный?
Или как тут?
И можно-ли кванторы переставлять местами?

[mkot]

nbyte в сообщении #331828 писал(а):

Подскажите пожалуйста как его следует решать?
Где-бы я мог найти руководство к решению таких задач?

Мне всегда казалось, что процесс скулемизации чисто механический и думать не надо.
А достаточно хорошо про скулемизацию рассказано в книге Верещагина, Шеня "Языки и исчисления", которую легко найти в интернете.

[nbyte]

Вроде-бы уловил суть
Проверьте пожалуйста
$\exists {x_1}\forall {y_1}\exists {x_2}\forall {y_2}P({x_1},{x_2},{x_3},{y_1},{y_2})$
будет
$\exists {x_1}\exists {x_2}P({x_1},{x_2},{x_3},f({x_1}),g({x_2}))$
mkot, спасибо Вам за книжку. Первыя толковая книжка, которая мне попалась по грядущему экзамену

[mkot]

nbyte в сообщении #332000 писал(а):

Вроде-бы уловил суть
Проверьте пожалуйста
$\exists {x_1}\forall {y_1}\exists {x_2}\forall {y_2}P({x_1},{x_2},{x_3},{y_1},{y_2})$
будет
$\exists {x_1}\exists {x_2}P({x_1},{x_2},{x_3},f({x_1}),g({x_2}))$

Ну нет же, совсем нет.

У вас должна получиться универсальная формула, то есть все кванторы -- "для любого", и с функциями тоже не порядок. Алгоритм же для предложений следующий:
(1) Приводите формулу к пренексной нормальной форме.
(2) Начинаете смотреть на кванторную приставку слева направо. Если находите квантор существования, то его убираете, а вхождение переменной, которую он связывал, заменяете на функцию от переменных, которые связаны кванторами всеобщности слева от него, если же тот квантор существования первый, то ясно дело нужно вместо функции использовать константу.

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

[nbyte]

mkot в сообщении #332072 писал(а):

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

Проверил, у меня без опечатки.

Может тогда вот так

будет
$\forall {y_1}\forall {y_2}P(a,f({y_1}),{x_3},{y_1},{y_2})$

[nbyte]

[mkot]

Не будь свободный переменных так оно и было б. А раз они есть, то, как мне кажется, от них вводимые функции тоже должны зависеть, если это не так, то пусть меня поправят.

[Профессор Снэйп]

nbyte в сообщении #331828 писал(а):

Хочу разобраться что такое скулемизация.

Сколемизация --- это процесс обогащения модели путём введения в сигнатуру новых функциональных и константных символов, позволяющий для каждой формулы обогащённой модели записать эквивалентную её универсальную формулу (то есть формулу в пренексной нормальной форме, содержащую только кванторы всеобщности). Элементарная теория модели, подвергшейся процедуре сколемизации, является модельно полной и, следовательно, для любой пары моделей этой теории всякое изоморфное вложение первой модели во вторую является элементарным.

Короче, всё очень просто. Вот есть у нас модель $\mathfrak{M}$ некоторого языка $L_0$ и пусть $\Psi(\bar{x}) = \exists y \Phi(\bar{x}, y)$ --- формула языка $L_0$, начинающаяся с квантора существования. Вводим для неё новый функциональный символ $f_\Psi$ и интерпретируем его на носителе модели так, чтобы было выполнено $\mathfrak{M} \models \forall \bar{x} (\Psi(\bar{x}) \leftrightarrow \Phi(\bar{x}, f(\bar{x}))$. Когда проделаем это для каждой формулы, получаем модель нового языка $L_1$, являющуюся обогащением старой. Далее проделываем всю эту байду снова, но уже с языком $L_1$, получаем новое обогащение и язык $L_2$. Далее по индукции язык $L_3$, $L_4$ и т. д. Наконец, определив для каждого натурального $n$ язык $L_n$, берём язык $L_\omega = \bigcup_{n \in \mathbb{N}} L_n$ и рассматриваем $\mathfrak{M}$ как модель языка $L_\omega$. Вот это и есть сколемизация.

Зачем это нужно? Ну, например, для доказательства теоремы Левенгейма-Сколема (которая вниз). Например, есть у нас бесконечная модель $\mathfrak{M}$ счётного языка и счётное подмножество носителя $X_0$. Ясно, что в процессе сколемизации мы введём лишь счётное число новых функциональных символов. Теперь для всех натуральных $n$ полагаем $X_{n+1} = \{ f(\bar{x}) : \bar{x} \in X_n, \, f \text{ --- введённый в процессе сколемизации функциональный символ} \}$ и $X_\omega = \bigcup_{n \in \mathbb{N}} X_n$. Получаем, что $X_\omega$ --- счётное подмножество носителя исходной модели, содержащее $X_0$ и выделяющее элементарную подмодель.

[senseless]

А если первый квантор - существования, все вхождения зависимой переменной заменяем на одну константу или на разные?

[Профессор Снэйп]

На одну и ту же для каждого квантора.Для разных кванторов -на разные.