Подстановки в выражения языка первого порядка

[creative]

Сначала привожу цитату из книги с моим вопросом, а ниже почти все необходимые определения из книги.

Есть вопрос по пункту 7 §2 главы 2 книги Колмогорова, Драгалина "Введение в математическую логику" (если понадобится, то её можно скачать вот тут):

Цитата:

7. Пусть $A$ - формула и $\theta$ - подстановка, необязательно допустимая для $A$. Как мы уже говорили, в этом случае $A \theta$, вообще говоря, непригодна с точки зрения предполагаемого смысла подстановки. Правильный способ действий в этой ситуации таков. Следует найти вариант $A'$, $A' \approx A$, такой, что $\theta$ допустима для $A'$, и рассмотреть формулу $A' \theta$. Мы назовем $A' \theta$ результатом правильной подстановки $\theta$ в $A$ и обозначим $A' \theta$ через $[A \theta]$.
Формула $[A \theta]$ определена неоднозначно, она зависит от выбора варианта $A'$. Однако если $A' \approx A' '$ и $\theta$ - подстановка, свободная для $A'$ и для $A''$, то $A' \theta \approx A'' \theta$. Таким образом, правильная подстановка определена однозначно с точностью до конгруэнтности.
То обстоятельство, что нужный вариант $A'$, для которого $\theta$ допустима, найдется, вытекает, например, из следующей леммы.
Будем говорить, что формула $A$ обладает свойством чистоты переменных, если, во-первых, все ее связанные переменные отличны от свободных и, во-вторых, любые два различные вхождения кванторных приставок связывают различные переменные.

Лемма (о чистоте переменных). Пусть $A$ - формула и $S$ - конечное множество переменных. Тогда может быть построена формула $B$ со свойством чистоты переменных такая, что $A \approx B$ и всякая связанная переменная $B$ отлична от переменных из множества $S$.

Вопрос: Зачем вообще вводить свойство чистоты переменных, если требуется только то, что бы для любого $x \in dom \theta \cap Fv(T)$ терм $\theta (x)$ не содержал свободных переменных, которые могли бы стать связанными попав в область действия одного из кванторов в выражении $T$, тем более что конечное множество $S$ тут играет роль $Fv(\theta(x_1) \cup ... \cup \theta(x_k))$ (где $x_1, ..., x_k$ множество всех $x \in dom \theta$)?

ОПРЕДЕЛЕНИЯ:

Определение связанной переменной из 8 §1 главы 2:

Цитата:

8. В формулах вида $\forall x A$, $\exists x A$ выражение $\forall x$ или $\exists x$ называется кванторной приставкой, $x$ - переменной кванторной приставки, а формула $A$ - областью действия квванторной приставки.
Каждое вхождение переменной в формулу мы будем называть свободным или связанным. А именно, вхождение переменной $x$ в формулу $A$ называется связанным, если в $A$ входит формула вида $QxB$, причем рассматриваемое вхождение $x$ в $A$ является вхождением $x$ в эту формулу $QxB$.

Определение из 8 §1 главы 2 того, что переменные терма входят в него свободно:

Цитата:

В атомарную формулу всякая переменная по определению входит свободно. Удобно также считать по определению, что все переменные, входящие в терм, входят в него свободно.

Определение $Fv(A)$ из 9 §1 главы 2:

Цитата:

10. Переменная $x$ называется свободной переменной формулы $A$, или параметром $A$, если $x$ входит (хотя бы один раз) свободно в $A$. Разумеется, при этом $x$ может входить в $A$ и связанно.
Множество всех параметров $A$ обозначим через $Fv(A)$.

Определение конгруэнтности (т.е. бинарного отношения обозначаемого $\approx$) из 12 §1 главы 2:

Цитата:

12. Уточним теперь, что именно означает ситуация, когда две формулы $A$ и $A'$ отличаются друг от друга лишь правильным (т.е. без коллизий переменных) переименованием связанных переменных. В этом случае мы будем говорить, что формулы $A$ и $A'$ конгруэнтны, или что формула $A'$ является вариантом формулы $A$, и писать $A \approx A'$.

