2014 dxdy logo

Научный форум dxdy

Математика, Физика, Computer Science, Machine Learning, LaTeX, Механика и Техника, Химия,
Биология и Медицина, Экономика и Финансовая Математика, Гуманитарные науки


Правила форума


Посмотреть правила форума



Начать новую тему Ответить на тему
 
 Сколемовские функции
Сообщение19.02.2017, 00:46 


10/11/15
142
Можно ли как-то объяснить введение сколемовских функций, не прибегая к помощи логики предикатов второго порядка? Насколько я понимаю, $\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))$? Дайте хотя бы идею. Спасибо.

 Профиль  
                  
 
 Re: Сколемовские функции
Сообщение21.02.2017, 12:39 


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

-- 21.02.2017, 12:41 --

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

 Профиль  
                  
 
 Re: Сколемовские функции
Сообщение23.02.2017, 23:07 
Заслуженный участник


31/12/15
922
В таком виде никак, надо использовать двойственный подход (эрбрановские функции, теорема Эрбрана). Возьмём формулу
\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))
Полученная формула, если я правильно помню (могу детали спутать), выводима в классическом исчислении предикатов если и только если выводима исходная. Подробности в книге Верещагин, Шень "Языки и исчисления" на слова "теорема Эрбрана"

 Профиль  
                  
 
 Re: Сколемовские функции
Сообщение24.02.2017, 12:19 


10/11/15
142
george66 в сообщении #1194870 писал(а):
Подробности в книге Верещагин, Шень "Языки и исчисления" на слова "теорема Эрбрана"


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

 Профиль  
                  
 
 Re: Сколемовские функции
Сообщение24.02.2017, 18:55 


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

 Профиль  
                  
 
 Re: Сколемовские функции
Сообщение24.02.2017, 19:50 
Заслуженный участник


31/12/15
922
Вот, я теперь знаю, как здесь оформлять формулы.
Есть ещё такой результат: допустим, мы доказали формулу
$\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 -- новый функциональный символ.

 Профиль  
                  
 
 Re: Сколемовские функции
Сообщение24.02.2017, 19:54 


20/03/14
12041
 i 
george66 в сообщении #1195139 писал(а):
Вот, я теперь знаю, как здесь оформлять формулы.

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


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

 Профиль  
                  
Показать сообщения за:  Поле сортировки  
Начать новую тему Ответить на тему  [ Сообщений: 7 ] 

Модераторы: Модераторы Математики, Супермодераторы



Кто сейчас на конференции

Сейчас этот форум просматривают: нет зарегистрированных пользователей


Вы не можете начинать темы
Вы не можете отвечать на сообщения
Вы не можете редактировать свои сообщения
Вы не можете удалять свои сообщения
Вы не можете добавлять вложения

Найти:
Powered by phpBB © 2000, 2002, 2005, 2007 phpBB Group