# Sequent calculus and natural deduction derivation

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? • For your EDIT : you are reding it bottom-up; thus the rule is$\exists$-r and the term$t$used can be arbitrary : I've chosen$y$. 2nd to 3rd line : you are right, it's a typo; must be$\exists y$both time. Nov 15, 2015 at 19:56 • @MauroALLEGRANZA Okay, not it makes sense :) Thanks for the correction. And regarding the natural deduction part, I spent some time on it, and even tried to make a tree like view of it, but I just couldn't follow it like that, I don't at all see what's going on. Can you someone show me the tree like natural deduction derivation? If it is easier for you, even an image of a handwritten natural deduction derivation is okay. – user72151 Nov 15, 2015 at 21:17 ## 2 Answers 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 : 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)}}$$ • I thought that the sequent calculus derivation would be pretty straightforward like Graham Kemp that has provided. Meaning we do the$(\exists l)$rule, and we continue reaching$A(t)\mid^t_x \vdash A(t)\mid^t_x$. I thought that things would get pretty complicated for the natural deduction rule. But, seems like I was wrong. xD – user72151 Nov 14, 2015 at 20:14 • @portal - the formula is valid and the calculus is complete; thus, the formula must be provable. Nov 14, 2015 at 21:45 • Firstly, I really didn't understand the natural deduction derivation, I cannot follow it, unless it is in a tree structure. Second, in the sequent calculus derivation, you said below in Graham Kemp's answer, that we cannot do something like this$\exists y\;A(y)\to A(t)\big)\mid^t_x$, but in the third line (I always start from below), you have$\vdash \exists x \big( \exists y A(y) \to A(x) \big), \exists y A(y) \to A(x)$, where the$A(x)$at the end appear free. Can you show me how the natural deduction derivation will look like in a tree? I tried to convert ti somehow but couldn't manage. – user72151 Nov 15, 2015 at 15:58 • I also wrote an edit with a few more questions. – user72151 Nov 15, 2015 at 19:15 • @portal - I've suggested a derivation that seems right to me, but of course I'm wrong. Regarding the "double" formula, we have that$∃x(∃yA(y)→A(x))$is valid while$∃yA(y)→A(x)$is not. Thus, we cannot have a correct derivation ending with$\vdash ∃yA(y)→A(x)$. The semantics for sequent calculus "reads"$\Gamma \vdash \Delta$as a conjunction on the LHS and a disjunction on the RHS: Thus$⊢∃x(∃yA(y)→A(x)),∃yA(y)→A(x)$is$⊢∃x(∃yA(y)→A(x)) \lor (∃yA(y)→A(x))$and this is not invalid. Nov 15, 2015 at 19:24 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)