Past exam of the computer science course of the University of Oxford / 2015 / Logic and proof / 3 / a

Use unary predicates $H$ and $M$ for happiness and merriness, a binary predicate $L$ with $L(x,y)$ meaning that $x$ loves $y$, and a constant symbol $\ell$ for Lucy. The domain consists of people. The following four first-order sentences use this same first-order signature.

The existential quantifier supplies the person loved, with a choice that may depend on $x$:The outer universal quantifier ranges over everyone. The logical disjunction is inclusive; it permits a person both to be happy and to love somebody.

The property of loving at least one person is the antecedent:An equivalent first-order sentence, useful for Skolemization, is $\forall x\forall y[L(x,y)\to L(x,\ell )]$. The person loved in the antecedent need not be Lucy; the conclusion concerns Lucy specifically.

The same person $y$ must both love $x$ and be loved by $x$:Equivalently, use $\forall x\forall y[(L(y,x)\wedge L(x,y))\to H(x)]$. There is no restriction that $x$ and $y$ be distinct; this matters when the later ground resolution proof considers Lucy loving herself.

Lucy's happiness is a single antecedent, while the conclusion applies to everyone:Since $x$ does not occur in the antecedent, this is equivalent to $\forall x[H(\ell )\to M(x)]$. The universal quantifier does not assert that everyone is happy; it is the merriness conclusion that is universal.