Пробел в доказательстве у Ершова-Палютина?

[lofar]

Доброго дня, господа!

Разбираюсь с основой теории доказательств, читаю 6-ю главу Ершова-Палютина.
В определении генценовского исчисления $\text{G}$ требуется, чтобы ни одна переменная не входила в секвенцию одновременно свободно и связанно (несмешанные переменные). Это «невинное» требование заставляет быть очень аккуратным при различных перекройках деревьев доказательств.

В Предложении 2 параграфа 32 утверждается, что секвенция, доказуемая в $\text{ИП}$, также доказуема и в $\text{G}$. Доказывается эта штука индукцией по дереву доказательства в $\text{ИП}$. При этом вопрос несмешанности переменных обходится стороной. Но ведь в $\text{ИП}$ переменные могут смешиваться! Более того, в $\text{ИП}$ так часто и бывает: $P(x)\vdash_{\text{ИП}}\exists x P(x)$.

Как закрыть этот пробел? Сам не придумал — перекройка деревьев доказательств в $\text{ИП}$ штука неподъемная. Единственный путь, что пришел в голову — снять в $\text{G}$ требование о несмешиваемости переменных и во всех правилах вывода разрешить переименование связанных переменных (замену формул на конгруэнтные им). Но это что-то уж слишком, и не уверен, что при таком переопределении $\text{G}$ все остальное изложение Ершова-Палютина не пострадает. Буду рад любым комментариям!

[3D Homer]

В книге Ершов Ю.Л., Палютин Е.А. Математическая логика. М.: Физматлит, 2011 нет параграфа 32, но есть предложение 6.3.4, которое действительно утверждает, что если секвенция $С$ исчисления $G$ доказуема в \text{ИП}^\Sigma$, то она доказуема и в исчислении $G$. Но в начале § 6.3 говорится: "В этом параграфе докажем, что секвенция исчисления \text{ИП}^\Sigma$, которая является и секвенцией исчисления $G$ (т.е. не содержит знаков импликации $\to$ и равенства $\approx$ и удовлетворяет условию несмешанности переменных), доказуема в \text{ИП}^\Sigma$ тогда и только тогда, когда она доказуема в $G$". С доказательством я, правда, незнаком.

[pupugai]

Я не знаком с книгой Ершова-Палютина, но вообще связанные переменные можно переименовывать, не меняя значения выражения. $P(x)\vdash\exists x P(x)$ и $P(x)\vdash\exists y P(y)$ - это просто одно и то же. Можно считать, что когда вы видите $P(x)\vdash\exists x P(x)$, связанная переменная $x$ и свободная переменная $x$ это разные переменные, просто имеют одинаковые названия.