Use formal deduction for predicate logic to prove that the following argument is valid:

Question

premise 1: $\forall x \forall y [((A(x)\land A(y)\land \neg I(x,y))\to (R(x,y)\lor R(y,x))]$

premise 2: $\forall x (B(x)\to A(x))$

conclusion: $\forall x \forall y [(B(x)\land B(y)\land \neg I(x,y))\to (R(x,y)\lor R(y,x))]$

You can use any of the 17 rules of formal deduction for predicate logic. Clearly indicate which rules or proved theorems of formal deduction you use.

There are 17 rules of formal deduction for predicate logic:

I've been working on this question for quite some time, truly need help.

Thanks a lot!

Answer 1

In this problem, "all we have to do" is turn the $A$s into $B$s in premise 1, using premise 2. Of course, even the simplest ideas look quite complicated in formal proofs.

Here's some motivation for how to discover this proof: To access those $A$s, we need to "deconstruct" premise 1, and then "reconstruct" it. So we'll have to apply $\forall-$, $\rightarrow-$, and $\land-$ in the first half of the proof, and then $\land+$, $\rightarrow+$, and $\forall+$ in the second half of the proof. The rule $\rightarrow+$ requires an extra hypothesis on the left-hand side of the turnstile $\vdash$, so we have the idea to make an extra assumption from the very beginning, to be discharged by $\rightarrow-$ later.

Let's write $\Sigma$ for your two premises and $\Sigma' = \Sigma,B(a)\land B(b)\land \lnot I(a,b)$, where $a$ and $b$ are variables distinct from $x$ and $y$. Note that by Ref and $+$, we have $\Delta\vdash A$ for any formula $A$ appearing in $\Delta$. Then:

1. $\Sigma'\vdash \forall x\, \forall y\, [(A(x)\land A(y)\land \lnot I(x,y))\rightarrow (R(x,y)\lor R(y,x))]\quad$ by Ref and $+$ (premise 1)
2. $\Sigma'\vdash \forall y\, [(A(a)\land A(y)\land \lnot I(a,y))\rightarrow (R(a,y)\lor R(y,a))]\quad$ by $\forall-$ from 1.
3. $\Sigma'\vdash (A(a)\land A(b)\land \lnot I(a,b))\rightarrow (R(a,b)\lor R(b,a))\quad$ by $\forall-$ from 2.
4. $\Sigma'\vdash \forall x\, (B(x)\rightarrow A(x))\quad $ by Ref and $+$ (premise 2)
5. $\Sigma'\vdash B(a)\rightarrow A(a)\quad $ by $\forall-$ from 4.
6. $\Sigma'\vdash B(b)\rightarrow A(b)\quad $ by $\forall-$ from 4.
7. $\Sigma'\vdash B(a)\land B(b)\land \lnot I(a,b)\quad$ by Ref and $+$ (premise 3 in $\Sigma'$)
8. $\Sigma'\vdash B(a)\quad$ by $\land-$ from 7.
9. $\Sigma'\vdash B(b)\quad$ by $\land-$ from 7.
10. $\Sigma'\vdash \lnot I(a,b)\quad$ by $\land-$ from 7.
11. $\Sigma'\vdash A(a)\quad$ by $\rightarrow-$ from 5. and 8.
12. $\Sigma'\vdash A(a)\quad$ by $\rightarrow-$ from 6. and 9.
13. $\Sigma'\vdash A(a)\land A(b)\land \lnot I(a,b)\quad$ by $\land+$ from 11. and 12. and 10.
14. $\Sigma'\vdash (R(a,b)\lor R(b,a)) \quad$ by $\rightarrow-$ from 3. and 13.
15. $\Sigma\vdash (B(a)\land B(b)\land \lnot I(a,b))\rightarrow (R(a,b)\lor R(b,a))\quad$ by $\rightarrow +$ from 14.
16. $\Sigma\vdash \forall y\, [(B(a)\land B(y)\land \lnot I(a,y))\rightarrow (R(a,y)\lor R(y,a))]\quad$ by $\forall +$ from 15.
17. $\Sigma\vdash \forall x\, \forall y\, [(B(x)\land B(y)\land \lnot I(x,y))\rightarrow (R(x,y)\lor R(y,x))]\quad$ by $\forall +$ from 16.