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

Answer 2

Something is fishy here: how is a function supposed to exhibit $A(x)$ with a “known” $x$ from merely $\exists y A(y)$, where $y$ is “forgotten”? This seems very counter-intuitive. Since the problem description says “classical logic”, I reckon there is no intuitionistic/constructive proof of this theorem. Any attempt that doesn’t involve a classical axiom (law of excluded middle, double negation elimination, or equivalent) is bound to fail.

Here's my solution in sequent notation. It starts off with the law of excluded middle (XM):

$$\dfrac{ \dfrac{ }{ \vdash \exists z A(z) \lor \lnot \exists w A(w) }\mathrm{XM} \quad \dfrac{ }{ \exists z A(z) \vdash \cdots }(1) \quad \dfrac{ }{ \lnot \exists w A(w) \vdash \cdots }(2) }{ \vdash \exists x (\exists y A(y) \to A(x)) }\mathrm{E}_\lor$$

To keep the width of the proof sensible, I split the proof into separate parts (1) and (2), each responsible for handling one of the two possible cases that result from XM. To avoid confusion, I use distinct letters for different bound variables, but keep in mind that $\exists z A(z)$ and $\exists w A(w)$ are exactly the same thing.

Case (1), where $\exists z A(z)$ holds:

$$ \dfrac{ \dfrac{ }{ \exists z A(z) \vdash \exists u A(u) }\mathrm{Id} \quad \dfrac{ \dfrac{ \dfrac{ \dfrac{ }{ A(u) \vdash A(u) }\mathrm{Id} }{ A(u), \exists y A(y) \vdash A(u) }\mathrm{Wk} }{ A(u) \vdash \exists y A(y) \to A(u) }\mathrm{I}_\to }{ A(u) \vdash \exists x (\exists y A(y) \to A(x)) }\mathrm{I}_\exists }{ \exists z A(z) \vdash \exists x (\exists y A(y) \to A(x)) }\mathrm{E}_\exists $$

Case (2), where $\exists w A(w)$ does not hold:

$$ \dfrac{ \dfrac{ \dfrac{ }{ \lnot \exists w A(w) \vdash \lnot \exists v A(v) }\mathrm{Id} }{ \lnot \exists w A(w) \vdash \exists v A(v) \to \bot }\mathrm{E}_\lnot \quad \dfrac{ }{ \exists y A(y) \vdash \exists v A(v) }\mathrm{Id} }{ \dfrac{ \dfrac{ \dfrac{ \lnot \exists w A(w), \exists y A(y) \vdash \bot }{ \lnot \exists w A(w), \exists y A(y) \vdash A(x) }\mathrm{E}_\bot }{ \lnot \exists w A(w) \vdash \exists y A(y) \to A(x) }\mathrm{I}_\to }{ \lnot \exists w A(w) \vdash \exists x (\exists y A(y) \to A(x)) }\mathrm{I}_\exists }\mathrm{E}_\to $$

And just to prove that this derivation is not completely crazy, here's it is again, written as a Haskell program that correctly type checks:

{-# LANGUAGE GADTs #-}
module Foo where
import Data.Void (Void, absurd)

data Exists a where
  Exists :: a x -> Exists a

data Theorem a where
  Theorem :: (Exists a -> a x) -> Theorem a

excludedMiddle :: Either (p -> Void) p
excludedMiddle = error "you'll just have to trust me!"

theorem :: Theorem a
theorem =
  case excludedMiddle of
    Left notExists -> Theorem (\ exists -> absurd (notExists exists))
    Right (Exists evidence) -> Theorem (\ _ -> evidence)