Natural deduction in quantification logic Can someone please help me on how to answer this using natural deduction?
$$\begin{array}{c}
(\exists x,\ F\ x) \supset (\exists x,\ (G\ x \land H\ x)) \\
(\exists x,\ (H\ x\lor K\ x)) \supset (\forall x,\ L\ x) \\
\hline
\forall x,\ F\ x \supset L\ x
\end{array}$$
 A: You want to prove $\forall x,\ (F\ x \supset L\ x)$, 
with premises 1 and 2.
By deduction theorem, you just need to prove $L\ x$ from premises 1, 2, $x$, $F\ x$.
By $\exists$ introduction, and premises $x$, $F\ x$, you can prove $\exists x,\ F\ x$.
Thus, by $\supset$ elimination, and premises 1 and $\exists x,\ F\ x$, you can prove $\exists x,\ G\ x \land H\ x$, then extract the witness $y$.
Now, your premises are 1, 2, $\exists x,\ F\ x$, $y$, $G\ y$, $H\ y$.
By $\lor$ introduction, and premise $H\ y$, you have $H\ y \lor K\ y$, which can be changed by $\exists$ introduction as $\exists y,\ H\ y \lor K\ y$.
By $\supset$ elimination, you can thus prove $\forall x,\ L\ x$, and in particular $L\ x$ for your particular x.
A: I'll go through this proof step by step : )
The way I like to do Natural Deduction proofs is by building a tree-like structure (see Halbach's 'The Logic Manual' if you're unfamiliar). 
Line 1: ∀Intro. So now we have (Fa -> La).
Line 2: ->Intro. So now we have La. 
Line 3: ∃Elim. So we have ∃x(Gx^Hx) and La on the same line. 
Let's focus on proving ∃x(Gx^Hx) first. 
Line 4: ->Elim. We have ∃xFx -> ∃x(Gx^Hx) and ∃xFx on the same line. 
∃xFx -> ∃x(Gx^Hx) is a premise, but we need to prove ∃xFx. 
Line 5: ∃Intro. So we have Fa. Fa can be discharged at line 2. 
Now to prove La. 
Line 6: ∀Elim. So now we have ∀xLx.
Line 7: ->Elim. We have ∃x(Hx v Kx) -> ∀xLx and ∃x(Hx v Kx) on one line.
Now ∃x(Hx v Kx) -> ∀xLx is a premise but we need to prove ∃x(Hx v Kx).
Line 8: ∃Intro. So now we have (Ha v Ka).
Line 9: VIntro. So now we have Ha.
Line 10: ^Elim. So now we have (Ga ^ HA). This can be discharged at Line 3. 
The proof is now complete. Hope that's helpful!
