# Valid inference in first-order predicate logic

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

• The negation of the conclusion is wrong: $¬(∀xAx→∀x¬Bx)$ is: $∀xAx \land ¬∀x¬Bx$. – Mauro ALLEGRANZA Mar 26 '16 at 22:05
• 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)$, – Mauro ALLEGRANZA Mar 27 '16 at 16:03
• 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. – Mauro ALLEGRANZA Mar 27 '16 at 16:06

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.

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