proof in sequent calculus LK

Question

I was reading a book that uses sequent calculus (and calls than Natural deduction ) and that mentions as rules

$$\frac{X,A\vdash B}{X\vdash A\to B}$$

and

$$ \frac{\begin{align}X &\vdash A\to B\\ Y& \vdash A\end{align}}{X,Y\vdash B} $$

I wanted to rewrite proof from this book to an original sequent calculus proof in the original sequent calculus (Gentzens LK system)
http://en.wikipedia.org/wiki/Sequent_calculus
http://gdz.sub.uni-goettingen.de/dms/resolveppn/?PPN=GDZPPN002375508

the rule $\to I$ above is in Gentzen's system FES or in modern language $\to R$

but the rule $\to E$ does not exist

How to derive $\to E$ in LK?

Answer 1

One method could be to use cut. (Forgive me, as far as I know, mathSE doesn't have a good way to type out sequent proof trees, so I'll just have to describe the tree.)

Suppose in your proof, you've derived both $X \vdash A \rightarrow B$ and $Y \vdash A$. Then using $\wedge R$ (and commutativity), you can derive $X, Y \vdash A \wedge (A \rightarrow B)$. Now, in a separate tree, start with the identities $A \vdash A$ and $B \vdash B$. Then, using $\rightarrow L$ (where $\Sigma$ and $\Delta$ are empty), we get $A, A \rightarrow B \vdash B$. By $\wedge L$ and contraction, you can then derive $A \wedge (A \rightarrow B) \vdash B$ (to do this, use $\wedge L_1$ to get $A \wedge (A \rightarrow B), A \rightarrow B \vdash B$, and then $\wedge L_2$ to get $A \wedge (A \rightarrow B), A \wedge (A \rightarrow B) \vdash B$; then use contraction). Finally, using cut on these two trees (where again $\Sigma$ and $\Delta$ are empty), you get $X, Y \vdash B$.

Now of course, by Cut Elimination, one could get a proof without using cut, but this proof tree is relatively simple because of the use of cut. Commutativity is needed if you want the order to be $X, Y$, though I imagine this wasn't a main issue. Contraction was used, but if you have an intensional conjunction in your system (as logics which reject contraction sometimes do), then the proof can be easily modified. So this proof still holds in quite a few Gentzen systems apart from LK.

Answer 2

You can see Sara Negri & Jan von Plato, Structural Proof Theory (2001), Ch.8 : Back to Natural Deduction for a very useful discussion of the relation between :

derivability relation of single succedent sequent calculus, written $\Gamma \Rightarrow C$,

and

derivability relation of natural deduction, written $\Gamma \vdash C$.

Natural deduction rule $\rightarrow$-I :

$$\frac {\frac {[A]} B } {A \rightarrow B}$$

may be rewritten in "sequent form" as :

$$\frac {\Gamma \cup \{ A \} \vdash B } {\Gamma \vdash A \rightarrow B}$$

With this form, the comparison with sequent calculus rule $\rightarrow$-right is easy :

$$\frac {A, \Gamma \Rightarrow \Delta, B } {\Gamma \Rightarrow \Delta, A \rightarrow B}$$

With natural deduction rule $\rightarrow$-E, things are a little bit more complicated.

The "standard" rule :

$$ \frac{A \rightarrow B \quad \quad A}{B}$$

may be rewritten in "sequent form" (as in your question) as :

$$ \frac{\Gamma \vdash A \rightarrow B \quad \quad \Delta \vdash A}{\Gamma,\Delta\vdash B}$$

Negri & von Plato consider the $\rightarrow$-E rule in a more general form :

$$ \frac{\vdash A \rightarrow B\ \quad \Gamma \vdash A \quad B \vdash C}{C}$$

Now, we can see the connection with the sequent calculus rule $\rightarrow$-left :

$$\frac {\Gamma_1 \Rightarrow A \quad \quad B, \Gamma_2 \Rightarrow C } {A \rightarrow B, \Gamma_1, \Gamma_2 \Rightarrow C }$$