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.