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!


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 :


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$.

  • $\begingroup$ Anyhow, if we had a Skolem form $(\lnot\varphi(x)\lor\psi)\land\varphi(f(x))\land\lnot\psi$, would it be legitimate to substitute $f(x)$ to $x$ in $\{\lnot\varphi(x),\psi\}$ without substituting $(f\circ f)(x)$ to $f(x)$ in $\{\varphi(f(x))\}$? Thank you very much! (In case it were available to you, the text is Vincenzo Manca's Logica matematica) $\endgroup$ – Self-teaching worker Feb 2 '15 at 17:21
  • 1
    $\begingroup$ @Self-teachingDavide - your concern is right ... in that case, we have to subst e.g. $a$ for $x$ and then $f(x)$ becomes $f(a)$. $\endgroup$ – Mauro ALLEGRANZA Feb 2 '15 at 17:35
  • $\begingroup$ That has given me a headache. Thank you very much, you've saved me from the cephalgia... $\endgroup$ – Self-teaching worker Feb 2 '15 at 17:46

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.