Explanation of implication-introduction rule

I read in Proofs and Types by Girard et alii. the following excerpt that talks about the calculus of natural deduction:


Now a sentence at a leaf (of the deduction tree) can be dead, when it
no longer plays an active part in the proof. Dead sentences are
obtained by killing live ones. The typical example is the
$\implies$-introduction rule:


$$ \dfrac{\stackrel{[A]}{\stackrel{\vdots}{B}}}{A \implies B} $$


It must be understood thus: starting from a deduction of B, in which
we choose a certain number of occurrences of $A$ as hypotheses (the
number is arbitrary: 0,1,250,$\ldots$), we form a new deduction of
which the conclusion is $A \implies B$, but in which all these
occurrences of $A$ have been dicharged, ie. killed. There may be other
occurrences of $A$ which we have chosen not to discharge.


This rule illustrates very well the illusion of the tree-like
notation: it is of critical importance to know when a hypothesis was
discharged, and so it is essential to record this. But if we do this
in the exmaple above, this means we have to link the crossed A with
the line of the $\implies$I rule; but it is no longer a genuine tree
we are considering.

May I ask you for an explanation and example of this situation?

Every assumption that is introduced between brackets has to be discharged at some point for the proof to be complete. Otherwise, we could prove that $A$ is true for any given $A$ as follows.

[A]¹
───
 A

This proof is incorrect, we have not discharged the initial assumption. The following proof of $A\to A$ would be correct, as it discharges the assumption (and the implication introduction rule is necessary to do so!).

[A]¹
 ───
  A
───── (discharging ¹)
A → A

Now, let's compare two derivations of $A \to A \times A$ and $A \to A \to A \times A$. On the first one, we will discharge the two occurrences of $A$ at the same time (on the same deduction step). On the second one, we will discharge the two occurrences on two separate steps.

First proof

[A]¹   [A]²        
  ─────────   
    A × A        
───────────── (discharging ¹ and ²)
  A → A × A

Second proof

[A]¹    [A]²             
 ──────────          
   A × A             
───────────── (discharging ¹, note that ² is still alive!)   
  A → A × A        
──────────────── (discharging ²)
 A → A → A × A

Maybe looking at this from the perspective of the simply-typed lambda calculus is more illuminating. Instead of tracking superscripts, variable
names represent which assumptions are we choosing to discard at each point. Note the difference between the two proofs, and how the introduction rule of the implication corresponds to a lambda abstraction,
while the introduction rule of the conjunction corresponds to a pair type.

First proof

a : A   a : A        
   ─────────────     
   (a,a) : A × A        
 ────────────────────
 λa.(a,a) : A → A × A

Second proof

a : A   b : A             
     ─────────────          
     (a,b) : A × A             
   ────────────────────     
   λb.(a,b) : A → A × A        
 ───────────────────────────
 λa.λb.(a,b) : A → A → A × A

(I am using a lambda interpreter I wrote to generate these derivation trees. It may be useful for you if you are interested in the connection between propositional intuitionistic logic and lambda calculus.)

StackExchange Computer Science Q#95703, answer score: 5