What is the point of the Thinning Rule? I am studying predicate calculus on some lecture notes on my own. I have a question concerning a strange rule of inference called the Thinning Rule which is stated from the writer as the third rule of inference for the the formal system K$(L)$ (after Modus Ponens and the Generalisation Rule):
TR) $ $ if $\Gamma \vdash \phi$ and $\Gamma \subset \Delta$, then $\Delta \vdash \phi$.
Well, it seems to me that TR is not necessary at all since it is easily proven from the very definition of formal proof (without TR, of course). I am not able to see what is the point here.
The Notes are here http://www.maths.ox.ac.uk/system/files/coursematerial/2011/2369/4/logic.pdf (page 14-15)

After a lot of research here and there I think I have found the correct answer thanks to Propositional and Predicate Calculus by Derek Goldrei. So I will try to answer my own question.
The fact is that when we are dealing with Predicate Calculus we have the following Generalization Rule:
GR) If $x_i$ is not free in any formula in $\Gamma$, then from $\Gamma \vdash \phi$ infer $\Gamma \vdash \forall x_i \phi$.
So we easily see that the Thinning Rule 
TR) $ $ If $\Gamma \vdash \phi$ and $\Gamma \subset \Delta$, then $\Delta \vdash \phi$.
is a metatheorem of the Propositional Calculus (where no quantifications and so no Generalization Rule occur) but it is not (in general) true for the Predicative Calculus.
As a matter of fact it could happen that $x_i$ has a free occurrence in a formula $\phi$ and $\phi \in \Gamma$ but $\phi \notin \Delta$ with $\Gamma \subset \Delta$. 
In such a case (without TR) if we have found that $\Gamma \vdash \forall x_i \phi$ from $\Gamma \vdash \phi$ we cannot say that $\Delta \vdash \forall x_i \phi$ because we cannot longer apply GR. 
This is the reason for the Thinning Rule.