...

Можно дать и аккуратное математическое определение отношения $A \approx A'$ индукцией по логической сложности $l(A)$ формулы $A$. А именно:

А) единственным вариантом атомарной формулы является она сама;
Б) если $A$ имеет вид $(B \Delta C)$, то всякий вариант $A'$ формулы $A$ имеет вид $(B' \Delta C')$, где $B \approx B'$ и $C \approx C'$;
если $A$ имеет вид $\neg B$, то всякий вариант $A'$ формулы $A$ имеет вид $\neg B'$, где $B \approx B'$;
В) если $A$ имеет вид $QxB$, то всякий вариант $A'$ формулы $A$ имеет вид $QyC$, где $y$ и $C$ таковы, что для всякой новой переменной $z$ (т.е. не входящей ни свободно, ни связанно в формулы $QxB$ и $QyC$) имеем $B_z^x \approx C_z^y$.

Здесь через $B_z^x$ обозначен результат замещения всех свободных вхождений переменной $x$ в $B$ на переменную $z$. Аналогично понимается $C_z^y$.

Определение формальной подстановки $\theta$ из 2 §2 главы 2:

Цитата:

2. Пусть $T$ - выражение языка $\Omega$ (т.е. формула или терм) и $\theta$ - формальная подстановка $\Bigl(\begin{tabular}{ c c c } x_1, & ..., & x_k \\ t_1, & ..., & t_k \\ \end{tabular}\Bigr)$. Через $(T \theta)$ мы обозначим результат одновременного замещения всех свободных вхождений переменных $x_1, ..., x_k$ в $T$ на термы $t_1, ..., t_k$ соответственно. Конечно, при этом некоторе $x_i$ могут и не входить свободно в $T$. Тогда соответствующие $t_i$ никуда не подставляются и просто не играют никакой роли. Подчеркнем, что замещаются только свободные вхождения $x_i$ в $T$. Вместо $(T \theta)$ будем иногда употреблять одно из следующих обозначений:

$T \theta, \quad T \Bigl(\begin{tabular}{ c c c } x_1, & ..., & x_k \\ t_1, & ..., & t_k \\ \end{tabular}\Bigr), \quad T \begin{tabular}{ c c c } x_1, & ..., & x_k \\ t_1, & ..., & t_k \\ \end{tabular}$.

Дадим теперь индуктивный рецепт для вычисления подстановки в формулу. Этот рецепт можно рассматривать и как самостоятельное индуктивное определение подстановки. Можно убедится с помощью индукции, что оно эквивалентно данному ранее определению.

А. $(P(t_1, ..., t_m)\theta) = P(t_1 \theta, ..., t_m \theta)$.
Б. $(A \Delta B)\theta = (A\theta \Delta B\theta)$,
$(\neg A\theta) = \neg(A\theta)$.
В. $(QzB\theta) = Qz(B(\theta - \{z\}))$.

Здесь через $\theta - {z}$ обозначен результат "выбрасывания" переменной $z$ из области определения $\theta$, т.е. $\theta - {z}$ есть такая подстановка $\theta '$, что
$dom \theta ' = dom \theta \textbackslash \{z\}$ и $\theta ' (x) = \theta (x)$ для всякой переменной $x \in dom \theta '$.

Определение свободной (допустимой) подстановки из 4 §2 главы 2:

Цитата:

