conditional proof with different variable

Question

I don't know how to prove $(Ǝx~F(x)~→~Ǝx~G(x))$ with conditional proof from:

$(Ǝx~F(x) ~→~ ∀z~H(z))$

$H(a)~→~G(b)$

I have a problem with different variables here and conditional proof as well.

Answer 1

Hint: $\forall z~H(z) ~\vdash~ H(a)$ and $G(b)~\vdash~\exists z~G(z)$

• If the domain of discourse contains $a$ then $\forall z~H(z)$ entails $H(a)$ by universal elimination.

• If $G(b)$ then we have a witness to $\exists z~G(z)$ for existential introduction.

---

For the rest:

Assume $\exists x~F(x)$ then use $\to$elimination (modus ponens) and the above to reach the required consequent, and then use $\to$introduction to discharge the assumption.

---

$$\begin{align} & \begin{array}{|l|l:l|}\hline 1 & \forall x~F(x) ~\to~\forall z~H(z) & \textsf{Premise 1} \\ 2 & H(a)~\to~G(b) & \textsf{Premise 2} \\ \hdashline 3 & \quad \forall x~F(x) & \textsf{Assumption 1} \\ 4 & \quad \forall z~H(z) & 1,3,\to\textsf{elim (Modus Ponies)} \\ \hdashline 5 & \qquad H(a) & 4,\forall\textsf{instantiation to witness} \\ 6 & \qquad G(b) & 2,5,\to\textsf{elim (Modus Ponies)}\\ \hline 7 & \quad \exists x~G(x) & 6, \exists\textsf{generalisation from witness}\\ \hline 8 & \forall x~F(x)~\to~\exists x~G(x) & 3,7,\to\textsf{intro discharges assumption 1}\\ \hline \end{array} \\[1ex] & \forall x~F(x) ~\to~\forall z~H(z) ~,~H(a)~\to~G(b)~~\vdash~~\forall x~F(x)~\to~\exists x~G(x) \\[1ex] \Box \end{align}$$