Привести к ПНФ заданную формулу логики предикатов

[convert]

Здравствуйте!
Помогите пожалуйста разобраться в одной задаче по матлогике.
Буду рад, если кто проверит мое решение и поможет разобраться до конца.

Нужно привести к предваренной нормальной форме заданную формулу логики предикатов.

$$ \forall x \big(P(x) \wedge \forall y \exists x (Q(x,y) \vee \forall z R(a,x,y))\big) $$

Предваренная нормальная форма - это форма, в которой все кванторы стоят сначала, а за ними следует выражение в конъюнктивной нормальной форме (конъюнкция элементарных дизъюнкций).

То есть, по сути надо вытащить все кванторы наружу и представить оставшееся выражение в КНФ.
Есть такая эквивалентность, которая справедлива при условии что $u$ не входит в $\Phi$:

$$\Phi \vee \forall u \Psi \equiv \forall u (\Phi \vee \Psi)$$

По идее, я могу вынести $\forall z$, так как $z$ не входит в $Q(x,y)$.
Но меня беспокоит то, что $z$ и в $R(a,x,y)$ не входит. Я не знаю как поступать в таком случае. Возможно $\forall z$ следовало просто исключить, можно ли так делать? Но я все же вынес. Вот это та проблемная ситуация, в которой я не уверен.

В общем, вынес:

$$ \forall x \big(P(x) \wedge \forall y \exists x \forall z (Q(x,y) \vee R(a,x,y))\big) $$

Теперь, согласно этим эквивалентностям:

$$\Phi \wedge \forall u \Psi \equiv \forall u (\Phi \wedge \Psi)$$ $$\Phi \wedge \exists u \Psi \equiv \exists u (\Phi \wedge \Psi)$$

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

$$ \forall x \big(P(x) \wedge \forall y \exists t \forall z (Q(t,y) \vee R(a,t,y))\big) $$

Насколько мне известно, замена делалась бы только в случае, если перед $P(x)$ стояло бы $\exists x$, так как:

$$ (\exists x P(x)) \wedge (\exists x Q(x)) \equiv \exists x \exists t (P(x) \wedge Q(x)) $$

А в моем случае этого квантора перед $P(x)$ нету. Получается, делать замену не надо? Просто выношу?

$$ \forall x \forall y \exists x \forall z \big(P(x) \wedge (Q(x,y) \vee R(a,x,y))\big) $$

Выражение после кванторов и так в КНФ, значит это все.
Но вот все равно чувствую что что-то не так, не до конца понимаю.
Помогите пожалуйста разобраться, в чем косяки.

[Sonic86]

convert в сообщении #1145439 писал(а):

Но меня беспокоит то, что $z$ и в $R(a,x,y)$ не входит. Я не знаю как поступать в таком случае. Возможно $\forall z$ следовало просто исключить, можно ли так делать?

Можно. А на практике даже нужно.

convert в сообщении #1145439 писал(а):

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

$$ \forall x \big(P(x) \wedge \forall y \exists t \forall z (Q(t,y) \vee R(a,t,y))\big) $$

Замену $x$ на $t$ делать не только стоит, но и обязательно, иначе будет неэквивалентное преобразование и т.н. коллизия переменных.

convert в сообщении #1145439 писал(а):

Насколько мне известно, замена делалась бы только в случае, если перед $P(x)$ стояло бы $\exists x$

Она делается для любого квантора (хотя бы из двойственности это следует)

convert в сообщении #1145439 писал(а):

$$ (\exists x P(x)) \wedge (\exists x Q(x)) \equiv \exists x \exists t (P(x) \wedge Q(x)) $$

Опечатались?

[convert]

Sonic86 в сообщении #1145563 писал(а):

Опечатались?

Нет, это формула из видео: https://youtu.be/n0ViBuKcbKk?t=5m41s
В тех примерах в принципе понятно, почему делалась замена.
Это для случаев, когда перед каждым выражением (или правильно сказать предикатом?) стоял бы квантор и нужно было бы их вынести.
Однако в моем примере квантор был только у одного.

$$ \forall x \big(P(x) \wedge \forall y \exists x (Q(x,y) \vee R(a,x,y))\big) $$

Кажется я начинаю понимать.
Обозначим за $P(x)$ за $\Phi$, а остальную часть за $\Psi$.
По идее, можно воспользоваться эквивалентностями ниже, чтобы вынести $\forall y \exists x$.

$$\Phi \wedge \forall u \Psi \equiv \forall u (\Phi \wedge \Psi)$$ $$\Phi \wedge \exists u \Psi \equiv \exists u (\Phi \wedge \Psi)$$

Но как я уже писал, они справедливы при условии что $u$ не входит в $\Phi$.

Но ведь тогда в моем случае $x$ будет входить и в $\Phi$, и в $\Psi$. И поэтому я не могу использовать эти эквивалентности.
Или же могу, но только если сделаю замену? То есть эти эквивалентности все равно справедливы, главное лишь переименовать переменные?

$$\forall x \forall y \exists t \big(P(x) \wedge (Q(t,y) \vee R(a,t,y))\big)$$

Если я все понял верно, это правильное решение?

[Sonic86]

convert в сообщении #1145575 писал(а):

Нет, это формула из видео: https://youtu.be/n0ViBuKcbKk?t=5m41s

Значит у него там тоже опечатка.

convert в сообщении #1145575 писал(а):

Или же могу, но только если сделаю замену? То есть эти эквивалентности все равно справедливы, главное лишь переименовать переменные?

Да, да, именно так.
Скачайте Верещагина, Шеня, Матлогику 4-е издание. В главе 4 про исчисление предикатов есть целая подглавка про переименование переменных.
А в Бурбаках связанные переменные вообще выкидывали и заменяли на квадратики, связанные палочками. Тогда вообще вопросов не возникало. Связанные переменные безымянны - их наименование неважно, потому их можно менять произвольно.

convert в сообщении #1145575 писал(а):

Если я все понял верно, это правильное решение?

Да.

[convert]

Спасибо огромное за помощь!

Sonic86 в сообщении #1145704 писал(а):

Значит у него там тоже опечатка.

А все же опечатка была моя.
Вместо:

$$ (\exists x P(x)) \wedge (\exists x Q(x)) \equiv \exists x \exists t (P(x) \wedge Q(x)) $$

Должно быть:

$$ (\exists x P(x)) \wedge (\exists x Q(x)) \equiv \exists x \exists t (P(x) \wedge Q(t)) $$

Хотя в видео опечатка возможно тоже есть, в последнем пункте:

$$ (\forall x P(x)) \vee (\forall x Q(x)) \equiv \forall x \forall y (P(x) \vee Q(x)) $$

Должно быть:

$$ (\forall x P(x)) \vee (\forall x Q(x)) \equiv \forall x \forall y (P(x) \vee Q(y)) $$

Верно?

[Sonic86]

convert в сообщении #1145729 писал(а):

Верно?

Угу