Исчисление предикатов

[Paul Ivanov]

Опасаюсь, что мог где-то ошибиться.
Прошу подтвердить или опровергнуть следующее в рамках исчисления предикатов.
Не оставляет сомнения, что $A\supset B, B\supset C \vdash A\supset C$ верно также для исчисления предикатов, причём легко создать прямой вывод.
Далее по теореме дедукции для исчисления предикатов, так как все свободные переменные фиксированы для исходной формулы $B\supset C$ вследствие того, что в изначальном выводе не используются правила вывода из исчисления предикатов (а именно удаление общности и существования), выходит, что $A\supset B \vdash (B\supset C) \supset (A\supset C)$, и также верно, что $\vdash (A\supset B) \supset ((B\supset C) \supset (A\supset C))$, по той же причине только уже по отношению к последнему выводу. (В этих рассуждениях я руководствовался "Введением в метаматематику" Клини)
Я где-нибудь ошибся?

-- 20.07.2021, 15:25 --

И если это верное рассуждение, то подобным образом можно показать, что допустим $A(x) \sim B(x) \vdash (A(x)\supset C(x))\sim (B(x)\supset C(x))$. А в таком ключе непонятно, зачем в теореме о замене для исчисления предикатов $A\sim B \vdash^{x_1...x_n} C_A \sim C_B $ устанавливается ограничение на то, что все свободные переменные $x_1,x_2...,x_n$ в $A$ или $B$ должны быть завешены кванторами?

[kernel1983]

А что, для исчисления предикатов нужно отдельно доказывать? Разве исчисление высказываний не является частью исчисления предикатов? Можно, строя доказательство закона силлогизма, взять вместо переменных произвольные формулы исчисления предикатов.

[Paul Ivanov]

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

-- 20.07.2021, 16:30 --

Пардон, вопрос снят, это оказывается не ограничение, а описание тех переменных, что варьируются, хотя варьироваться обязаны не все.