Proving implicature fact $\Gamma \models D$.

Question

I would like to prove the following: We have the sentences (1) $\forall \, x \, (\neg Ax \rightarrow \neg \exists \, t \,(Bt \wedge Rtx))$; (2) $\neg \exists \, x \, (Cx \wedge Ax)$. I will write $\Gamma$ for the two taken together. Show that $\Gamma$ implies $D=\neg \exists \, t \, \exists \, x(Bt \wedge Cx \wedge Rtx)$. This is an implicature fact used in Boolos $\textit{Computability and Logic}$ in their proof of the undecidability of FOL via Turing machines.

I reason by interpretations; namely, since we wish to show that $\Gamma \models D$, i.e., there is not an interpretation $I$ that makes $\Gamma$ true and $D$ false, we can assume that there is an $I$ such that $I \models \Gamma$ but $I \not\models D$ and thereby derive a contradiction.

Now, $I \not \models D$ is given by $I \models \neg (\neg \exists \, t \, \exists \, x(Bt \wedge Cx \wedge Rtx)) \equiv \exists \, t \, \exists \, x \, (Bt \wedge Cx \wedge Rtx)$. Here I instantiate my variables $t, x$ using objects $a,b$ respectively in the domain of the interpretation. Thus, we have $I \models (B(a) \wedge C(b) \wedge R(a,b))$.

Now handle the premises. We drive in the negation for each sentence to get that $I \models (\forall \, x \, (\neg Ax \rightarrow \forall \, t \, (\neg Bt \vee \neg Rtx)) \wedge \forall \, x \, (\neg Cx \vee \neg Ax))$. After this reduction we can instantiate with objects from the domain of $I$. Since we now have only universal quantifiers for our variables, we are free to choose $a,b$ as our objects again. Thus, $I \models (\neg A(b) \rightarrow (\neg B(a) \vee \neg R(a,b)) \wedge (\neg C(b) \vee \neg A(b))$. Given this instantiation, it appears we cannot get both the premises and conclusion to be true. Contradiction, thus, $\Gamma \models D$.

Is my reasoning here correct (in particular my instantiations)? Is this the best way to approach the problem? Are there any interesting ways to proceed without appealing to this reduction process for interpretations? Finally, does any information have to be explicitly given in using this method? To me, it would appear not.

Answer 1

Long comment

It seems right to me.

We can "verify" it with a simple derivation :

1) $∀x(¬Ax→¬∃t(Bt∧Rtx))$ --- premise

2) $¬∃x(Cx∧Ax)$ --- premise

3) $Ax \lor ¬∃t(Bt∧Rtx)$ --- from 1) by instantiation and the tautological equivalence : $\lnot p \to q \equiv p \lor q$

4) $\lnot Cx \lor \lnot Ax$ --- from 2) by the equivalence between $¬∃$ and $∀¬$ and De Morgan

Now we need a poof by cases (or : Disjunction elimination) on 4) :

5) $\lnot Cx$ --- temporary assumption from 4)

6) $\lnot Bt \lor \lnot Cx \lor \lnot Rt$ --- from 5 by Disjunction introduction

7) $\lnot (Bt \land Cx \land Rt)$ --- from 6) by De Morgan

8) $\lnot Ax$ --- temporary assumption from 4)

9) $¬∃t(Bt∧Rtx)$ --- from 3) and 8) by Modus Tollens

10) $\lnot Bt \lor \lnot Rt$ --- from 9) by the equivalence between $¬∃$ and $∀¬$, instantiation and De Morgan

11) $\lnot (Bt \land Cx \land Rt)$ --- from 10) by Disjunction introduction and De Morgan.

Thus, having proved $\lnot (Bt \land Cx \land Rt)$ both from assuptions 5) and 8), we may discharge them and conclude by proof by cases (from 4) with :

12) $\lnot (Bt \land Cx \land Rt)$

and thus, by generalization :

13) $\forall t \forall x \lnot (Bt \land Cx \land Rt)$.