2014 dxdy logo

Научный форум dxdy

Математика, Физика, Computer Science, Machine Learning, LaTeX, Механика и Техника, Химия,
Биология и Медицина, Экономика и Финансовая Математика, Гуманитарные науки


Правила форума


Посмотреть правила форума



Начать новую тему Ответить на тему
 
 О лемме из книги Раутенберга(мат. логика)
Сообщение04.03.2023, 20:58 


26/12/22
52
Возникли сложности при понимании леммы второго параграфа 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$ не содержит переменных, и я ошибаюсь в другом месте?

 Профиль  
                  
 
 Re: О лемме из книги Раутенберга(мат. логика)
Сообщение04.03.2023, 22:40 


26/12/22
52
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}$

 Профиль  
                  
 
 Re: О лемме из книги Раутенберга(мат. логика)
Сообщение07.03.2023, 21:19 
Заслуженный участник
Аватара пользователя


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

 Профиль  
                  
 
 Re: О лемме из книги Раутенберга(мат. логика)
Сообщение07.03.2023, 22:09 


26/12/22
52
Имел ввиду, что для формулы $\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}$ свободны от "коллизий"(если да, то каким образом)?

 Профиль  
                  
 
 Re: О лемме из книги Раутенберга(мат. логика)
Сообщение07.03.2023, 22:36 
Заслуженный участник
Аватара пользователя


16/07/14
8355
Цюрих
Я всё еще не понимаю, что Вас смущает.
Нам дали формулу $\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$.

 Профиль  
                  
 
 Re: О лемме из книги Раутенберга(мат. логика)
Сообщение08.03.2023, 01:00 


26/12/22
52
mihaild в сообщении #1584770 писал(а):
Формула $\forall z \beta$ содержит $z$.

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

 Профиль  
                  
 
 Re: О лемме из книги Раутенберга(мат. логика)
Сообщение08.03.2023, 01:29 
Заслуженный участник
Аватара пользователя


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

 Профиль  
                  
 
 Re: О лемме из книги Раутенберга(мат. логика)
Сообщение09.03.2023, 20:58 


26/12/22
52
Да, так и есть. Определение "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?

 Профиль  
                  
 
 Re: О лемме из книги Раутенберга(мат. логика)
Сообщение11.03.2023, 00:38 
Заслуженный участник
Аватара пользователя


16/07/14
8355
Цюрих
Всё хорошо, только нужно сказать, что $y \neq z$.
Tcirkubakin в сообщении #1584941 писал(а):
P.S. Стоит ли переписывать док-ва из учебника или, по возможности, можно ссылаться на онлайн вариант из archive.org?
Это в "Работу форума". ИМХО довольно логично, потому что получаются большие блоки текста, которые в получающемся в форумном движке виде читаются хуже, чем в книге.

 Профиль  
                  
Показать сообщения за:  Поле сортировки  
Начать новую тему Ответить на тему  [ Сообщений: 9 ] 

Модераторы: Модераторы Математики, Супермодераторы



Кто сейчас на конференции

Сейчас этот форум просматривают: нет зарегистрированных пользователей


Вы не можете начинать темы
Вы не можете отвечать на сообщения
Вы не можете редактировать свои сообщения
Вы не можете удалять свои сообщения
Вы не можете добавлять вложения

Найти:
Powered by phpBB © 2000, 2002, 2005, 2007 phpBB Group