2
$\begingroup$

I should prove for the following premises and conclusion if the inference/conclusion is valid by using general resolution for clauses.

The conclusion is valid if it is possible to derivate a contradiction. After that Put every formula in prenex-form and in skolem-form. Then Create clauses for every formula. Finally Use general resolution for inference.

Negate the conclusion:

$ \forall x Ax \land \lnot \forall x \lnot Bx $

The second step. Put every premise in prenex-form.

The first part:

1.$ \forall x \; (Ax \rightarrow \exists y \; Rxy) $
2.$ \forall x \; \exists y \; (Ax \rightarrow \; Rxy) $ .Extract the $\exists y $
3.$ \forall x \; \exists y \; (\lnot Ax \lor Rxy) $. Disjunction instead of implication.
4.$ \forall x \; (\lnot Ax \lor Rxf(x)) $. Skolem-function for $ \exists y $

The second part of the premise:

1.$\forall x \; \forall y \; (Rxy \rightarrow \lnot Bx) \;$
2. $ \forall x \; \forall y \; (\lnot Rxy \lor \lnot Bx) \;$.Disjunction instead of implication.

In program format:
1.$ Rxf(x) \leftarrow Ax $
2.$ Rxy, Bx \leftarrow $

The third part (the negated conclusion):

1.$ \forall x Ax \land \lnot \forall x \lnot Bx $
2.$ \forall x Ax \land \lnot \forall z \lnot Bz $ .Alphabet
3.$ \forall x Ax \land \exists z \; \lnot \lnot Bz $ .Extract the $ \forall z $
4.$ \forall x Ax \land \exists z \; Bz $ . Remove the $\lnot \lnot $.
5.$ \forall x \exists z \; Ax \land Bz $
6.$ \forall x \; Ax \land \forall x Bg(x) $ . Replace the $\exists z $ for a skolem-function.

The set of clauses is: {$\lnot Ax \lor Rxf(x), \lnot Rxy \lor \lnot Bx), \leftarrow Ax, Bg(x)$}

The goal in clause-form:
1.$ \leftarrow Ax $
2.$ \leftarrow Bg(x) $

Deriving the contradiction by using general resolution for clauses.

1'.$ \leftarrow Ax $. First goal
2'.$ Rxf(x) \leftarrow Ax $ .Sentence 1
3'.$ Rxf(x) \leftarrow $ . Res. 1,2. $ ,\; \theta =[x/x] $
4'.$ \leftarrow Rxy, Bx $ Sentence 2
5'.$ Bg(x) \leftarrow $. Second goal
6'.$ \leftarrow Rxy \; $ Res. 4,5. $ \theta =[g(x)/x] $
7'.$ \; \square \; $Re. 3,6 $ \theta =[f(x)/y] $

$\endgroup$
  • $\begingroup$ The negation of the conclusion is wrong: $¬(∀xAx→∀x¬Bx)$ is: $∀xAx \land ¬∀x¬Bx$. $\endgroup$ – Mauro ALLEGRANZA Mar 26 '16 at 22:05
  • $\begingroup$ I'm not sure that you can use the same skolem function $f$ twice... To me, we have four clauses: 1) $¬Ax ∨ Rxf(x)$ 2) $¬Rxy ∨ ¬Bx$ 3) $Ax$ 4) $Bg(x)$, $\endgroup$ – Mauro ALLEGRANZA Mar 27 '16 at 16:03
  • $\begingroup$ With resolution on 3) and 1) we have: 1') $Rxf(x)$ 2) $¬Rxy ∨ ¬Bx$ 4) $Bg(x)$. Susbt $g(x)$ for $x$ and $f(x)$ for $y$ we get: 1'') $Rg(x)f(x)$ 2') $¬Rg(x)f(x)$ and we are done. $\endgroup$ – Mauro ALLEGRANZA Mar 27 '16 at 16:06
1
$\begingroup$

Your strategy, if it is one, is all over the place and much too complicated. The point is to distribute the quantifiers across the implications, using one "trick" re the $y$ quantifier. The last step of the proof is then just propositional logic (a syllogism!).

Note that for any formulas $p(x), q(x)$, possibly with other free variables, $$ \forall x\,(p(x)\to q(x)) \vdash (\forall x\,p(x)\to \forall x\,q(x))\tag{1} $$ Also note that if $y$ is not free in $t$, then $$ \forall y\,(s(y)\to t) \equiv (\exists y\,s(y)\to t)\tag{2} $$ This is true because $(s(y)\to t) \equiv (\neg s(y)\lor t)$, and if $y$ is not free in $t$ then $\forall y\,(\neg s(y)\lor t) \equiv (\forall y\,\neg s(y)\lor t)$. Using $\forall \neg\equiv \neg \exists$, the last formula is equivalent to $(\neg \exists y\,s(y)\lor t)$, and thus to $(\exists y\,s(y)\to t)$.

Using (1), from your first premise $\forall x \, (Ax \rightarrow \exists y \, Rxy)$ we can infer $$ \forall x \, Ax \to \forall x \,\exists y \, Rxy.\tag{I} $$ Using (2), your second premise is equivalent to $$\forall x \, (\exists y \, Rxy \to \lnot Bx)\tag{pre-II}, $$ and applying (1) to (pre-II) we can derive $$ \forall x \,\exists y \, Rxy \to \forall x \,\neg Bx\tag{II}. $$ Now, from (I) and (II), just by propositional logic, we can conclude: $$ \forall x \, Ax \to \forall x \,\neg Bx, $$ which is what you wanted to derive.

$\endgroup$
0
$\begingroup$

Not sure if this will help in your system, but here is how I would prove the required result using my own "ordinary rules of logic" (without Skolem functions, non-empty domains, etc.) Perhaps you can translate it into your system.

Part 1: Prove that $\forall x:[A(x) \implies \neg B(x)]$

  1. Suppose $A(t)$

  2. From premise #1, $A(t) \implies \exists y:R(t,y)$

  3. From (1) and (2), $\exists y:R(t,y)$

  4. From (3), $R(t,u)$

  5. From premise #2 and (4), $\neg B(t)$

  6. From (1) and (5), we can conclude that $\forall x:[A(x) \implies \neg B(x)]$


Part 2: Prove by contradiction that $\forall x:A(x)\implies \forall x: \neg B(x)$

  1. Suppose $\forall x: A(x)$

  2. Suppose to the contrary that we have $B(v)$

  3. From (6) $A(v)\implies \neg B(v)$

  4. From (7) $A(v)$

  5. From (9) and (10), we obtain the contradiction $\neg B(v)$

  6. From (8) and (11), we can conclude that $\forall x:\neg B(x)$ (by contradiction)

  7. From (7) and (12), we can conclude, as required, that $\forall x:A(x)\implies \forall x: \neg B(x)$

$\endgroup$

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.