Выводимость в исчислении предикатов

[SomePupil]

Игошин В. - Математическая логика и теория алгоритмов, 2008 (стр. 225)
Учебник указан выше. Вот так автор вводит понятие выводимости в формализованном исчислении предикатов первого порядка (правила вывода стандартные):

Цитата:

Формула $G$ называется выводимой из гипотез $F_1, \ldots, F_m$ с фиксированными вхождениями (в гипотезы) свободных переменных, если существует такая конечная последовательность формул $B_1, B_2,\;\;\ldots,\;\;B_k,\;\; \ldots,\;\;B_s \equiv G,$ каждая формула которой является либо аксиомой, либо гипотезой, либо получена из предыдущих формул последовательности по одному из правил вывода. При этом, если $B_k$ есть первая гипотеза, встречающаяся в выводе, то дальше в этом выводе не могут быть использованы $\forall$- и $\exists$-правила вывода по любой переменной $x,$ которая входит свободно хотя бы в одну из гипотез.

Означает ли это, что после $k$-ой формулы используется только modus ponens?
Если это так, то это очень странно. Потому что убирать кванторы в выводах только лишь для того, чтобы фиксировать свободу переменных $-$ в высшей степени искусственная вещь, имхо.

[SomePupil]

P. S. Здравствуйте.

[arseniiv]

SomePupil в сообщении #1301581 писал(а):

Означает ли это, что после $k$-ой формулы используется только modus ponens?

Ну почему, есть же переменные кроме $x$.

Вообще дело в том, что необходимо или накладывать такое ограничение на выводы, или ослаблять теорему о дедукции. Здесь, видимо, решили пожертвовать первым.

-- Ср апр 04, 2018 18:06:07 --

А что, неужели там нет какой-то мотивации? (Или, может, она будет около теоремы о дедукции, а не здесь?)

[SomePupil]

arseniiv в сообщении #1301603 писал(а):

А что, неужели там нет какой-то мотивации?

По идее, должна быть. Поищу завтра утром. Тут уже десять часов вечера)