4. Заметим теперь, что не все подстановки одинаково пригодны с точки зрения логики.
Пусть, например, в некотором языке атомарная формула $P(x, y, z)$ выражает предикат $x + y = z$, где переменные пробегают натуральные числа $0, 1, 2, ...$. Формула $\exists y P(x, y, z)$ выражает уже предикат от переменных $x$ и $z$, а именно $x \leq z$.
Пусть в этом же языке терм $f(x, y)$ задает операцию умножения натуральных чисел $x \cdot y$. Теперь мы желали бы подставить $f(x, y)$ в $\exists y P(x, y, z)$ вместо переменной $x$ с целью выразить предикат от трех переменных $x \cdot y \leq z$. Однако ошибочно было бы рассмотреть с этой целью формулу $(\exists y P(x, y, z)(\begin{tabular}{ c } x \\ f(x, y) \\ \end{tabular}))$, т.е. формулу $\exists y P(f(x,y), y, z)$. Эта последняя формула выражает совсем имую мысль (в частности, зависимость от двух параметров $x$ и $z$, а не от трех).
Причина затруднения состоит в том, что переменная $y$ была свободна в терме $f(x, y)$, а оказалась связанной в результирующей формуле. Как говорят, произошла коллизия переменных при подстановке.
Правильный подход состоит в том, что сначала следует переименовать связанную переменную $y$, например, образовать формулу $\exists u P(x, u, z)$, которая выражает тот же предикат, а уже затем произвести подстановку, так что в резульате получим формулу $\exists u P( f(x,y), u, z)$, которая и выражает нужный предикат.

5. Выделим теперь класс подстановок, которые заведомо не приводят к коллизии переменных.
Подстановка $\theta$ называется свободной для выражения $T$ (или допустимой для выражения $T$), если для всякой переменной $x \in dom \theta$ любое свободное вхождение $x$ в $T$ не попадает в область действия кванторов по переменным, свободно входящим в терм $\theta(x)$.
Как всегда, мы укажем и индуктивное определение свободной подстановки.

A. Если $T$ - терм или атомарная формула, то всякая подстановка является допустимой для $T$.
Б. $\theta$ свободна для $(A \Delta B)$ $\Leftrightarrow$ $\theta$ свободна для $A$ и $\theta$ свободна для $B$.
$\theta$ свободна для $\neg A$ $\Leftrightarrow$ $\theta$ свободна для $A$.
В. $\theta$ свободна для $QzB$ $\Leftrightarrow$ подстановка $\theta - \{z\}$ свободна для $B$, и, кроме того, для всяков переменной $x \in dom \theta \cap Fv(QzB)$ терм $\theta(x)$ не содержит свободно переменной $z$.

[Xaositect]

creative в сообщении #446249 писал(а):

Вопрос: Зачем вообще вводить свойство чистоты переменных,

Ну, во-первых, этот частный случай доказывает нужное нам утверждение. А еще потому, что именно такие формулы в основном используются на практике. То есть если человек пишет формулу, он напишет ее так, чтобы не путать связанные и свободные переменные, или разные связанные. Вообще, встречаются книги, в которых в определении языка алфавиты свободных и связанных переменных различны. Это позволяет вообще не париться с понятием свободы подстановки для формулы.

[creative]

Не понимаю с первым :

Xaositect в сообщении #446380 писал(а):

Ну, во-первых, этот частный случай доказывает нужное нам утверждение.

Не понимаю какие могут быть противоречия, если в формуле существуют два квантора переменные которых одинаковы по имени. Например:

$(\exists y P(x, y, z) \wedge \forall y Q(x, y))(\begin{tabular}{ c } x \\ f(u, w) \\ \end{tabular})$

Так же непонимаю, что плохого, если связанная переменная в формуле совпадает со свободной переменной. Например:

$(\exists y P(x, y, z) \wedge Q(x, y))(\begin{tabular}{ c } x \\ f(u, w) \\ \end{tabular})$

Я понимаю, что главное только то, чтобы ни один элемент из $Fv(\theta(x_1)) \cup ... \cup Fv(\theta(x_k))$ (где $x_1, ..., x_k \in dom \theta \cap Fv(T)$ ($T$ формула, где производится подстановка)) не был одинаковым по имени со связанной переменной формулы, где производится подстановка. То есть свойство чистоты просто лишним оказывается.

[Xaositect]

Вы правы, здесь достаточно доказать существование формулы, в которой ни одна связанная переменная не входит свободно в $\theta(x_i)$.
Но потом могут потребоваться и более сильное требование чистоты переменных, например, при нахождении предваренной нормальной формы.

[creative]

Xaositect

Большое спасибо!