Proof of lemma on parameters in natural deduction I could not understand the proof of the Lemma on parameters on page 29 of this book (Natural Deduction) by Dag Prawitz. Why if all proper parameters in a derivation $\pi$ are pure, $\pi$ will satisfy 3 clauses as stated in the Lemma?
(On page 28 and 29, a pure parameter $a$ has the properties of (a) being the only proper parameter of an application $\alpha$ of $\forall I$ or $\exists E$, and  (b) all formula occurrences $B$s where $a$ occurs in $B$s are linked by $a$ to the premiss or discharged premiss of $\alpha$.)
Specifically,

*

*Why in a deduction $\pi$ whose proper parameters are pure, every proper parameter used by a quantifier rule $\alpha$ ($\forall I$ or $\exists E$) is a proper parameter of exactly one quantifier rule in the derivation? (Or put it differently, how the second property of a pure parameter $a$ is violated if it occurs twice in 2 different $\alpha$ ?)


*Why if a pure parameter $a$ is used by an application $\alpha$ of $\forall I$ or $\exists E$, then it occurs only in the part of the derivation above $\alpha$?
I tried to cook up a counter example as follows. Let $\pi$ be the derivation $\forall xPx$ $\rightarrow$ $Pa$ $\rightarrow$ $\forall xPx$ $\rightarrow$ $Pa\supset\forall xPx$. The bottom formula ($Pa\supset\forall xPx$) occurs below $Pa$ and is linked to $Pa$ by $a$ (by clause 4 of the definition of a connection between 2 formulas in page 28). So $a$ is still a pure parameter in $\pi$, but it occurs below the consequence of $\forall I$.
 A: The issue of the Lemma [page 29 of Dag Prawitz's Natural Deduction (1965)] regards the management of parameters in the quantifier rules.
A couple of rules has restrictions on the parameter used: the simple example is the restriction of the $(∀ \text I)$ rule where the parameter $a$ must not occur free in some open assumption [reason: we cannot "generalize" on the assumption $x=0$ to derive the incorrect $∀x(x=0)$].
The simplest way to fulfill the restrictions is that:

*

*every parameter used by a quantifier rule is used only once in the derivation, and


*if a parameter $a$ is used by an application $\alpha$ of a rule, then it occurs only in the part of the derivation above $\alpha$.
The Lemma describe a procedure that applied to a derivation $\Pi$ transforms it in a new derivation where all parameters are pure: in a nutshell, start from the uppermost application $\alpha$ of a quantifier rule with restriction and if the parameter $a$ of $\alpha$ is not pure, replace it with a fresh parameter $b$ that is not used in $\Pi$.

The gist of the "purification" procedure is that, in order to avoid potential clash between variables, we can always transform a derivation $\Pi$ in an "equivalent" one (same assumptions, same conclusion) $\Pi'$ such that:

*

*no variable occurs in $\Pi'$ both free and bound: and this is achieved in Prawitz's system using parameter (free) and variables (bound), and


*all parameters are distinct and different from the remaining parameters occurring in $\Pi'$: they are used only once.
