1
$\begingroup$

this is what I've tried so farI have difficulties proving with natural deduction the following:

$$Ga\rightarrow\exists xFx \vdash \exists x(Ga\rightarrow Fx)$$

Thanks for the help!

$\endgroup$
2
  • $\begingroup$ I added a picture of what I've tried. I think somewhere i have to use the existential quantor elimination. I know how the rule works but i don't know how to apply it in this case. That's what I'm having problems with $\endgroup$
    – M-S-R
    Jun 28 at 9:54
  • $\begingroup$ I would suggest using LEM: $Ga \lor \lnot Ga$. $\endgroup$ Jun 30 at 7:20

1 Answer 1

1
$\begingroup$

The idea is to first isolate $\exists x Fx$ from the hypothesis $Ga \to \exists x Fx$ to get rid of the existential quantifier in $\exists xFx$, and then reintroduce the existential quantifier outside of $Ga \to Fx$. Formally, the derivation in natural deduction has the form below.

\begin{align} \dfrac{ \dfrac{ Ga \to \exists x Fx \qquad Ga }{ \exists xFx }\to_\text{elim} \qquad \dfrac{\dfrac{[Fx]^*}{Ga \to Fx}\to_\text{intro} }{ \exists x (Ga \to Fx)}\exists_\text{intro}}{\exists x (Ga \to Fx) } \exists_\text{elim}^* \end{align}

But there is a problem! We added an hypothesis $Ga$ which we have not discharged. Thus, the derivation above actually proves that $Ga \to \exists x Fx, \ Ga \vdash \exists x (Ga \to Fx)$.

The next step to answer your question is then to plug the derivation above into another derivation, so that we can discharge the further hypothesis $Ga$. The way to do that is quite technical, see below (the vertical dots stand for the derivation $Ga \to \exists x Fx, \ Ga \vdash \exists x (Ga \to Fx)$ above).

\begin{align} \small \dfrac{\dfrac{[\lnot\exists x (Ga \to Fx)]^\bullet \qquad \dfrac{\dfrac{\dfrac{\dfrac{[\lnot\exists x (Ga \to Fx)]^\bullet \qquad \genfrac{}{}{0pt}{0}{\genfrac{}{}{0pt}{0}{Ga \to \exists x Fx, \ [Ga]^\circ}{\vdots}}{\exists x (Ga \to Fx)}}{\bot}\lnot_\text{elim}}{Fx}\text{efq}}{Ga \to Fx}\to_\text{intro}^\circ }{\exists x (Ga \to Fx)}\exists_\text{intro}}{\bot}\lnot_\text{elim} }{\exists x (Ga \to Fx)}\text{raa}^\bullet \end{align}

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.