I am going through Troelstra and Schwictenberg's Basic Proof Theory, and I can understand most of the sequent calculus rules by finding some sort of parallel between the rule and a corresponding natural deduction rule, except the L$\to$ rule:
I have no idea what this is supposed to stand for: does this mean when you have a proof for A (be it from a set of formula $\Gamma$ or just an empty set), and something else ($\Delta$ in this case) that you can prove from B, you can 'add' A$\to$B to the LHS of the provability?
Is this a correct application of the rule? (Conclusion is at the top, so it's an inversed proof tree)
Also I understand that for G1$_i$ you can only have one formula on the RHS of the provability/sequent arrow, but again what is the G1$_i$ L$\to$ rule supposed to mean, and what is the difference between the G1$_i$ L$\to$ and G1$_c$ L$\to$?
Many thanks for any help offered!
Thinking in terms of natural deduction, consider the standard rule for $\mathord{\to}E$:
$$\frac{A\to{B}\quad A}{B}$$
The $L\mathord{\to}$ sequent rule says that whenever you have a derivation of the minor premiss $A$ from some assumptions $\Gamma$ ($\Gamma\Rightarrow{A}$) and a derivation of $\Delta$ from the same assumptions $\Gamma$ together with $B$ ($B,\Gamma\Rightarrow{\Delta}$), then you can construct a derivation of the same $\Delta$ from assumptions $\Gamma$ together with $A\to{B}$ ($A\to{B},\Gamma\Rightarrow{\Delta}$) by obtaining $B$ using $\mathord{\to}E$ from $A\to{B}$ and appending the derivation for the minor premiss $A$ from $\Gamma$. Like so:
$$\frac{A\to{B}\quad \Gamma\Rightarrow{A}}{B,\Gamma\Rightarrow\Delta}$$
or, more naturally,
$$\frac{\begin{array}{cc} & \Gamma\\ & \vdots\\ A\to{B} & A\end{array}}{\begin{array}{c}B\\ \vdots\\ \Delta\end{array}}$$
The $L\mathord{\to}$ sequent rule is perhaps best represented in natural deduction by the generalised elimination rule for implication $\mathord{\to}GE$ (see Structural Proof Theory by Negri & von Plato, §8.2):
$$\frac{\begin{array}{ccc} & & [B]\\ & & \vdots\\ A\to{B} & A & C\end{array}}{C}$$
Notice that the standard rule $\mathord{\to}E$ can be derived as a special case of $\mathord{\to}GE$ where $B=C$.
P.S. As far as I can tell, the application of the classical $G1_c$ $L\mathord{\to}$ sequent rule in your upside-down derivation is correct. Intuitionistically, it is not correct (notice that the first premiss of the $G1_i$ $L\mathord{\to}$ rule has a single formula on RHS of the sequent).