Sequent calculus and natural deduction derivation

Question

Given the formula $\exists x(\exists yA(y) \rightarrow A(x))$ of classical logic. Provide a sequent calculus derivation and a natural deduction derivation of the formula.

I started to do something like this for the natural deduction, but then I got stuck: $$\dfrac{\dfrac{[\exists y\; A(y)] \quad, \quad A(t)}{A(t)}}{\dfrac{[\exists y\; A(y)] \rightarrow A(t)}{\exists x\;\big(\exists y\;A(y) \rightarrow A(x)\big)}}$$

I don't know how the natural derivation will continue, and I also I don't know how to sequent calculus derivation will look like. Sorry for the poor typesetting, but I don't see any easy way to write derivations in MathExchange, and I cannot follow any other method than tree style derivation. Any ideas?

EDIT:

$$\dfrac{\dfrac{A(y) \vdash A(y)}{\exists x A(x), A(y) \vdash A(y), A(x)}}{\dfrac{A(y) \vdash \exists y A(y) \to A(y), A(x)}{A(y) \vdash \exists x \big( \exists y A(y) \to A(x) \big), A(x)}}$$

I don't understand how from $\exists x(\exists y A(y) \rightarrow A(x))$ you have obtained $\exists y A(y) \rightarrow A(y)$. Clearly, you have removed $\exists$, but why the $x$ is changed to $y$? Also when you have gone from the second line to third line $\exists y A(y) \rightarrow A(y)$ has been transformed to $\exists x A(x)$, you clearly have done $(\rightarrow r)$, but why is $y$ changed to $x$? And at the end, how did you get rid of $\exists x A(x)$ and $A(x) on the other side completely?

Answer 1

Natural Deduction

It seems to me that we have to "complicate" a little bit the derivation, in order to avoid the "invalid" : $\exists y A(y) \to A(x)$.

1) $\exists y A(y)$ --- premise

2) $A(x)$ --- assumed from 1) for $\exists$-elim

3) $\exists x A(x)$ --- from 2) by $\exists$-intro, followed by $\exists$-elim with 1) and 2)

4) $\vdash \exists y A(y) \to \exists x A(x)$ --- from 1) and 3) by $\to$-intro.

Now we can use $\vdash \exists y A(y) \to \exists x A(x)$ in the second part of the derivation :

5) $\exists y A(y)$ --- assumed [a]

6) $\exists x A(x)$ --- from 4) and 5) by $\to$-elim

7) $A(x)$ --- assumed [b] for $\exists$-elim

8) $\exists y A(y) \to A(x)$ --- from 5) and 7) by $\to$-intro, discharging [a]

9) $\exists x (\exists y A(y) \to A(x))$ --- from 8) by $\exists$-intro

10) $\vdash \exists x (\exists y A(y) \to A(x))$ --- from 6) and 7)-9) by $\exists$-elim, discharging [b].

---

Sequent Calculus

For the sequent calculus rules, see :

• Gaisi Takeuti, Proof Theory (2nd ed - 1987)

The deceptively "simple" derivation :

$$\dfrac{\dfrac{A(x) \vdash A(x)}{\exists y \ A(y) \vdash A(x)}}{\dfrac{\vdash \exists y \ A(y) \rightarrow A(x)}{\vdash \exists x \ \big(\exists y \ A(y) \rightarrow A(x) \big)}}$$

is wrong, because in te second line we are violating the proviso of the $\exists$-l rule : the eigenvariable $x$ must not occur free in the lower sequent.

It seems to me that the way to fix it is the following :

$$\dfrac{\dfrac{A(y) \vdash A(y)}{\exists y A(y), A(y) \vdash A(y), A(x)}}{\dfrac{A(y) \vdash \exists y A(y) \to A(y), A(x)}{A(y) \vdash \exists x \big( \exists y A(y) \to A(x) \big), A(x)}}$$

First we need $\text{Weakining}$ on both sides, followed by $\to\text{-r}$ and $\exists\text{-r}$.

Now, we apply $\exists\text{-l}$, with the proviso satisfied, followed by $\to\text{-r}$ and $\exists\text{-r}$ again; finally, we need $\text{Contraction}$ :

$$\dfrac{\dfrac{\exists y A(y) \vdash \exists x \big( \exists y A(y) \to A(x) \big), A(x)}{\vdash \exists x \big( \exists y A(y) \to A(x) \big), \exists y A(y) \to A(x)}}{\dfrac{\vdash \exists x \big( \exists y A(y) \to A(x) \big), \exists x \big( \exists y A(y) \to A(x) \big)}{\vdash \exists x \big( \exists y A(y) \to A(x) \big)}}$$