Application of the resolution method

Question

The text of logic that I am following give an example of the resolution method to prove the theorem$$\models \forall x((\varphi(x)\rightarrow\psi)\rightarrow(\exists x\varphi(x)\rightarrow\psi)).$$ In order to prove it, the negation of the theorem is reduced to $$\forall x\exists y ((\lnot\varphi(x)\lor\psi)\land\varphi(y)\land\lnot\psi)$$which has the Skolem form$$(\lnot\varphi(x)\lor\psi)\land\varphi(f(x))\land\lnot\psi$$where the universal quantification of $x$ is subtintended and where $f(x)$ represent the "$y$ that exists for all $x$". The last expression is represented in clausal form by $$C_1=\{\lnot\varphi(x),\psi\}$$$$C_2=\{\varphi(f(x))\}$$$$C_3=\{\lnot\psi\}.$$Then the text follows:

Substituting $x$ with $f(x)$ in $C_1$ we get $C_4=\{\lnot\varphi(f(x)),\psi\}$;

Resolving $C_2$ and $C_4$ we get $C_5=\{\psi\}$.

Finally, resolving the third with the fifth clause we determine the empty clause.

I really do not understand why, resolving $C_2$ and $C_4$ we get $C_5=\{\psi\}$: why does not $C_2$ become $(f\circ f)(x)$ if $C_1$ has become $\{\lnot\varphi(f(x)),\psi\}=C_4$, since the argument of $\varphi$ in $C_2$ is the value of $f$ on the argument of $\lnot\varphi$ in $C_1$? I thank everybody for any explanation!

Answer 1

It seems to me that there is something wrong in the problem ...

Let start with $∀x[(φ(x)→ψ)→(∃xφ(x)→ψ)]$; after renaming of second bound $x$, its negation will be :

$$\lnot ∀x[(φ(x)→ψ)→(∃yφ(y)→ψ)] \equiv \exists x \lnot [(φ(x)→ψ)→(∃yφ(y)→ψ)] \equiv $$

$$\equiv \exists x \lnot [(φ(x)→ψ) → \forall y(φ(y)→ψ)]$$

because $y$ is not free in $\psi$.

Now we apply the propositional transformations :

$\exists x [(φ(x)→ψ) \land \lnot \forall y(φ(y)→ψ)] \equiv \exists x [(\lnot φ(x) \lor ψ) \land \forall y(φ(y) \land \lnot ψ)]$.

Finally :

$\exists x \forall y[(\lnot φ(x) \lor ψ) \land φ(y) \land \lnot ψ]$.

Thus, we need only a Skolem constant :

$(\lnot φ(a) \lor ψ) \land φ(y) \land \lnot ψ$.

---

If so, the resolution will be applied :

substituting $y$ with $a$ in $C_2 = \{ \varphi(y) \}$

we get $C_4 = \{ \varphi(a) \}$.

Then we resolve $C_1 = \{ \lnot \varphi(a), \psi \}$ with $C_4 = \{ \varphi(a) \}$, i.e. we apply the Resolution rule :

$$\frac{a \lor b \, \, \, \, \, \, \, \, \, \, \lnot a \lor c}{b \lor c}$$

In our case this amounts to :

$$\frac{\varphi(a) \, \, \, \, \, \, \, \, \, \, \lnot \varphi(a) \lor \psi}{\psi}$$

Thus, the result is $C_5 = \{ \psi \}$.

Finally $C_5$ and $C_3$ will produce the empty clause, thus showing that the original formula is valid.

---

Regarding the formula :

$(¬φ(x)∨ψ)∧φ(f(x))∧¬ψ$

there is no (correct) substitution that con prove it unsatisfiable (i.e. a substitution that can produce the empty clause) because it is satisfiable.

Consider an interpretation nin $\mathbb N$ and let $\psi := (1=0)$. Thus, $\psi \equiv FALSE$ and $\lnot \psi \equiv TRUE$.

With them, we can simplify the above formula as follows :

$[(¬φ(x) ∨ FALSE) ∧ φ(f(x)) ∧ TRUE] \equiv ¬φ(x) \land φ(f(x))$.

Now we can interpret $\varphi$ as $x > 0$ and the functuion $f$ as $S$ (the successor function); thus we have :

$\lnot (x > 0) \land (S(x) > 0)$

which is clearly satisfiable in $\mathbb N$ assigning $0$ as value for the variable $x$.