Symbolic logic proof

Question

Can any one please give me the correct proof for this, i got this far but i am stuck.

Thank you!

Answer 1

In (3) you have correctly "instantiated" (1) with $a$ new.

Then you have correctly assumed $Fa$ in order to derive by $\rightarrow$-elim : $\exists z \lnot R(a,z)$.

Now you "instantiate" it , preliminary to $\exists$-elimination, with $b$ new, to get : $\lnot R(a,b)$.

But from (3), by $\land$-elim, you have also $\forall z R(a,z)$.

Thus, you can use $b$ to get : $R(a,b)$.

Now you have your contradiction, with $R(a,b)$ and $\lnot R(a,b)$, i.e $\bot$.

But you have derived $\bot$ "under the assumption" 9 for $\exists$-Elimination.

Applying this rule [see Comment] in your example, we have that $\bot$ is your $\theta$, and you can conclude it "discharging" the assumption $¬R(a,b)$ in 9 [which is the $\sigma(b)$ of the rule], because you have $∃z¬R(a,z)$ in 8 [i.e. the $\exists z \sigma(z)$ of the rule].

Now, having derived $\bot$, you can use $\lnot$-intro to discharge the assumption $Fa$ and derive $\lnot Fa$ (this is your new step 13).

With (4) : $Ga$

and (13) : $\lnot Fa$

you can use $\land$-intro to derive :

(14) $Ga \land \lnot Fa$

and then conclude with $\exists$-intro :

(15) $\exists y (G(y) \land \lnot F(y))$.

Comment

This is the formal statement of $∃$-Elimination, form Richard Kaye, The Mathematics of Logic (2007), page 122 :

(∃-Elimination) To show $Σ \cup \{ ∃zσ(z) \} \vdash θ$ it suffices to show $Σ \cup \{ σ(b) \} \vdash θ$, provided the substitution is valid and the variable $b$ is a new variable not already free in some formula in $Σ$ nor in $θ$.

An instance of $∃$-Elimination looks like the following :

(1) $∃z \sigma(z)$

(2) Let $b$ satisfy $\sigma(b)$

...

(3) $\theta$

(4) $\theta$ --- by $∃$-Elimination.