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

Избавляемся от импликации
¬∃xPx→∀yQy≡¬∃x¬Px∨∀yQy,
проносим внешний знак отрицания до предикатных переменных
¬∃x¬Px∨∀yQy≡∀x¬¬Px∨∀yQy≡∀x¬¬Px&¬∀yQy≡∀xPx&∃yQy
теперь выносим квантор существования по у
∀xPx&∃yQy≡∀x∃yPx&Qy.
2) Избавляемся от импликации
¬P→∃xRx≡¬¬P∨∃xRx
проносим внешний знак отрицания до предикатных переменных
¬¬P∨∃xRx≡¬¬P&¬∃xRx≡P&∀xRx.
3) Избавляемся от эквивалентности
¬∀x∃yAx↔Ay≡¬∀x∃y¬Ax∨Ay&Ax∨¬Ay
проносим внешний знак отрицания до предикатных переменных
¬∀x∃y¬Ax∨Ay&Ax∨¬Ay≡∃x∀y¬¬Ax∨Ay&Ax∨¬Ay≡
≡∃x∀y¬¬Ax∨Ay&Ax∨¬Ay≡∃x∀y¬¬Ax∨Ay∨¬Ax∨¬Ay≡
≡∃x∀y¬¬Ax&¬Ay∨¬Ax&¬¬Ay≡∃x∀yAx&Ay∨Ax&Ay.
При желании можно записать и так:
∃x∀yAx⨁Ay.