О лемме из книги Раутенберга(мат. логика)

[Tcirkubakin]

Возникли сложности при понимании леммы второго параграфа 3 главы книги Раутенберга (стоит ли здесь впредь выкладывать проблемные доказательства целиком, или лучше ссылаться на книгу в онлайн-варианте, указывая страницу?).

Lemma 2.1 (on constant elimination). Suppose $X\vdash _{\mathcal{L}_{c}}\alpha$. Then
$X\frac{z}{c}\vdash _{\mathcal{L}}\alpha\frac{z}{c}$ for almost all variables $z$.

Proof by rule induction in $\vdash _{\mathcal{L}_{c}}$. If $\alpha\in X$ then $\alpha \frac{z}{c} \in X \frac{z}{c}$ is clear; if $\alpha$ is
of the form $t=t$, so too is $\alpha \frac{z}{c}$. Thus, $X\frac{z}{c} \vdash _{\mathcal{L}} \alpha\frac{z}{c}$ a in either case, even for
all $z$. Only the induction steps on $\left( \forall 1 \right)$, $\left( \forall 2 \right)$, and $\left( = \right)$ are not immediately
apparent. We restrict ourselves to $\left( \forall 1 \right)$, because the induction steps for
$\left( \forall 2 \right)$ and $\left( = \right)$ proceed analogously. Let $\alpha , \frac{t}{x}$ be collision-free, $X \vdash _{\mathcal{L}_{c}} \forall x \alpha$,
and assume that $X\frac{z}{c} \vdash _{\mathcal{L}} \left( \forall x \alpha \right)\frac{z}{c}$ for almost all $z$. In addition, we may
suppose that $z\notin \text{var} \left\{ \forall x a, t \right\}$ for almost all $z$. A separate induction on $\alpha$
readily confirms $\alpha \frac{t}{x} \frac{z}{c} = \alpha '\frac{t'}{x}$ with $\alpha'\colon \!= \alpha\frac{z}{c}$ and $t'\colon \!= t\frac{z}{c}$. Clearly $\alpha',\frac{t'}{x}$
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'$.
Rule $\left( \forall 1 \right)$ then clearly yields $X\frac{z}{c} \vdash _{\mathcal{L}} \alpha'\frac{t}{x}=\alpha\frac{t}{x}\frac{z}{c}$, and this holds still for
almost all $z$ which completes the proof of the induction step on $\left( \forall 1 \right)$.
(Здесь $\mathcal{L}_{c}$ - язык, дополненный константой, а $\left( \forall 1 \right)$ обозначает правило вывода: $(\forall 1) \frac{X \vdash \forall x \alpha}{X \vdash \alpha \frac{t}{x}}\left(\alpha, \frac{t}{x} \quad\right. \text { collision-free) }$
Формула $\varphi$ и замена $\frac{t}{x}$ являются "свободными от коллизий(столкновений) "(как правильно перевести collision-free?),если для всех переменных y, отличных от x, и таких, что $y\in \text{var}t$ выполняется условие: $y\notin \text{bnd}\varphi$(var -множество переменных, bnd- множество связанных переменных)).
Здесь утверждается, что $\alpha',\frac{t'}{x}$ будут также свободны от коллизий. Возник вопрос: т.к. $z\notin \text{var} \left\{ \forall x a, t \right\}$, то переменная $z$ не входит в $\alpha$ и всё должно выполняться. Однако,можно взять формулу $\alpha$ с избыточным квантором $\forall z$ и получается следующее:
$\alpha = \forall z \beta$ для некоторой формулы $\beta$. Тогда $\alpha'=\left( \forall z \beta \right)\frac{z}{c}$, и при наличии в формуле $\beta$ константы $c$ формула $\alpha'=\left( \forall z \beta \right)\frac{z}{c}$ уже будет содержать в себе связанную переменную z, и $\alpha',\frac{t'}{x}$ в общем случае уже не будет свободной от коллизий, достаточно, чтобы в терме $t$ содержалась константа $c$, и , следовательно, $t'=t\frac{z}{c}$ будет содержать переменную $z$, встречающуюся в связанном виде в формуле $\alpha'=\left( \forall z \beta \right)\frac{z}{c}$.
Может быть, моя ошибка заключается в том, что если $z\notin \text{var} \left\{ \forall x a, t \right\}$, то также не допускается добавление даже избыточного квантора с сопутствующей переменной, т.е переменная $z$ уже содержится в кванторе,или $\forall z$ не содержит переменных, и я ошибаюсь в другом месте?

[Tcirkubakin]

Tcirkubakin в сообщении #1584312 писал(а):

