Замена связанных переменных, область действия кванторов

[neverovskii]

Здравствуйте, есть проблемы с пониманием небольшого вопроса о замене связанных переменных. Есть формула $\neg(\exists x)(P(x)\Rightarrow(\exists x)R(x) )$. Нужно произвести замену связанной переменной. Методичное пособие и материалы говорят что заменой будет $\neg(\exists x)(P(x)\Rightarrow(\exists z)R(z) )$. Но почему мы меняем только часть "справа"? Действие квантора $\neg(\exists x)$ распространяется на всю скобку. Я понимаю что замена $\neg(\exists z)(P(z)\Rightarrow(\exists z)R(z) )$ не имеет смысла, но более узкого определения связанной переменной кроме той, "что находится в области действия квантора", я не нашел. У меня есть два объяснения: то, что $\neg(\exists x)$ идет с отрицанием (но тогда можно заменить на $(\forall x)$ перенеся отрицание вперед), и то что квантор должен стоять прямо перед предикатом, или что мы должны идти изнутри формулы наружу. Но я сам не думаю что в этом причина именно такой замены.
Прошу помочь разобраться.

[arseniiv]

neverovskii в сообщении #1432105 писал(а):

Я понимаю что замена $\neg(\exists z)(P(z)\Rightarrow(\exists z)R(z) )$ не имеет смысла

Ну что значит не имеет — эта формула точно так же эквивалентна первой, как и вторая, хотя фактически она получается из первой двумя заменами, а не одной. Одной мы можем получить $\neg(\exists z)(P(z)\Rightarrow(\exists x)R(x))$.

Я бы правда не называл это заменами, синтаксически просто заменой такого не получить, это переименование переменной в кванторной формуле. В исходной формуле две кванторные подформулы — она сама — и тогда переименованием $x$ в $z$ мы получим мою, — и $(\exists x)R(x)$, переименованием $x$ в $z$ в которой мы получим вашу вторую.

Если обозначить замену $v$ на $t$ в $\varphi$ как $\varphi[t/v]$, переименование кванторной переменной в формуле $(\mathsf Qv)\varphi$ на $v'$ определяется как $(\mathsf Qv')(\varphi[v'/v])$. (Заметьте, что мы не можем написать $((\mathsf Qv)\varphi)[v'/v]$, потому что $v$ не свободна в $(\mathsf Qv)\varphi$ и не заменится.) Вообще надо сначала разобраться, чем плоха исходная формула и хороша вторая, тогда и будет яснее, почему что-то переименовывается.

[neverovskii]

arseniiv в сообщении #1432132 писал(а):

Вообще надо сначала разобраться, чем плоха исходная формула и хороша вторая, тогда и будет яснее, почему что-то переименовывается.

Да, надо было сказать что это все делается для приведения в предваренную нормальную форму, для использования метода резолюций. В этом примере — конечная предваренная форма $(\forall x)(\forall z)(P(x)\wedge \neg R(z))$. Если начать с другого конца, с преобразования импликации и протаскивания внутрь отрицаний (это, вроде, не возбраняется, могут получиться разные, но эквивалентные формулы) то можно прийти к $(\forall x)(P(x)\wedge (\forall x)\neg R(x))$. Однако продолжить и вынести квантор можно уже только с заменой переменной. Тогда, наверное, нужно мыслить что раз мне нужно вынести квантор, то я делаю замену именно в этой связке квантор-предикат, то есть в моем случае в $(\exists x)(R(x))$, потому что действительно, в ваших преобразованиях тоже нет ничего плохого .

[george66]

Здесь левая переменная глобальная, а правая локальная, как в программировании. Локальная "забивает" глобальную в своей области видимости.

[arseniiv]

Да, раз квантор поехал из глубины наружу, то надо удостовериться, что он не захватит переменные, которые к нему отношения не имели, но назывались так же, и самый простой способ — переименовать именно его переменную в какую-то новую не имеющую шанса совпасть.