введение и удаление общности в исчислении предикатов

[Paul Ivanov]

Известно, что $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$ может содержаться свободно, а во втором не может. То есть эти высказывания должны быть равносильны. В чём подвох?

[kernel1983]

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)$.

[Paul Ivanov]

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

[kernel1983]

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

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

-- 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$. По- моему то же самое есть в книге Мендельсона.

[kernel1983]

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

[epros]

kernel1983 в сообщении #1525798 писал(а):

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

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

[Paul Ivanov]

В книжке Клини не было никаких дополнительных условий на правило $\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$

[Nemiroff]

Paul Ivanov в сообщении #1526335 писал(а):

И почему бы не добавить $\varphi \supset \forall x \varphi$ в качестве аксиомы

Потому что это не общезначимая формула?

[gefest_md]

Paul Ivanov в сообщении #1525776 писал(а):

вывод в формальной системе аксиом исчисления предикатов рассмотрен Клини во "Введении в метаматематику" на странице 92 и осуществляется по указанной странице в 6 шагов

Этот вывод не является формальным доказательством, а формальным выводом из допущений. Это два разных понятия. В формальном выводе из допущений не все формулы вывода теоремы (в широком смысле). В формальном доказательстве каждая формула или аксиома, или доказываемая теорема.

[epros]

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))$.

[Paul Ivanov]

Вроде понял, всем спасибо, epros, за этот пример очень благодарен, открыло глаза, как-то даже не предполагал,что из такого допущения сразу следует такая бессмыслица, поэтому не копал в этом направлении

Цитата:

Ибо $\varphi \to \forall x~\varphi$ означает $(\exists x~\varphi) \to (\forall x~\varphi)$, т.е. из существования $x=2$ следует, что все $x=2$.