Определение выводимости

[lofar]

Добрый день!
В замечательной книжке Ершова-Палютина в параграфе 22 о гильбертовском исчесленни предикатов ($\mbox{ИП}^{\Sigma}_1$) дается определение вывода формулы $\Phi$ из множества формул $G$. (Все аксиомы и правила вывода переписывать не стану -- это классика.)

$\Phi$ выводится из $G$ (обозначается $G \rhd\Phi$) если существует последовательность формул $\Phi_0,...,\Phi_n$ такая, что для каждого $i$: или $\Phi_i$ -- аксиома $\mbox{ИП}^{\Sigma}_1$, или $\Phi_i\in G$, или $\Phi_i$ получается из некоторых $\Phi_j$, $j < i$ по правилам вывода. Кроме того требуется следующее:
(*) Если в выводе используется правило

$$ \frac{\Phi\to\Psi}{\Phi\to\forall x\Psi}, x\mbox{ не входит свободно в }\Phi $$

то $x$ не должно входить ни в одну из формул из $G$ свободно.

У меня вопрос как раз по этому дополнительному условию (*). Зачем оно нужно понятно: из доказуемости $x\approx y\to x\approx y$ не должна следовать доказуемость $x\approx y\to \forall x\:\: x\approx y$. С другой стороны, возникает интересный казус, который меня и заботит: как при таком определении доказать, что для любых множеств формул $G$ и $G'$, $G\subseteq G'$ и формулы $\Phi$ из $G\rhd\Phi$ следует $G'\rhd\Phi$.

[Профессор Снэйп]

Там в книжке неточность. $x$ не должна входить свободно не во все формулы из $G$, а лишь в те, которые участвуют в выводе.

-- Вс мар 13, 2011 13:11:17 --

И даже не так, ещё сложнее

[lofar]

Я тоже так подумал, это было бы естественно. А что там еще сложнее?

[dkflbvbhknb]

У меня тоже есть вопрос касающийся этой книжки, может быть он и Вас заинтересует. В параграфе 19 дается определение конгруэнтных формул. В книге Колмогорова-Драгалина в параграфе "Язык первого порядка. Формулы и термы" приводится индуктивное определение этого понятия. Как можно доказать эквивалентность этих определений?

[lofar]

Профессор Снэйп писал(а):

И даже не так, ещё сложнее

Да, действительно. Положим мы смягчили требование, и просим только, чтобы при использовании указанного правила вывода, $x$ не входил свободно в элементы $G$ задействованные в выводе. Все равно не понятно как тогда доказать, скажем, что из $G\rhd\Phi$ и $G\rhd\Psi$ следует $G\rhd\Phi\wedge\Psi$. Как быть? Рассматривать деревья вывода и требовать чтобы при применении пресловутого правила $x$ не входил свободно в элементы $G$, стоящие в ветке, выходящей из точки применения правила? Чувствую, что-то не так: Ершов и Палютин не могли проглядеть подобный нюанас!