Приведение формул к предваренной форме

[Getch]

Приветствую!
Дана формула привести её к предваренной форме.
$ (\forall x \exists y A(x, y))\vee ( \forall x \exists y B(x, y))$ мне кажется естественным по закону дистрибутивности
получить $ \forall x \exists y (A(x, y)\vee B(x, y)) $ но думаю это было бы слишком просто.
Не могли бы вы подсказать первый шаг или возможно какой то "закон" который от меня убежал.
Заранее спасибо.
Пардон я допустил ошибку в записи. Уже исправил.

[svv]

Не знаю, что такое предваренная форма, но хочу показать на примере, что такой вывод не может быть верным.

$\forall x$
Для любого момента времени $x$
$\exists y$
существует птичка $y$,
$A(x, y)$
такая, что в момент $x$ эта птичка $y$ сидит на ветке;
$\wedge$ и
$\forall x$
для любого момента времени $x$
$\exists y$
существует птичка $y$,
$B(x, y)$
такая, что в момент $x$ эта птичка $y$ летит.

Но неверен вывод:
$\forall x$
для любого момента времени $x$
$\exists y$
существует птичка $y$,
$A(x, y) \wedge B(x, y)$
такая, что в момент $x$ эта птичка $y$ сидит на ветке и летит.

Т.е. хотя существует такой $y$, для которого верно $A$, и существует такой $y$, для которого верно $B$, эти свойства не обязаны для некоторого $y$ совмещаться.

-- Чт мар 15, 2012 19:13:19 --

Для $\vee$ -- верно.

[Профессор Снэйп]

А предварённая форма - это что такое? Это когда все кванторы впереди, а бескванторная часть может быть какой попало? Или как-то иначе?

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

[Getch]

Формула А находится в предваренной форме, если она имеет следуюший вид: A=Q1x1...Qnxn B(x1..xn), где

Q1 – некоторые кванторы;
В – бескванторная формула;
приставка Q1x1..Qnxn - префикс;
формула В – матрицa.
Итак алгоритм таков:
1) Избавляетесь от импликаций. (тут их нет)
2) Проносите отрицания под кванторы. (Отрицания тоже нет)
Ага

$$ \exists u \Phi(u) \vee \exists u \Psi(u) \equiv \exists u \big(\Phi(u) \vee \Psi(u)\big) $$

$$ \forall u \Phi(u) \mathbin{\&} \forall u \Psi(u) \equiv \forall u \big(\Phi(u) \mathbin{\&} \Psi(u)\big) $$

НО!!! При этом

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

$$ \exists u \Phi(u) \mathbin{\&} \exists u \Psi(u) \not\equiv \exists u \big(\Phi(u) \mathbin{\&} \Psi(u)\big) $$

Значит как я написал нельзя делать.
получается $ \exists y (( \forall x A(x, y) ) \vee ( \forall x B(x, y) )) $
если я прав ставим + ))

[Getch]

И еще у меня вопрос на счет отрицания. Основные формулы я нашел. какие из следующих формул справедливы?
$ \forall x \neg\neg A(x, y) \equiv \forall x A(x, y)$
$ \neg \forall x \neg A(x, y) \equiv \exists x A(x, y) $

-- 16.03.2012, 12:20 --

И если в посте выше все верно ..
$\exists y(\neg \neg (\forall x A(x,y)) \vee \neg \neg(\forall x B(x,y))) $
$ \exists y ( \neg(\exists x \neg A(x,y) ) \vee \neg (\exists x \neg B(x,y)))$
$ \exists y \neg( (\exists x \neg A(x,y) ) \mathbin{\&} (\exists x \neg B(x,y))) $
$ \exists y \neg( \neg (\forall x A(x,y) ) \mathbin{\&} \neg (\forall x B(x,y))) $
$ \exists y \neg\forall x ((\neg A(x,y) ) \mathbin{\&} (\neg B(x,y))) $
$ \exists y \neg\forall x (\neg( A(x,y) \vee B(x,y) )) $

? )))

[Профессор Снэйп]

Getch в сообщении #548852 писал(а):

какие из следующих формул справедливы?

Обе справедливы.

Алгоритм, я так понял, Вы нашли. Вот и здорово. Не знаю, что там может быть непонятного.

Getch в сообщении #548852 писал(а):

И если в посте выше все верно ..

Откуда у Вас какие-то отрицания появились? Их же изначально не было!

-- Пт мар 16, 2012 14:37:00 --

От отрицаний надо избавляться поелику это возможно. А новых вводить ни в коем случае не следует!!!

[Getch]

Я внес. Ну вот смотрите как у меня получилось я пост исправил..
Хех тогда я в тупике ) $ \forall x $ не знаю как вынести

[Профессор Снэйп]

Один из возможных правильных ответов на Вашу задачу следующий:

$$ \forall x \forall z \exists y (A(x,y) \vee B(z,y)) $$

Проделайте шаги описанного мною алгоритма так, чтобы прийти именно к этой формуле.

P. S. Дайте, пожалуйста, ссылку на тот мой пост, где описан алгоритм приведения к пнф. А то я сам её не помню, а Вы, похоже, нашли

-- Пт мар 16, 2012 14:45:50 --

Getch в сообщении #548859 писал(а):

Хех тогда я в тупике ) $ \forall x $ не знаю как вынести

Меняйте связанную переменную! Там, куда я Вас посылал, всё написано.

[Getch]

topic13252.html?hilit=предваренной форме предваренной&start=15
Да, это мне в голову приходило но так не хотелось чтобы это было правдой))

[Профессор Снэйп]

Getch в сообщении #548840 писал(а):

если я прав ставим + ))

Минус, минус, минус, минус, минус...

Кванторы переставлять местами нельзя. Это самая страшная ошибка, какую только можно допустить!!!!

Сами подумайте. Для любого человека существует отец. Но ведь неверно, что существует отец всех людей!

[Getch]

Итак мой ответ не много не как у вас но ..
$ \exists y (\forall x A(x,y) \vee (\forall x B(x,y)))$
$ \exists y (\forall z A(z,y) \vee (\forall x B(x,y)))$
$ \exists y \forall z( A(z,y) \vee (\forall x B(x,y)))$
$ \exists y \forall z \forall x( A(z,y) \vee B(x,y))$
вот. Стреляйте!))

[Профессор Снэйп]

Стреляю! В упор и наповал. Материться охота!!!

НАХРЕНА КВАНТОРЫ ПЕРЕСТАВИЛ МЕСТАМИ?!! НЕЛЬЗЯ ЭТОГО ДЕЛАТЬ НИ В КОЕМ СЛУЧАЕ!!!

[Getch]

Ах да. Это от неопытности, невнимательности и еще чего то.

$ (\forall x \exists y A(x,y) \vee (\forall x \exists yB(x,y)))$
$ (\forall z \exists yA(z,y)) \vee (\forall x \exists y B(x,y)))$
$ \forall z(( \exists yA(z,y)) \vee (\forall x \exists yB(x,y)))$
$ \forall z \forall x( (\exists y A(z,y)) \vee (\exists y B(x,y)))$
$ \forall z \forall x \exists y( A(z,y) \vee B(x,y))$

Ну вроде, с десятой попытки, все верно .

[Профессор Снэйп]

Да, теперь всё верно.