Natural deduction and introduction of universal quantifier I have a hard time with quantification introduction and elimination ; for instance, if I want to prove
$$\forall x \quad (Px\rightarrow Px ) $$
I am tempted to do the following :
$$\underline{[Py]}_{\, I\rightarrow} \\\underline{\quad \ Py \rightarrow Py \quad}_{\,I \, \forall}
\\\forall x \  (Px\rightarrow Px )
 $$
But I am not convinced since $y$ is not non-free in $Py \rightarrow Py$ (or is it?)
What do I miss?
 A: Your derivation is perfectly valid. Indeed, in natural deduction, the rule
$$
\frac{A(y)}{\forall x \, A(x)}\forall_\text{intro}
$$
can be applied only when the variable $y$ does not occur free in the undischarged hypotheses of the derivation.
The undischarged hypotheses of  derivation are the leaves of the derivation trees (i.e. the formula occurrences that do not have any premise above them) that have not been discharged yet.
Now, your derivation before applying the rule $\forall_\text{intro}$ is
$$
\frac{[Py]^*}{Py \to Py}\to_\text{intro}^*
$$
where there are not undischarged hypotheses, because the hypothesis $Py$ has been discharged by the rule $\to_\text{intro}$ (the symbol ${}^*$ marks when the hypotheses has been discharged). Therefore, when you apply the rule $\forall_\text{intro}$, the condition "$y$ does occur free in the undischarged hypotheses of the derivation" is vacuously true, since there are no undischarged hypotheses in that moment.
Clearly, $y$ occurs free in $Py \to Py$. However, note that when you apply the rule $\forall_\text{intro}$, the formula occurrence  $Py \to Py$ is not an hypothesis in your derivation, because it has a premise above it, $[Py]$.
