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?
asked Mar 28, 2018 at 5:14 I likeThatMeow I likeThatMeow 460 3 3 silver badges 16 16 bronze badgesIn 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 \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