Implication Introduction in reverse way

Question

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?

Answer 1

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.