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

The following is a natural deduction proof of the formula $\exists x (\exists y A(y) \rightarrow A(x))$ $$ \dfrac { \dfrac { \dfrac { \dfrac { \dfrac { \dfrac {} { [\exists y A(y)]_2 } \dfrac { \dfrac { \dfrac { \dfrac{\dfrac{}{[A(b)]_3}}{\exists y A(y) \rightarrow A(b)} \rightarrow_i } { \exists x (\exists y A(y) \rightarrow A(x)) } \exists_i \dfrac{}{[\neg \exists x (\exists y \rightarrow A(x))]_1} } {\bot} \neg_e } { A(x) } \bot_e } { A(x) } \exists_{e,3} } { \exists y A(y) \rightarrow A(x) } \rightarrow_{i,2} } { \exists x (\exists y A(y) \rightarrow A(x)) } \dfrac{}{[\neg \exists x(\exists y A(y) \rightarrow A(x))]_1} } { \bot } \neg_e } { \exists x (\exists y A(y) \rightarrow A(x)) } \mathrm{RAA_1} $$ Since the formula $\exists x(\exists y A(y) \rightarrow A(x))$ is not valid in intuitionistic logic, it can not be proven in this natural deduction system without the rule RAA (or the rule DNE).

Answer 2

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 3

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)}$$