Сколемовские функции

[kernel1983]

Можно ли как-то объяснить введение сколемовских функций, не прибегая к помощи логики предикатов второго порядка? Насколько я понимаю, $\forall x \exists y P(x,y) \simeq \exists f \forall y P(x,f(x))$. Если нет, то как доказать экивалентность выполнимости формул $\forall x \exists y P(x,y)$ и $\forall y P(x,f(x))$? Дайте хотя бы идею. Спасибо.

[kernel1983]

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

-- 21.02.2017, 12:41 --

Ясно, что выражение "для любого $x$ найдётся $y$" символизирует зависимость $x$ от $y$. Но как это обосновать, если не вводить по определению?

[george66]

В таком виде никак, надо использовать двойственный подход (эрбрановские функции, теорема Эрбрана). Возьмём формулу
\exists x \forall y P(x,y)
Возьмём её отрицание
\forall x \exists y \not P(x,y)
Вводим сколемовскую функцию
\exists f \forall x \not P(x,f(x))
Берём отрицание того, что получилось
\forall f \exists x P(x,f(x))
и убираем передний \forall, считая f новой функциональной константой, про которую ничего не известно
\exists x P(x,f(x))
Полученная формула, если я правильно помню (могу детали спутать), выводима в классическом исчислении предикатов если и только если выводима исходная. Подробности в книге Верещагин, Шень "Языки и исчисления" на слова "теорема Эрбрана"

[kernel1983]

george66 в сообщении #1194870 писал(а):

Подробности в книге Верещагин, Шень "Языки и исчисления" на слова "теорема Эрбрана"

Спасибо. Посмотрю.

[Lia]

george66
Замечание за неоформление формул. Всего-то долларов не хватило по краям.

[george66]

Вот, я теперь знаю, как здесь оформлять формулы.
Есть ещё такой результат: допустим, мы доказали формулу
$\forall x\exists y P(x,y)$
Тогда мы можем добавить новый функциональный символ f и новую аксиому
$\forall x P(x,f(x))$
и во многих случаях полученная теория оказывается "консервативна" над старой (то есть, в ней доказуемы только те формулы без символа f, которые были доказуемы раньше). На эту тему наверняка написано у Верещагина и Шеня в разделе про скулемовские функции.
Если же мы не доказали
$\forall x\exists y P(x,y)$
то работает только двойственный скулемовскому метод Эрбрана, когда убираются чередования кванторов
$\exists x\forall y P(x,y)$
путём замены на
$\exists x P(x,f(x))$
где f -- новый функциональный символ.

[Lia]

george66 в сообщении #1195139 писал(а):

Вот, я теперь знаю, как здесь оформлять формулы.

«Краткий FAQ по тегу [math]»

Всегда есть ссылка слева от окна ответа на сообщение.