Could anyone give an intuitive (not intutionistic) explanation of the correspondence of left introduction and elimination of implication in Sequent Calculus (SC) and Natural Deduction (ND) respectively? I know they should by the symmetry of SC but I don't see how they correspond to each other. More generally, I don't understand how left introduction of a connective in SC renders exactly the elimination of it in ND intuitively.
About the correspondence of left introduction and elimination of implication in Sequent Calculus and in Natural Deduction resp.
lo.logic;proof theory;sequent calculus;natural deduction
In computational terms, a sequent calculus term is a sequentialization of a lambda term. That is, viewed as a type system, sequent calculus can be seen as giving an evaluation order of a lambda-term.So, suppose $\Gamma \vdash e_1 : A \to B$, and $\Gamma \vdash e_2 : A$. In natural deduction, the term for implication elimination is $\Gamma \vdash e_1\;e_2 : B$ -- that is, application. However, note that this doesn't tell us whether to evaluate $e_1$ first or $e_2$ first. In sequent calculus, a corresponding proof term assignment must look like $$\mathsf{let}\; f = e_1 \;\mathsf{in}\;\mathsf{let}\;v = e_2\;\mathsf{in}\;\mathsf{let}\; x = f\;v \;\mathsf{in}\;x$$ or else it must look like $$\mathsf{let}\; v = e_2\;\mathsf{in}\;\mathsf{let}\;f = e_1 \;\mathsf{in}\;\mathsf{let}\; x = f\;v \;\mathsf{in}\;x$$ Here, the let-form is the proof term corresponding to the use of the cut-rule, and since all of the left rules act only on hypotheses/variables, this forces us to bind all intermediate results to variables. This requirement ensures that we are forced to explicitly say which of $e_1$ or $e_2$ we reduce and bind to a variable first. For purely functional languages, this explicitness doesn't matter, but as you add effects it becomes easier to work with sequent calculi. This is why things like calculi of control effects/classical logic are typically presented sequent calculus. 