Natural deduction proof for $\exists x(\exists y A(y) \rightarrow A(x))$

Question

I spent a long time trying to find a natural deduction derivation for the formula $\exists x(\exists y A(y) \rightarrow A(x))$, but I always got stuck at some point with free variables in the leaves. Could someone please help me or give me some hints to find a proof.

Thanks.

Answer 1

You can derive it this way:

1. $\exists y\,A(y) \qquad\qquad\textsf{assumption}$
2. $A(a) \qquad\quad\qquad\textsf{$\exists$ new parameter introduction}\text{ ($a$)}$
3. $\exists y\,A(y) \to A(a) \quad\quad\textsf{discharge 1.}$
4. $\exists x\,(\exists y\,A(y) \to A(x)) \quad\textsf{$\exists$ introduction}$

Answer 2

If you prefer the tree style notation this is a valid proof:

$$\dfrac{\dfrac{\lower{1.5ex}{[\exists y~A(y)]^1}~~\dfrac{[A(s)]^2}{A(s)}{}}{\dfrac{A(s)}{\exists y~A(y)~\to~A(s)}{(\to i,1)}}{(\exists e,1)}}{\exists x~(\exists y~A(y)~\to~A(x))}{(\exists i)}$$