2014 dxdy logo

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

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


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


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



Начать новую тему Ответить на тему
 
 введение и удаление общности в исчислении предикатов
Сообщение11.07.2021, 12:40 


23/04/18
143
Известно, что $A(x) \vdash \forall x A(x) $ и что $\forall x A(x) \vdash A(t)$, если $t$ свободно для $x$ в $A(x)$, откуда вытекает, что $\forall x A(x) \vdash A(x)$. При этом есть аксиома $\forall x A(x) \supset A(t)$ с тем же условием на $t$, откуда также вытекает $\forall x A(x) \supset A(x)$, но при этом насколько я понял, обратное, что $A(x) \supset \forall x A(x)$ не всегда верно в исчислении предикатов, а именно может быть неверно, если x варьируется в выводе $A(x) \vdash \forall x A(x) $. Не понимаю почему так, если по сути между высказываниями $A(x)$ и $\forall x A(x)$ нет никакой разницы кроме той, что в первом высказывании $x$ может содержаться свободно, а во втором не может. То есть эти высказывания должны быть равносильны. В чём подвох?

 Профиль  
                  
 
 Re: введение и удаление общности в исчислении предикатов
Сообщение11.07.2021, 14:35 


10/11/15
142
Paul Ivanov в сообщении #1525752 писал(а):
Известно, что $A(x) \vdash \forall x A(x) $


Это не верно. Возьмите, например, $x>2, x \in \mathbb{N}$, вместо $A(x)$. Верно следующее: если $\vdash A(x)$, то $\vdash \forall x A(x)$.

 Профиль  
                  
 
 Re: введение и удаление общности в исчислении предикатов
Сообщение11.07.2021, 14:58 


23/04/18
143
Это не верно только если рассматривать взятую вами формулу, как необязательно верную. Если же мы берём её за исходную (что подразумевает уже что $x>2, x \in \mathbb{N}$ - истина), то вывод в
формальной системе аксиом исчисления предикатов рассмотрен Клини во "Введении в метаматематику" на странице 92 и осуществляется по указанной странице в 6 шагов.

 Профиль  
                  
 
 Re: введение и удаление общности в исчислении предикатов
Сообщение11.07.2021, 17:57 


10/11/15
142
Не знаю, что там у Клини, не читал. Это не верно, учитывая определение квантора общности и логического следования, не верно на содержательном уровне, значит, не должно быть верно и на формальном уровне. Иначе какой смысл в такой формализации?

Гляньте: Крупский, Плиско, Математическая логика и теория алгоритмов.

-- 11.07.2021, 18:00 --

А книжку Клини посмотрю. Есть у меня такая. Спасибо.

-- 11.07.2021, 18:13 --

В выводе у Клини используется правило 9, которое верно только в таком виде: если $\vdash C \to A(x)$, то $\vdash C \to \forall x A(x)$, где $C$ не зависит от переменной $x$. По- моему то же самое есть в книге Мендельсона.

 Профиль  
                  
 
 Re: введение и удаление общности в исчислении предикатов
Сообщение11.07.2021, 19:59 


10/11/15
142
Да, у Мендельсона тоже есть правило обобщения, но нигде не указано, что это не логическое следование, а правило вывода в более слабом смысле.

 Профиль  
                  
 
 Re: введение и удаление общности в исчислении предикатов
Сообщение13.07.2021, 09:23 
Заслуженный участник
Аватара пользователя


28/09/06
10414
kernel1983 в сообщении #1525798 писал(а):
Да, у Мендельсона тоже есть правило обобщения, но нигде не указано, что это не логическое следование, а правило вывода в более слабом смысле.

$\varphi \vdash \forall x~\varphi$ - это и есть правило обобщения, каковое является одним из правил вывода в исчислении предикатов. Только это правило ограничено дополнительным условием - его нельзя применять в условном выводе, если $\varphi$ - гипотеза. Именно по этой причине импликация $\varphi \to \forall x~\varphi$ невыводима.

 Профиль  
                  
 
 Re: введение и удаление общности в исчислении предикатов
Сообщение16.07.2021, 16:06 


