Transform the following formula to clausal form:
$∀x∀y(∃zp(z)∧∃u(q(x, u)→∃vq(y, v)))$
Attempt:
Recall the
Definition: A closed formula is in clausal form if and only if it's prefix are only universal quantifiers.
Thus $∀x∀y(∃zp(z)∧∃u(q(x, u)→∃vq(y, v)))\iff ∀x∀y\ (\lnot(\forall zp(z)\lor \forall u(q(x, u)\to∃vq(y, v)))\iff ? $
I am stuck here, I don't know how to take out the quantifiers $\forall z$ and $\forall u$ without the $\lnot$ ?
Could someone help please?
In general, to transform a first-order formula into a clause form, follow the rules listed here (see also here).
According to that, your formula is transformed as follows ($f,g,h$ are new binary function symbols introduced by Skolemization):
\begin{align} \forall x \forall y \big(\exists z \, p(z) \land \exists u (q(x, u) \to \exists v \, q(y, v)) \big) &\equiv \forall x \forall y \big(\exists z \, p(z) \land \exists u (\lnot q(x, u) \lor \exists v \, q(y, v)) \big) \\ &\equiv \forall x \forall y \exists z \exists u \exists v \big(p(z) \land (\lnot q(x, u) \lor q(y, v)) \big) \\ &\equiv \forall x \forall y \big(p(f(x,y)) \land (\lnot q(x, g(x,y)) \lor q(y, h(x,y))) \big) \end{align}