Возникли сложности при понимании леммы второго параграфа 3 главы книги Раутенберга (стоит ли здесь впредь выкладывать проблемные доказательства целиком, или лучше ссылаться на книгу в онлайн-варианте, указывая страницу?).
Lemma 2.1 (on constant elimination). Suppose
![$X\vdash _{\mathcal{L}_{c}}\alpha$ $X\vdash _{\mathcal{L}_{c}}\alpha$](https://dxdy-02.korotkov.co.uk/f/d/5/1/d51991763f0552d24baacd1e2a307aaa82.png)
. Then
![$X\frac{z}{c}\vdash _{\mathcal{L}}\alpha\frac{z}{c}$ $X\frac{z}{c}\vdash _{\mathcal{L}}\alpha\frac{z}{c}$](https://dxdy-04.korotkov.co.uk/f/3/5/f/35ffa13212efad32914308ca194d39e282.png)
for almost all variables
![$z$ $z$](https://dxdy-04.korotkov.co.uk/f/f/9/3/f93ce33e511096ed626b4719d50f17d282.png)
.
Proof by rule induction in
![$\vdash _{\mathcal{L}_{c}}$ $\vdash _{\mathcal{L}_{c}}$](https://dxdy-02.korotkov.co.uk/f/d/c/2/dc215571fde4f1b3036b991399101b5f82.png)
. If
![$\alpha\in X$ $\alpha\in X$](https://dxdy-02.korotkov.co.uk/f/d/b/f/dbf9c1524180f153ef5c165074552c4e82.png)
then
![$\alpha \frac{z}{c} \in X \frac{z}{c}$ $\alpha \frac{z}{c} \in X \frac{z}{c}$](https://dxdy-02.korotkov.co.uk/f/1/3/7/1377169dba40c79f27cc34e27c6c49dd82.png)
is clear; if
![$\alpha$ $\alpha$](https://dxdy-01.korotkov.co.uk/f/c/7/4/c745b9b57c145ec5577b82542b2df54682.png)
is
of the form
![$t=t$ $t=t$](https://dxdy-02.korotkov.co.uk/f/5/7/2/572f16623268bd1cc3634677955a5eec82.png)
, so too is
![$\alpha \frac{z}{c}$ $\alpha \frac{z}{c}$](https://dxdy-03.korotkov.co.uk/f/a/0/a/a0aa3f964437cb47d7ecfe531b719e6b82.png)
. Thus,
![$X\frac{z}{c} \vdash _{\mathcal{L}} \alpha\frac{z}{c}$ $X\frac{z}{c} \vdash _{\mathcal{L}} \alpha\frac{z}{c}$](https://dxdy-01.korotkov.co.uk/f/4/d/e/4de415adc8b57836a43b5aa0000077e782.png)
a in either case, even for
all
![$z$ $z$](https://dxdy-04.korotkov.co.uk/f/f/9/3/f93ce33e511096ed626b4719d50f17d282.png)
. Only the induction steps on
![$\left( \forall 1 \right)$ $\left( \forall 1 \right)$](https://dxdy-04.korotkov.co.uk/f/b/3/1/b317a23885ee4014efdce2b39096346582.png)
,
![$\left( \forall 2 \right)$ $\left( \forall 2 \right)$](https://dxdy-03.korotkov.co.uk/f/6/4/c/64ce57cbc598e9cc5f5890d19c672e3582.png)
, and
![$\left( = \right)$ $\left( = \right)$](https://dxdy-01.korotkov.co.uk/f/4/5/2/4526642ec5a562a927f027273328c22c82.png)
are not immediately
apparent. We restrict ourselves to
![$\left( \forall 1 \right)$ $\left( \forall 1 \right)$](https://dxdy-04.korotkov.co.uk/f/b/3/1/b317a23885ee4014efdce2b39096346582.png)
, because the induction steps for
![$\left( \forall 2 \right)$ $\left( \forall 2 \right)$](https://dxdy-03.korotkov.co.uk/f/6/4/c/64ce57cbc598e9cc5f5890d19c672e3582.png)
and
![$\left( = \right)$ $\left( = \right)$](https://dxdy-01.korotkov.co.uk/f/4/5/2/4526642ec5a562a927f027273328c22c82.png)
proceed analogously. Let
![$\alpha , \frac{t}{x}$ $\alpha , \frac{t}{x}$](https://dxdy-04.korotkov.co.uk/f/3/1/e/31e5512102c8d79368d5c5c76152134082.png)
be collision-free,
![$X \vdash _{\mathcal{L}_{c}} \forall x \alpha$ $X \vdash _{\mathcal{L}_{c}} \forall x \alpha$](https://dxdy-04.korotkov.co.uk/f/f/6/d/f6d70eb8697c9782f2e7bb5e416bb2dd82.png)
,
and assume that
![$X\frac{z}{c} \vdash _{\mathcal{L}} \left( \forall x \alpha \right)\frac{z}{c}$ $X\frac{z}{c} \vdash _{\mathcal{L}} \left( \forall x \alpha \right)\frac{z}{c}$](https://dxdy-03.korotkov.co.uk/f/2/2/5/2256efeefaaea18bd87596af67d431cc82.png)
for almost all
![$z$ $z$](https://dxdy-04.korotkov.co.uk/f/f/9/3/f93ce33e511096ed626b4719d50f17d282.png)
. In addition, we may
suppose that
![$z\notin \text{var} \left\{ \forall x a, t \right\}$ $z\notin \text{var} \left\{ \forall x a, t \right\}$](https://dxdy-04.korotkov.co.uk/f/7/f/6/7f6359f8b6289029d93db3fa023db25382.png)
for almost all
![$z$ $z$](https://dxdy-04.korotkov.co.uk/f/f/9/3/f93ce33e511096ed626b4719d50f17d282.png)
. A separate induction on
![$\alpha$ $\alpha$](https://dxdy-01.korotkov.co.uk/f/c/7/4/c745b9b57c145ec5577b82542b2df54682.png)
readily confirms
![$\alpha \frac{t}{x} \frac{z}{c} = \alpha '\frac{t'}{x}$ $\alpha \frac{t}{x} \frac{z}{c} = \alpha '\frac{t'}{x}$](https://dxdy-02.korotkov.co.uk/f/5/f/d/5fd2c94fcee5629457510d2c34dc112382.png)
with
![$\alpha'\colon \!= \alpha\frac{z}{c}$ $\alpha'\colon \!= \alpha\frac{z}{c}$](https://dxdy-03.korotkov.co.uk/f/6/9/4/694e1ffaff65465dbd81336c8f95363082.png)
and
![$t'\colon \!= t\frac{z}{c}$ $t'\colon \!= t\frac{z}{c}$](https://dxdy-01.korotkov.co.uk/f/4/c/9/4c9300ac2bdc0ff17a1eedbc9948bf7182.png)
. Clearly
![$\alpha',\frac{t'}{x}$ $\alpha',\frac{t'}{x}$](https://dxdy-01.korotkov.co.uk/f/4/9/d/49d81cd025f3a105438256c96d508d5682.png)
are collision-free as well. By our assumption,
![$X\frac{z}{c} \vdash _{\mathcal{L}} \left( \forall x \alpha \right)\frac{z}{c}=\forall x\alpha'$ $X\frac{z}{c} \vdash _{\mathcal{L}} \left( \forall x \alpha \right)\frac{z}{c}=\forall x\alpha'$](https://dxdy-01.korotkov.co.uk/f/0/a/0/0a057f15eaa06c344083406d89b1a0d182.png)
.
Rule
![$\left( \forall 1 \right)$ $\left( \forall 1 \right)$](https://dxdy-04.korotkov.co.uk/f/b/3/1/b317a23885ee4014efdce2b39096346582.png)
then clearly yields
![$X\frac{z}{c} \vdash _{\mathcal{L}} \alpha'\frac{t}{x}=\alpha\frac{t}{x}\frac{z}{c}$ $X\frac{z}{c} \vdash _{\mathcal{L}} \alpha'\frac{t}{x}=\alpha\frac{t}{x}\frac{z}{c}$](https://dxdy-03.korotkov.co.uk/f/e/3/e/e3e803ddd1d801b3718f4a7b489d552982.png)
, and this holds still for
almost all
![$z$ $z$](https://dxdy-04.korotkov.co.uk/f/f/9/3/f93ce33e511096ed626b4719d50f17d282.png)
which completes the proof of the induction step on
![$\left( \forall 1 \right)$ $\left( \forall 1 \right)$](https://dxdy-04.korotkov.co.uk/f/b/3/1/b317a23885ee4014efdce2b39096346582.png)
.
(Здесь
![$\mathcal{L}_{c}$ $\mathcal{L}_{c}$](https://dxdy-01.korotkov.co.uk/f/c/d/9/cd9d77838acc35b3e9324b8ac9ea9cbc82.png)
- язык, дополненный константой, а
![$\left( \forall 1 \right)$ $\left( \forall 1 \right)$](https://dxdy-04.korotkov.co.uk/f/b/3/1/b317a23885ee4014efdce2b39096346582.png)
обозначает правило вывода:
![$(\forall 1) \frac{X \vdash \forall x \alpha}{X \vdash \alpha \frac{t}{x}}\left(\alpha, \frac{t}{x} \quad\right. \text { collision-free) }$ $(\forall 1) \frac{X \vdash \forall x \alpha}{X \vdash \alpha \frac{t}{x}}\left(\alpha, \frac{t}{x} \quad\right. \text { collision-free) }$](https://dxdy-02.korotkov.co.uk/f/1/3/8/13854ad0668869b0ea9ca05cfdc73fde82.png)
Формула
![$\varphi$ $\varphi$](https://dxdy-01.korotkov.co.uk/f/4/1/7/417a5301693b60807fa658e5ef9f953582.png)
и замена
![$\frac{t}{x}$ $\frac{t}{x}$](https://dxdy-03.korotkov.co.uk/f/2/8/7/287ab611d0672431046072cf2fb5dfc082.png)
являются "свободными от коллизий(столкновений) "(как правильно перевести collision-free?),если для всех переменных y, отличных от x, и таких, что
![$y\in \text{var}t$ $y\in \text{var}t$](https://dxdy-02.korotkov.co.uk/f/1/b/0/1b06164c19387403848f9271eaf49e5b82.png)
выполняется условие:
![$y\notin \text{bnd}\varphi$ $y\notin \text{bnd}\varphi$](https://dxdy-01.korotkov.co.uk/f/8/c/1/8c18a9b9be21b82fed39665a4305e31782.png)
(var -множество переменных, bnd- множество связанных переменных)).
Здесь утверждается, что
![$\alpha',\frac{t'}{x}$ $\alpha',\frac{t'}{x}$](https://dxdy-01.korotkov.co.uk/f/4/9/d/49d81cd025f3a105438256c96d508d5682.png)
будут также свободны от коллизий. Возник вопрос: т.к.
![$z\notin \text{var} \left\{ \forall x a, t \right\}$ $z\notin \text{var} \left\{ \forall x a, t \right\}$](https://dxdy-04.korotkov.co.uk/f/7/f/6/7f6359f8b6289029d93db3fa023db25382.png)
, то переменная
![$z$ $z$](https://dxdy-04.korotkov.co.uk/f/f/9/3/f93ce33e511096ed626b4719d50f17d282.png)
не входит в
![$\alpha$ $\alpha$](https://dxdy-01.korotkov.co.uk/f/c/7/4/c745b9b57c145ec5577b82542b2df54682.png)
и всё должно выполняться. Однако,можно взять формулу
![$\alpha$ $\alpha$](https://dxdy-01.korotkov.co.uk/f/c/7/4/c745b9b57c145ec5577b82542b2df54682.png)
с избыточным квантором
![$\forall z$ $\forall z$](https://dxdy-04.korotkov.co.uk/f/f/4/e/f4e472a64089b209511dea101028f45782.png)
и получается следующее:
![$\alpha = \forall z \beta$ $\alpha = \forall z \beta$](https://dxdy-04.korotkov.co.uk/f/3/7/1/3719719395908948dcaa848961e7cba882.png)
для некоторой формулы
![$\beta$ $\beta$](https://dxdy-01.korotkov.co.uk/f/8/2/1/8217ed3c32a785f0b5aad4055f432ad882.png)
. Тогда
![$\alpha'=\left( \forall z \beta \right)\frac{z}{c}$ $\alpha'=\left( \forall z \beta \right)\frac{z}{c}$](https://dxdy-02.korotkov.co.uk/f/9/b/9/9b9c3ab5b064611a55a407fd4bc52b2582.png)
, и при наличии в формуле
![$\beta$ $\beta$](https://dxdy-01.korotkov.co.uk/f/8/2/1/8217ed3c32a785f0b5aad4055f432ad882.png)
константы
![$c$ $c$](https://dxdy-04.korotkov.co.uk/f/3/e/1/3e18a4a28fdee1744e5e3f79d13b9ff682.png)
формула
![$\alpha'=\left( \forall z \beta \right)\frac{z}{c}$ $\alpha'=\left( \forall z \beta \right)\frac{z}{c}$](https://dxdy-02.korotkov.co.uk/f/9/b/9/9b9c3ab5b064611a55a407fd4bc52b2582.png)
уже будет содержать в себе связанную переменную z, и
![$\alpha',\frac{t'}{x}$ $\alpha',\frac{t'}{x}$](https://dxdy-01.korotkov.co.uk/f/4/9/d/49d81cd025f3a105438256c96d508d5682.png)
в общем случае уже не будет свободной от коллизий, достаточно, чтобы в терме
![$t$ $t$](https://dxdy-01.korotkov.co.uk/f/4/f/4/4f4f4e395762a3af4575de74c019ebb582.png)
содержалась константа
![$c$ $c$](https://dxdy-04.korotkov.co.uk/f/3/e/1/3e18a4a28fdee1744e5e3f79d13b9ff682.png)
, и , следовательно,
![$t'=t\frac{z}{c}$ $t'=t\frac{z}{c}$](https://dxdy-01.korotkov.co.uk/f/0/8/e/08e4a5a0c2248c1ff40a154ae103f3f082.png)
будет содержать переменную
![$z$ $z$](https://dxdy-04.korotkov.co.uk/f/f/9/3/f93ce33e511096ed626b4719d50f17d282.png)
, встречающуюся в связанном виде в формуле
![$\alpha'=\left( \forall z \beta \right)\frac{z}{c}$ $\alpha'=\left( \forall z \beta \right)\frac{z}{c}$](https://dxdy-02.korotkov.co.uk/f/9/b/9/9b9c3ab5b064611a55a407fd4bc52b2582.png)
.
Может быть, моя ошибка заключается в том, что если
![$z\notin \text{var} \left\{ \forall x a, t \right\}$ $z\notin \text{var} \left\{ \forall x a, t \right\}$](https://dxdy-04.korotkov.co.uk/f/7/f/6/7f6359f8b6289029d93db3fa023db25382.png)
, то также не допускается добавление даже избыточного квантора с сопутствующей переменной, т.е переменная
![$z$ $z$](https://dxdy-04.korotkov.co.uk/f/f/9/3/f93ce33e511096ed626b4719d50f17d282.png)
уже содержится в кванторе,или
![$\forall z$ $\forall z$](https://dxdy-04.korotkov.co.uk/f/f/4/e/f4e472a64089b209511dea101028f45782.png)
не содержит переменных, и я ошибаюсь в другом месте?