Rule $\left( \forall 1 \right)$ 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}$

[mihaild]

Не очень понятно, в чем проблема. Ну да, некоторые $z$ входят в $\alpha$. Но нам сначала приносят $\alpha$, а потом мы должны выбрать $z$.
Добавление даже фиктивного квантора меняет формулу, и соответственно для новой формулы нужно проводить рассуждение отдельно.

[Tcirkubakin]

Имел ввиду, что для формулы $\alpha$ есть ограничение, вытекающее из $z\notin \text{var} \left\{ \forall x \alpha, t \right\}$(в первом сообщении в $z\notin \text{var} \left\{ \forall x a, t \right\}$ допустил ещё одну опечатку: вместо "альфы" написал $a$), что переменная $z$ не может входить в $\alpha$. Т.е. из этих условий, как я понимаю, следует, что $\alpha$ может быть любой формулой без переменных z.

mihaild в сообщении #1584763 писал(а):

Но нам сначала приносят $\alpha$, а потом мы должны выбрать $z$.

Разве не может среди "принесённых" формул быть $\alpha$ вида $\alpha = \forall z \beta$, не содержащая переменных $z$?
Запрещают ли нам это сделать условия теоремы? И если нет, то будут ли в этом случае $\alpha',\frac{t'}{x}$ свободны от "коллизий"(если да, то каким образом)?

[mihaild]

Я всё еще не понимаю, что Вас смущает.
Нам дали формулу $\alpha$. Выберем какую-нибудь переменную (и обозначим её как $\textbf{z}$ - давайте считать переменные в формулах написанными обычным шрифтом, а обозначения переменных в наших рассуждениях жирным), не входящую в $\alpha$ (в частности, $\alpha$ не имеет вид $\forall \textbf{z} \beta$). Далее проводим рассуждения.
Буква $\textbf{z}$ в доказательстве - это не переменная нашего языка, это обозначение какой-то переменной языка.

Tcirkubakin в сообщении #1584767 писал(а):

Разве не может среди "принесённых" формул быть $\alpha$ вида $\alpha = \forall z \beta$, не содержащая переменных $z$?

Формула $\forall z \beta$ содержит $z$. В этом случае в рассуждении выше надо брать например $\textbf{z} = p$, или какую-нибудь еще подходящую переменную, а не $\textbf{z} = z$.

[Tcirkubakin]

mihaild в сообщении #1584770 писал(а):

Формула $\forall z \beta$ содержит $z$.

Т.е причина(или нет?) кроется в моём неправильном понимании формулы $z\notin \text{var} \left\{ \forall x a, t \right\}$, которая на самом деле означает, что любое нахождение $z$(просто в виде символа) в формуле $\forall x \alpha$, в частности в $\alpha$, недопустимо. Если это так, то надо "прошерстить" учебник, на всякий случай.

[mihaild]

Да, посмотрите определение $\text{var}$. Я сходу не нашел, но наверняка там берется не только верхний квантор.

[Tcirkubakin]

