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

<p>$A \wedge B$<br>
$---$<br>
$A$
</p>

<p>$A \wedge B$<br>
$---$<br>
$B$
</p>

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

<p>Similarly, in SC:</p>

<p>$\Gamma,A\vdash \Delta$<br>
$------$<br>
$\Gamma,A\wedge B \vdash \Delta$
</p>

<p>$\Gamma,B\vdash \Delta$<br>
$------$<br>
$\Gamma,A\wedge B \vdash \Delta$
</p>

<p>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$.</p>

<p>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.</p>

<p>Now, for implication, in ND we have:</p>

<p>$A \rightarrow B$  &nbsp; &nbsp; &nbsp;  $A$<br>
$------$<br>
$B$
</p>

<p>In SC:</p>

<p>$\Gamma \vdash A,\Delta$ &nbsp; &nbsp; &nbsp;   $\Sigma,B\vdash \Pi$<br>
$----------$<br>
$\Gamma,\Sigma, A\rightarrow B \vdash \Delta,\Pi$
</p>

<p>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:</p>

<p>$\Gamma \vdash A$ &nbsp; &nbsp; &nbsp;  $B\vdash \Pi$<br>
$-------$<br>
$\Gamma, A\rightarrow B \vdash \Pi$
</p>

<p>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.</p>

CC BY-SA 2.5
2010-12-17T17:59:43.873Z
Nice answer, but the question asks about implication, not conjunction.
Dave Clarke
CC BY-SA 2.5
2010-12-18T02:28:21.433Z
@Radu yea, but that makes them come out tiny. I think this way works well enough.
Mark Reitblatt
CC BY-SA 2.5
2010-12-17T17:51:04.213Z
2010-12-17T18:16:05.290Z
2010-12-17T18:16:05.290Z
Mark Reitblatt
<p>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.</p>

<p>So, suppose $\Gamma \vdash e_1 : A \to B$, and $\Gamma \vdash e_2 : A$. </p>

<p>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. </p>

<p>In sequent calculus, a corresponding proof term assignment must look like </p>

<p>$$\mathsf{let}\; f = e_1 \;\mathsf{in}\;\mathsf{let}\;v = e_2\;\mathsf{in}\;\mathsf{let}\; x = f\;v \;\mathsf{in}\;x$$
</p>

<p>or else it must look like </p>

<p>$$\mathsf{let}\; v = e_2\;\mathsf{in}\;\mathsf{let}\;f = e_1 \;\mathsf{in}\;\mathsf{let}\; x = f\;v \;\mathsf{in}\;x$$
</p>

<p>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. </p>

<p>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. </p>

CC BY-SA 2.5
2010-12-18T12:37:05.680Z
Neel, thanks also for this interesting interpretation from the computation point of view.
day
CC BY-SA 3.0
2013-10-22T22:01:11.733Z
Neel, can you give any papers or book chapters where one can find more details?
zpavlinovic
CC BY-SA 2.5
2010-12-18T03:22:49.970Z
2010-12-18T03:22:49.970Z
Neel Krishnaswami
<p>Could anyone give an <strong>intuitive</strong> (<em>not</em> intutionistic) explanation of the correspondence of left introduction and elimination of implication in <a href="http://en.wikipedia.org/wiki/Sequent_calculus" rel="nofollow">Sequent Calculus</a> (SC) and <a href="http://en.wikipedia.org/wiki/Natural_deduction" rel="nofollow">Natural Deduction</a> (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.</p>

<lo.logic><proof-theory><sequent-calculus><natural-deduction>
About the correspondence of left introduction and elimination of implication in Sequent Calculus and in Natural Deduction resp.
day
# About the correspondence of left introduction and elimination of implication in Sequent Calculus and in Natural Deduction resp.

(Asked by: username_0 on 2010-12-17)

Could anyone give an **intuitive** (*not* intutionistic) explanation of the correspondence of left introduction and elimination of implication in [Sequent Calculus](http://en.wikipedia.org/wiki/Sequent_calculus) (SC) and [Natural Deduction](http://en.wikipedia.org/wiki/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.

**Tags:** lo.logic, proof-theory, sequent-calculus, natural-deduction


---

## 2 answers

### Answer by username_3 on 2010-12-18. Score: 9 | Accepted answer

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.

> **Comments:**
> **username_0**: Neel, thanks also for this interesting interpretation from the computation point of view.  
> **username_4**: Neel, can you give any papers or book chapters where one can find more details?  

---

### Answer by username_1 on 2010-12-17. Score: 8

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.

> **Comments:**
> **username_2**: Nice answer, but the question asks about implication, not conjunction.  
> **username_1**: @Radu yea, but that makes them come out tiny. I think this way works well enough.  

---

