Помогите закончить приведение к ПНФ. Логика предикатов

[kirflaer]

Здравствуйте. Необходимо привести к предваренной нормальной форме (то есть как я понял чтобы все кванторы были слева) следующую формулу:
$\forall x ( \neg A(x) \to \exists x(B(y))) \to (\neg B(y) \to A(x)) $
Следуя алгоритму найденному на этом форму сначала избавляюсь от импликации:
В правой скобке:
$\forall x ( \neg A(x) \to \exists x(B(y))) \to (B(y) \vee A(x) ) $
В первой скобке
$\forall x ( A(x) \vee \exists x(B(y))) \to (B(y) \vee A(x) ) $
Последняя импликация
$\neg \forall x ( A(x) \vee \exists x(B(y))) \vee (B(y) \vee A(x) ) $
Избавляюсь от отрицания
$\exists x (\neg( A(x) \vee \exists x(B(y)))) \vee (B(y) \vee A(x) ) $
$\exists x (\neg A(x) \wedge \neg\exists x(B(y))) \vee (B(y) \vee A(x) ) $
$\exists x (\neg A(x) \wedge \forall x(\neg B(y))) \vee (B(y) \vee A(x) ) $
В вот дальше затык, не понимаю как вынести квантор общности, и возможно ли это. Заранее спасибо.

[gefest_md]

Почему в данной формуле первый $y$ несвязанный? На каком-то этапе, если я хорошо помню, надо переименовать переменные.

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

gefest_md в сообщении #622683 писал(а):

Почему в данной формуле первый $y$ несвязанный?

Формально это ничему не противоречит. Хотя я, думаю, что тут скорее всего ТС переписывая условие ошибку допустил.

[kirflaer]

Нет при переписывании ошибка допущена не была. Раз 20 сравнил с методичкой. А может быть в принципе нельзя привести к ПНФ?

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

kirflaer в сообщении #622843 писал(а):

А может быть в принципе нельзя привести к ПНФ?

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

Тут просто квантор по $x$ внутри квантора по $x$, и навешан на формулу, в которой $x$ вроде бы как нет. Возможно, в методичке опечатка, а, возможно, так и задумывалось...

-- Пн сен 24, 2012 11:20:20 --

P. S. Скобок много лишних. Некрасиво!

[jinma]

Если действительно не опечатка, а так задумано, то...
квантор всеобщности можно выбросить вообще, потому что верно следующее:
Если (произвольная) формула $Z$ не содержит свободно переменную $x$, то $Z \equiv \forall x Z \equiv \exists x Z$.
Кстати, чтобы формула стала приведённой, нужно не только чтобы все кванторы оказались слева, но и чтобы в области их действия оказалась вся остальная формула. А вот чтобы добиться этого, одну переменную действительно придётся переименовать.