Prenex normal form and Skolemisation

1. The $\forall x$ comes out of the left-hand side of $\to$ and becomes $\exists x$: $\exists x\, \exists y\, (P(x) \to Q(y))$.
2. $\forall x\, \lnot(P(x) \land \forall y\, R(x, y)) \equiv \forall x\, (\lnot P(x) \lor \exists y\, \lnot R(x, y)) \equiv \forall x\, \exists y\, (\lnot P(x) \lor \lnot R(x, y))$.
3. Rename: $\forall x\, P(x) \land \exists z\, Q(z)$, then $\forall x\, \exists z\, (P(x) \land Q(z))$. (Or $\exists z\, \forall x\, (P(x) \land Q(z))$: the two are equivalent, because the two quantifiers range over independent parts.)
4. The $\exists x$ comes out of the left-hand side and becomes $\forall x$; then $\forall y$ and $\exists z$ come out of the right-hand side: $\forall x\, \forall y\, \exists z\, (P(x) \to Q(y) \lor R(y, z))$.

1. $y$ depends on $x$: $f(x)$; $w$ depends on $x$ and $z$: $g(x, z)$. $\forall x\, \forall z\, R(x, f(x), z, g(x, z))$.
2. $x$ depends on nothing: a constant $a$. $\forall y\, R(a, y)$.
3. $z$ depends on $x$ and $y$: $\forall x\, \forall y\, (R(x, h(x, y)) \land R(h(x, y), y))$.
4. Two fresh constants: $\forall z\, (R(a, z) \to R(z, b))$.

1. In every model of $P(a)$, the object $a^{\mathcal{M}}$ satisfies $P$: so there exists an $x$ that satisfies $P$.
2. $D = \{1, 2\}$, $a$ interpreted as 1, $P = \{2\}$: $\exists x\, P(x)$ is true, $P(a)$ false.
3. Resolution tries to show that a set has no model. Now $\exists x\, P(x)$ has a model if and only if $P(a)$ has one (with $a$ fresh): in a model of $\exists x\, P(x)$, it suffices to interpret $a$ as an object that satisfies $P$. The two are equisatisfiable, and that is all resolution uses.

• $\forall x\, (C(x) \to G(x))$: clause $\lnot C(x) \lor G(x)$.
• $\forall x\, (C(x) \to \mathit{Car}(x))$: clause $\lnot C(y) \lor \mathit{Car}(y)$ (variable renamed).
• $\exists x\, C(x)$: Skolemisation, $C(a)$ with $a$ fresh.
• $\lnot A = \lnot \exists x\, (\mathit{Car}(x) \land G(x)) \equiv \forall x\, (\lnot \mathit{Car}(x) \lor \lnot G(x))$: clause $\lnot \mathit{Car}(z) \lor \lnot G(z)$.

Had we Skolemised $A$ before negating it, we would have obtained $\lnot(\mathit{Car}(b) \land G(b))$, which only says that $b$ is not a carnivore with claws: much weaker than $\lnot A$.