About the correspondence of left introduction and elimination of implication in Sequent Calculus and in Natural Deduction resp.

Question

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.

Answer 1

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.

Answer 2

Just to recap: in ND, the elimination of a connective tells us how to use it:

$A \wedge B$
$---$
$A$

$A \wedge B$
$---$
$B$

are the elim rules for conjunction. They say that we can use $A\wedge B$ to get $A$, or to get $B$.

Similarly, in SC:

$\Gamma,A\vdash \Delta$
$------$
$\Gamma,A\wedge B \vdash \Delta$

$\Gamma,B\vdash \Delta$
$------$
$\Gamma,A\wedge B \vdash \Delta$

What the SC rules are telling us is that if we "need" $A$ or $B$, then we can use $A\wedge B$ in place of $A$ or $B$.

In general, SC left introduction rules tell us "when" we can use a connective, and ND elimination rules tell us "how" to use a connective.

Now, for implication, in ND we have:

$A \rightarrow B$       $A$
$------$
$B$

In SC:

$\Gamma \vdash A,\Delta$       $\Sigma,B\vdash \Pi$
$----------$
$\Gamma,\Sigma, A\rightarrow B \vdash \Delta,\Pi$

Now, the first thing to do with the SC rule is to ignore the "crap". $\Delta$ and $\Sigma$ can be ignored for the purposes of intuition:

$\Gamma \vdash A$       $B\vdash \Pi$
$-------$
$\Gamma, A\rightarrow B \vdash \Pi$

What this says is that if we know how to use what we "have" ($\Gamma$) to prove $A$, and we know how to use $B$ to prove what we want $(\Pi)$, then we can use $A\rightarrow B$ to get what we want ($\Pi$). That is, once again the left introduction rule is telling us "when" we can use the connective.