Какой смысл правила обобщения (GEN) в исчислении предикатов?

[creative]

Книга Колмогоров А.Н. Драгалин А.Г. Введение в математическую логику 1982.

Глава 3, § 1, пункт 1:

Цитата:

, $\begin{tabular}{ c c c } & A & \\ & \overline{ \therefore \forall x A } & \\ \end{tabular}$
...
... Второе правило называется правилом обобщения.
...
Правило обобщения также сохраняет истинность формул, но в некотором более слабом смысле - при интерпретации всеобщности: если $\theta$ - оценка для $\forall x A$ и для всякого объекта $a$ имеем $M \models {A_\underline{a}}^x \theta$, то $M \models (\forall x A)\theta$.

Глава 3, § 1, пункт 2:

Цитата:

Верхние формулы дерева формул, не имеющие вида аксиом исчисления предикатов, называются гипотезами, или открытыми посылками, дерева формул.
...
Деревом вывода, или просто выводом, в исчислении предикатов называется дерево формул, удовлетворяющее некоторому дополнительному структурному требованию. А именно если формула $\forall x A$ получена в выводе из формулы $A$ по правилу обобщения, то переменная $x$ не входит свободно в гипотезы, расположенные выше рассматриваемого вхождения формулы $\forall x A$.

Смысл правила обращения я понимаю примерно так:

Xaositect в сообщении #448962 писал(а):

Правило обобщение соответсвует такому довольно распространенному обороту: "Пусть $x$ - некоторая штука. Тогда <доказательство> получаем $A(x)$. Т.к. $x$ было выбрано произвольно, то для любой штуки $x$ верно $A(x)$"

Но все равно не понимаю почему, если нижняя формула $\forall x A$ была правильно получена по правилу обобщения из $A$, то ни одна гипотеза (в ветке, где нижняя формула $\forall x A$) не может содержать свободно $x$. Я так понимаю, что если верхние формулы (в ветке, где нижняя формула $\forall x A$) не гипотезы, а аксиомы исчисления предикатов, то они могут содержать свободно $x$, потому что аксиомы исчисления предикатов есть тавтологии, а потому верны при любых значениях свободных переменных.

Вопрос:

Разве гипотезы дерева вывода не рассматриваются как формулы истинные при всех значениях свободных переменных? Если не рассматриваются, то как именно их понимать (а именно как понимать их свободные переменные)?

Эти вопрос возникли из-за непонимания ограничения на правило обобщения описанное выше.

[Xaositect]

Это все нужно для того, чтобы выполнялась теорема о дедукции. Так, чтобы доказать $A(x)\to B(x)$, нужно предположить, что $A(x)$ выполняется для некоторого неопределенного, но конкретного(по которому нельзя обобщать) $x$, и вывести из него $B(x)$ не для любого, а для того же $x$. Поскольку обобщать здесь по этому $x$ нельзя, гипотеза $\forall x A(x)$ имеет другой смысл.

Здесь терминология и обозначения в разных книгах может отличаться. Часто используется значок $\vdash_{X}$ для вывода, в котором не используется обобщение по переменным из $X$. В этом случае мы явно говорим, что в $X$ у нас какие-то конкретные объекты, а остальные переменные --- произвольные.

[creative]

Xaositect

Большое спасибо!

Понятно, но буду переваривать, чтобы уложилось прочнее.