Valid inference in first-order predicate logic

Question

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

Answer 1

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.

Answer 2

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

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

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

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

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

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

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

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