= Solution
First convert the four <first-order sentences> to <clausal form>. In the first, pull the <existential quantifier> across the <logical disjunction>, then replace its witness by a fresh unary <Skolem function> $f(x)$. The usual nonempty-domain convention for <first-order logic> makes this transformation valid even when $H(x)$ already holds. The four <Skolem normal forms> are
$$
\begin{aligned}
A'&=\forall x\,[H(x)\lor L(x,f(x))],\\
B'&=\forall x\forall y\,[\neg L(x,y)\lor L(x,\ell)],\\
C'&=\forall x\forall y\,[\neg L(y,x)\lor\neg L(x,y)\lor H(x)],\\
D'&=\forall x\,[\neg H(\ell)\lor M(x)].
\end{aligned}
$$
The <Skolemization> of $A$ preserves satisfiability in an expanded <first-order signature>; it does not assert <logical equivalence> for every arbitrary interpretation of the new <Skolem function>. The other three <first-order sentences> only require elimination of implications and movement of <universal quantifiers>.
For a <ground resolution> refutation, negate the desired conclusion and introduce a fresh constant $c$ for a person who is not merry. This adds the <ground clause> $\neg M(c)$. Use these ground instances of the four universal <first-order sentences>:
$$
\begin{aligned}
K_1&=H(\ell)\lor L(\ell,f(\ell)),\\
K_2&=\neg L(\ell,f(\ell))\lor L(\ell,\ell),\\
K_3&=\neg L(\ell,\ell)\lor H(\ell),\\
K_4&=\neg H(\ell)\lor M(c),\\
K_5&=\neg M(c).
\end{aligned}
$$
Here $K_3$ comes from $C'$ with $x=y=\ell$, after removing a duplicate negative literal. All <first-order terms> in these <ground clauses> are ground. Resolving gives
$$
\begin{aligned}
K_6&=\operatorname{Res}_{L(\ell,f(\ell))}(K_1,K_2)
=H(\ell)\lor L(\ell,\ell),\\
K_7&=\operatorname{Res}_{L(\ell,\ell)}(K_6,K_3)=H(\ell),\\
K_8&=\operatorname{Res}_{H(\ell)}(K_7,K_4)=M(c),\\
K_9&=\operatorname{Res}_{M(c)}(K_8,K_5)=\square.
\end{aligned}
$$
Repeated positive literals in $K_7$ have again been removed. The empty <ground clause> proves unsatisfiability of the premises together with the negated conclusion. Therefore
$$
\boxed{A,B,C,D\models\forall x\,M(x).}
$$
The key is to apply the first three premises to Lucy herself: either she is already happy, or she loves somebody, hence loves herself, which forces her happiness and activates the final premise.
Back to article page
