# Implication Introduction in reverse way

In Gentzen system, there is an inference rule such that one can deduce $$\Gamma \to \Delta, \mathfrak{A} \supset \mathfrak{B}$$ from $$\Gamma, \mathfrak{A} \to \Delta, \mathfrak{B}$$.

Can we, in reverse way, deduce $$\Gamma, \mathfrak{A} \to \Delta, \mathfrak{B}$$ from $$\Gamma \to \Delta, \mathfrak{A} \supset \mathfrak{B}$$? More precisely,

1. In Gentzen sequent calculus, is there an inference rule of the form below? \begin{align} \frac{\Gamma \to \Delta, \mathfrak{A} \supset \mathfrak{B}}{\Gamma, \mathfrak{A} \to \Delta, \mathfrak{B}}* \end{align}

2. In Gentzen sequent calculus, is there a derivation of $$\Gamma,𝔄 \to \Delta,𝔅$$ from the assumption $$\Gamma \to \Delta,𝔄 \supset 𝔅$$? In other words, is the rule ($$*$$) derivable in Genztzen sequent calculus?

Mauro Allegranza's reply correctly answers Point 1 of the question. But the answer to Point 2 of the question is positive. Indeed, the rule $$\supset$$-right is reversible, which means that the inference rule \begin{align} \frac{\Gamma \to \Delta, \mathfrak{A} \supset \mathfrak{B}}{\Gamma, \mathfrak{A} \to \Delta, \mathfrak{B}}* \end{align} (i.e. the bottom-up version of the rule $$\supset$$-right) is derivable in Gentzen sequent calculus: ($$*$$) is not an inference rule of original Gentzen sequent calculus but it can be "simulated" in Gentzen sequent calculus, i.e. there exists a derivation of $$\Gamma, \mathfrak{A} \to \Delta, \mathfrak{B}$$ from the assumption $$\Gamma \to \Delta, \mathfrak{A} \supset \mathfrak{B}$$, for instance the following \begin{align}\tag{1} \dfrac{\Gamma \to \Delta, \mathfrak{A} \supset \mathfrak{B} \qquad \dfrac{\dfrac{}{\mathfrak{A} \to \mathfrak{A}}\text{ax} \qquad \dfrac{}{\mathfrak{B} \to \mathfrak{B}}\text{ax}}{\mathfrak{A},\mathfrak{A} \supset \mathfrak{B} \to \mathfrak{B}}\supset\!\!\text{-right} }{\Gamma, \mathfrak{A \to \Delta, \mathfrak{B}}}\text{cut} \end{align}

This entails that if the sequent $$\Gamma \to \Delta, \mathfrak{A} \supset \mathfrak{B}$$ is derivable, then $$\Gamma, \mathfrak{A} \to \Delta, \mathfrak{B}$$ is derivable: given a derivation $$\pi$$ of $$\Gamma \to \Delta, \mathfrak{A} \supset \mathfrak{B}$$, the composition of $$\pi$$ with the derivation $$(1)$$ yields a derivation of $$\Gamma, \mathfrak{A} \to \Delta, \mathfrak{B}$$.

No; in Sequent Calculus you do not "unpack" complex formulae but always build them up from their "components".

The rules for the conditional connective $\supset$ are:

\begin{align} {\cfrac{C, \Gamma \to \Delta, D}{\Gamma \to \Delta, C \supset D} \supset \text {-right}} \end{align}

\begin{align} {\cfrac{\Gamma \to \Delta, C \ \ \ \ \ \ \ D, \Pi \to \Lambda}{C \supset D, \Gamma, \Pi \to \Delta, \Lambda} \supset \text {-left}} \end{align}

An important feature of Sequent Calculus is that the rules are invertible, i.e. we can use them "bottom-up" in a proof-search procedure. In this case, what you are asking is nothing else than $\supset \text {-right}$ read bottom-up.

• Thanks! ... Sequent calculus always confuses me... – Bram28 Apr 12 '17 at 13:29
• I think the question in the OP has two possible interpretations. I made them more explicit in my edit. Of course, your answer is correct for question 1. But for question 2. the answer is positive, and I think this was the sense of the OP. I suggest to reopen the question. – Taroccoesbrocco Apr 1 '18 at 10:50