Meta-introduction for implication in Natural Deduction for intuitionistic Propositional Logic

Question

I am going through a paper entitled A Tutorial on the Curry-Howard Correspondence by Darryl McAdams.

The author defines a ternary notation as follow to easily manipulate proof trees (page 6 - line 4):

$\bigstar_{0} \vdash \bigstar_{1} : \bigstar_{2}$

which can be read: "assuming any of the hypotheses in $\bigstar_{0}$, the tree $\bigstar_{1}$ is a proof that $\bigstar_{2}$ holds”.

Following this, it introduces meta-rules of inference like this one:

I do not understand why the hypothesis that $\implies I$ is discharging, namely "a", is not declared as follow:

$\Gamma, a: A \vdash \implies I_{\mathcal{a}}(\mathcal(B)):(A\implies B)$

Why do we need to declare "$\mathcal{a}$" in the upper part of the meta-proof tree but not in its lower part? What is the "scope" of "$\mathcal{a}$"?

Answer 1

The symbolism is only a way to "trace" the assumptions to be discharged; the assumption is $A$ and $a$ is a sort of "pointer" to the occurrence of the assumption discharged by the rule. It is not another assumptions.

See page 6 :

$\Gamma$ is any collection of hypothesis that includes a hypothesis of $A$ named $a$ ...

Compare with : Ian Chiswell & Wilfrid Hodges, Mathematical Logic (2007), page 16, for the Natural Deduction $\to$-introduction rule, an page 20 for a way to "trace" assumptions in a derivation.