23/04/18
143
В книжке Клини не было никаких дополнительных условий на правило $\varphi \vdash \forall x \varphi$. Для вывода этого правила даже теорема дедукции не нужна. Вывод достаточно прост и в нём используется только модус поненс и правило введения общности из аксиом исчисления предикатов. Что вы имели в виду под условным выводом и гипотезой?
Если уж на то пошло мне также непонятно зачем вводятся правила введения $\forall$ и удаления $\exists$ вместо влечения $(c \supset \varphi) \supset (c \supset \forall x \varphi)$ и симметричного влечения для $\exists$ из которых эти правила выводятся посредством модус поненс. И почему бы не добавить $\varphi \supset \forall x \varphi$ в качестве аксиомы если это имеет самый непосредственный семантический смысл? Ведь у Клини под верностью $\varphi(x)$ подразумевается верность для произвольного, а значит для любого $x$

 Профиль  
                  
 
 Re: введение и удаление общности в исчислении предикатов
Сообщение16.07.2021, 16:31 
Заслуженный участник


20/07/09
4026
МФТИ ФУПМ
Paul Ivanov в сообщении #1526335 писал(а):
И почему бы не добавить $\varphi \supset \forall x \varphi$ в качестве аксиомы
Потому что это не общезначимая формула?

 Профиль  
                  
 
 Re: введение и удаление общности в исчислении предикатов
Сообщение16.07.2021, 21:54 
Аватара пользователя


01/12/06
697
рм
Paul Ivanov в сообщении #1525776 писал(а):
вывод в формальной системе аксиом исчисления предикатов рассмотрен Клини во "Введении в метаматематику" на странице 92 и осуществляется по указанной странице в 6 шагов
Этот вывод не является формальным доказательством, а формальным выводом из допущений. Это два разных понятия. В формальном выводе из допущений не все формулы вывода теоремы (в широком смысле). В формальном доказательстве каждая формула или аксиома, или доказываемая теорема.

 Профиль  
                  
 
 Re: введение и удаление общности в исчислении предикатов
Сообщение17.07.2021, 11:10 
Заслуженный участник
Аватара пользователя


28/09/06
10414
Paul Ivanov в сообщении #1526335 писал(а):
Для вывода этого правила даже теорема дедукции не нужна. Вывод достаточно прост и в нём используется только модус поненс и правило введения общности из аксиом исчисления предикатов.

Вы о чём? Правила вывода не выводятся, они - часть аксиоматики исчисления предикатов.

Paul Ivanov в сообщении #1526335 писал(а):
Что вы имели в виду под условным выводом и гипотезой?

Условный вывод начинается с некой гипотезы $\varphi$ и если с её использованием (подобно аксиоме) выведено некое $\psi$, то считается доказанной импликация $\varphi \to \psi$.

Paul Ivanov в сообщении #1526335 писал(а):
И почему бы не добавить $\varphi \supset \forall x \varphi$ в качестве аксиомы если это имеет самый непосредственный семантический смысл?

Ваш семантический смысл, очевидно, ошибочный, поскольку добавление такой схемы аксиом в исчисление предикатов мгновенно сделает его несостоятельным. Ибо $\varphi \to \forall x~\varphi$ означает $(\exists x~\varphi) \to (\forall x~\varphi)$, т.е. из существования $x=2$ следует, что все $x=2$.

Paul Ivanov в сообщении #1526335 писал(а):
Ведь у Клини под верностью $\varphi(x)$ подразумевается верность для произвольного, а значит для любого $x$

Разумеется, в этом и заключается правило обобщения. И без него исчислению предикатов никак не обойтись. Например, попробуйте без применения правила обобщения вывести такую тавтологию: $(\forall x~\varphi \to \psi) \to ((\forall x~\varphi) \to (\forall x~\psi))$.

 Профиль  
                  
 
 Re: введение и удаление общности в исчислении предикатов
Сообщение17.07.2021, 17:00 


23/04/18
143
Вроде понял, всем спасибо, epros, за этот пример очень благодарен, открыло глаза, как-то даже не предполагал,что из такого допущения сразу следует такая бессмыслица, поэтому не копал в этом направлении
Цитата:
Ибо $\varphi \to \forall x~\varphi$ означает $(\exists x~\varphi) \to (\forall x~\varphi)$, т.е. из существования $x=2$ следует, что все $x=2$.

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

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



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

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


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

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