Доброго дня, господа!
Разбираюсь с основой теории доказательств, читаю 6-ю главу Ершова-Палютина.
В определении генценовского исчисления
![$\text{G}$ $\text{G}$](https://dxdy-01.korotkov.co.uk/f/0/c/3/0c3f5fb42a80665e361994f11104d7dd82.png)
требуется, чтобы ни одна переменная не входила в секвенцию одновременно свободно и связанно (несмешанные переменные). Это «невинное» требование заставляет быть очень аккуратным при различных перекройках деревьев доказательств.
В Предложении 2 параграфа 32 утверждается, что секвенция, доказуемая в
![$\text{ИП}$ $\text{ИП}$](https://dxdy-03.korotkov.co.uk/f/e/c/e/ecea8942abae11b9740bc2e1620e2cd782.png)
, также доказуема и в
![$\text{G}$ $\text{G}$](https://dxdy-01.korotkov.co.uk/f/0/c/3/0c3f5fb42a80665e361994f11104d7dd82.png)
. Доказывается эта штука индукцией по дереву доказательства в
![$\text{ИП}$ $\text{ИП}$](https://dxdy-03.korotkov.co.uk/f/e/c/e/ecea8942abae11b9740bc2e1620e2cd782.png)
. При этом вопрос несмешанности переменных обходится стороной. Но ведь в
![$\text{ИП}$ $\text{ИП}$](https://dxdy-03.korotkov.co.uk/f/e/c/e/ecea8942abae11b9740bc2e1620e2cd782.png)
переменные могут смешиваться! Более того, в
![$\text{ИП}$ $\text{ИП}$](https://dxdy-03.korotkov.co.uk/f/e/c/e/ecea8942abae11b9740bc2e1620e2cd782.png)
так часто и бывает:
![$P(x)\vdash_{\text{ИП}}\exists x P(x)$ $P(x)\vdash_{\text{ИП}}\exists x P(x)$](https://dxdy-02.korotkov.co.uk/f/9/e/6/9e69acd3e8f24dfee7010a4cf8becc9982.png)
.
Как закрыть этот пробел? Сам не придумал — перекройка деревьев доказательств в
![$\text{ИП}$ $\text{ИП}$](https://dxdy-03.korotkov.co.uk/f/e/c/e/ecea8942abae11b9740bc2e1620e2cd782.png)
штука неподъемная. Единственный путь, что пришел в голову — снять в
![$\text{G}$ $\text{G}$](https://dxdy-01.korotkov.co.uk/f/0/c/3/0c3f5fb42a80665e361994f11104d7dd82.png)
требование о несмешиваемости переменных и во всех правилах вывода разрешить переименование связанных переменных (замену формул на конгруэнтные им). Но это что-то уж слишком, и не уверен, что при таком переопределении
![$\text{G}$ $\text{G}$](https://dxdy-01.korotkov.co.uk/f/0/c/3/0c3f5fb42a80665e361994f11104d7dd82.png)
все остальное изложение Ершова-Палютина не пострадает. Буду рад любым комментариям!