I'm given the following question:
Convert the following WFF into clausal form:
\begin{equation*}
\forall(X)(q(X)\to(\exists(Y)(\neg(p(X,Y)\vee r(X,Y))\to h(X,Y))\wedge f(X)))
\end{equation*}
This is what I've gotten so far, but I'm not confident that I'm in the proper form at the end.
First, eliminate the implications:
\begin{gather}
\forall(X)(q(X)\to(\exists(Y)((p(X,Y)\vee r(X,Y))\vee h(X,Y))\wedge f(X)))\\
\forall(X)(\neg q(X)\vee(\exists(Y)((p(X,Y)\vee r(X,Y))\vee h(X,Y))\wedge f(X)))
\end{gather}
Move the quantifiers out front:
\begin{gather}
\forall(X)\exists(Y)(\neg q(X)\vee((p(X,Y)\vee r(X,Y)\vee h(X,Y))\wedge f(X)))
\end{gather}
Skolemize existential quantifiers with $g(X)/Y$:
\begin{gather}
\forall(X)(\neg q(X)\vee((p(X,g(X))\vee r(X,g(X))\vee h(X,g(X)))\wedge f(X)))
\end{gather}
Remove universal quantifiers:
\begin{gather}
\neg q(X)\vee((p(X,g(X))\vee r(X,g(X))\vee h(X,g(X)))\wedge f(X))
\end{gather}
Best Answer
To write $\neg q(X)\lor\Big(\big(p(X,g(X))\lor r(X,g(X))\lor h(X,g(X))\big)\land f(X)\Big)$ in clausal form, you first need to put it in conjunctive normal form. To do so, you can distribute the first disjunction over the paranthesis to yield: $$\big(\neg q(X)\lor f(X)\big)\land\big(\neg q(X)\lor p(X,g(X))\lor r(X,g(X))\lor h(X,g(X))\big)$$ Each part of the conjunction corresponds to a clause, which is a finite disjunction of atomics. Thus, the clausal form of your original wff is: $$\bigg\{\Big\{\neg q(X),f(X)\Big\},\Big\{\neg q(X),p(X,g(X)),r(X,g(X)),h(X,g(X))\Big\}\bigg\}$$