Да, так и есть. Определение "var" для любой строки дано на 56 странице (https://archive.org/details/a-concise-i ... 6/mode/2up). Вернусь к этой лемме. Правильно ли я провёл индукцию для $\left( \forall 2 \right)$ и $\left( = \right)$?(эти шаги нужно выполнить самостоятельно). ($\left( \forall 2 \right)\ \frac{X\vdash \alpha\frac{y}{x}}{X\vdash \forall x \alpha} \left( y \notin \text{free} X\, \cup \, \text{var}\alpha \right)$ , $\left( = \right)\ \frac{X\vdash s=t,\alpha\frac{s}{x}}{X\vdash \alpha\frac{t}{x}} \left( \alpha \ \text{prime} \right)$)
$\left( \forall 2 \right)$:
Пусть $\left( y \notin \text{free} X\, \cup \, \text{var}\alpha \right)$, $X\vdash_{\mathcal{L}_{c}} \alpha\frac{y}{x}$, и предположим, что $X\frac{z}{c}\vdash_{\mathcal{L}} \left( \alpha\frac{y}{x} \right)\frac{z}{c}$. Отдельной индукцией по $\alpha$ можно показать, что $\alpha\frac{y}{x}\frac{z}{c}=\alpha\frac{z}{c}\frac{y}{x}$. Положим $\alpha'=\alpha\frac{z}{c}$. Тогда $X\frac{z}{c}\vdash_{\mathcal{L}} \alpha\frac{y}{x}\frac{z}{c}=\alpha\frac{z}{c}\frac{y}{x}$ можно записать, как $X\frac{z}{c}\vdash_{\mathcal{L}}\alpha'\frac{y}{x}$. Очевидно, что $\left( y \notin \text{free} X\frac{z}{c}\, \cup \, \text{var}\alpha' \right)$(по условию $y \notin \text{free} X$, следовательно $y$ не появится в $X$ (а тем более в его множестве свободных переменных) при замене $\frac z c$; по условию $y \notin\, \text{var}\alpha $, следовательно $y$ не появится в $\alpha$ и при замене $\frac z c$). Учитывая это, получаем: $\frac{X\frac{z}{c}\vdash_{\mathcal{L}}\alpha'\frac{y}{x}}{X\frac{z}{c}\vdash_{\mathcal{L}} \forall x\alpha'=\forall x\left( \alpha\frac{z}{c} \right)=\left( \forall x\alpha \right)\frac{z}{c}}$, или $\frac{X\frac{z}{c}\vdash_{\mathcal{L}}\alpha\frac{y}{x}\frac{z}{c}}{X\frac{z}{c}\vdash_{\mathcal{L}}\left( \forall x\alpha \right)\frac{z}{c}}$, т.е. индукция для $\left( \forall 2 \right)$ завершена.

$\left( = \right)$:
Пусть $\left( \alpha\ \text{prime} \right)$, $X\vdash_{\mathcal{L}_{c}} s=t,\alpha\frac{s}{x}$, и предположим, что $X\frac{z}{c}\vdash_{\mathcal{L}} \left( s=t \right)\frac{z}{c},\left( \alpha\frac{s}{x} \right)\frac{z}{c}$, после преобразования получаем $X\frac{z}{c}\vdash_{\mathcal{L}} s\frac{z}{c}=t\frac{z}{c},\alpha\frac{s}{x}\frac{z}{c}$. Пусть $s'=s\frac{z}{c}$, и $t'=t\frac{z}{c}$, тогда получаем $X\frac{z}{c}\vdash_{\mathcal{L}} s'=t',\alpha\frac{s}{x}\frac{z}{c}$. Отдельной индукцией по $\alpha$ можно показать, что $\alpha\frac{s}{x}\frac{z}{c}=\alpha'\frac{s'}{x}$, где $\alpha'=\alpha\frac{z}{c}$. Учитывая это, получим : $X\frac{z}{c}\vdash_{\mathcal{L}} s'=t',\alpha'\frac{s'}{x}$. Легко доказывается, что если $\alpha\in \text{prime}$, то $\alpha'\in \text{prime}$(простая формула имеет вид $s=t$, или $r\vec{t}$, где $s,t,\vec{t}$-термы, а $r$ - отношение, или предикат, очевидно, что при замене формулы и в первом, и во втором случае сохранят свой вид). Следовательно, к формуле$X\frac{z}{c}\vdash_{\mathcal{L}} s'=t',\alpha'\frac{s'}{x}$ можно применить $\left( = \right)$: $\frac{X\frac{z}{c}\vdash_{\mathcal{L}} s'=t',\alpha'\frac{s'}{x}}{X\frac{z}{c}\vdash_{\mathcal{L}}\alpha'\frac{t'}{x}}$. После обратного преобразования получаем: $\frac{X\frac{z}{c}\vdash_{\mathcal{L}} \left( s=t \right)\frac{z}{c},\left( \alpha\frac{s}{x} \right)\frac{z}{c}}{X\frac{z}{c}\vdash_{\mathcal{L}}\left( \alpha\frac{t}{x} \right)\frac{z}{c}}$, т.е шаг индукции для $\left( = \right)$ завершён(здесь мы воспользовались $\left( \alpha\frac{t}{x} \right)\frac{z}{c}=\alpha'\frac{t'}{x}, \alpha'=\alpha\frac{z}{c}$, доказывается аналогично $\alpha\frac{s}{x}\frac{z}{c}=\alpha'\frac{s'}{x}$).
Выше неявно воспользовался тем что при замене множество формул $X$ ($X \frac{z}{c}$)остаётся множеством формул (это также необходимо для использования формул $\left( \forall 2 \right)$ и $\left( = \right)$).
P.S. Стоит ли переписывать док-ва из учебника или, по возможности, можно ссылаться на онлайн вариант из archive.org?

[mihaild]

Всё хорошо, только нужно сказать, что $y \neq z$.

Tcirkubakin в сообщении #1584941 писал(а):

P.S. Стоит ли переписывать док-ва из учебника или, по возможности, можно ссылаться на онлайн вариант из archive.org?

Это в "Работу форума". ИМХО довольно логично, потому что получаются большие блоки текста, которые в получающемся в форумном движке виде читаются хуже, чем в книге.