# 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)

-
When I studied predicate calculus, such a rule was never mentioned... –  Ben Millwood Sep 14 '12 at 23:42
Maybe the thinning rule should be applied to itself... –  copper.hat Sep 14 '12 at 23:56
There is a difference between predicate calculus and propositional calculus, as hinted at by question 1 (e) here –  Henry Sep 14 '12 at 23:59
@Henry This is exactly the examination paper of the lectures notes I am reading. So what is the answer? –  user35549 Sep 15 '12 at 0:37
How would you demonstrate $\alpha, \beta \vdash \alpha$ without this rule? Certainly $\alpha \vdash \alpha$ can be demonstrated. –  Carl Mummert Sep 15 '12 at 1:23

Without seeing the original notes it is difficult to tell exactly what's going on. But on the face of it, the notes seem to be confused, if they present thinning as a rule on a par with modus ponens.

Thinning is usually explicitly there as a rule if we are developing a sequent calculus. But there we standardly distinguish the structural rules (the rules governing $\vdash$ that make it a consequence relation) from the logical rules governing specific logical operators like $\to$. Thinning is a structural rule (one of the rules that makes $\vdash$ a classical consequence relation), modus ponens is a logical rule (one of the rules governing the connective $\to$). Only confusion arises from muddling the two.

If we are presenting a natural deduction system, there will again be a distinction between structural rules and the introduction/elimination rules for the connectives. One of the standard background structural rules is (roughly) that an array counts as a proof from premisses $\Gamma$ to conclusion $\varphi$ if there is deduction tree all of whose undischarged topmost wffs are in $\Gamma$. That of course gives thinning trivially. Again it would be a confusion to just list the structural rule as if on a par with the modus ponens elimination rule.

-
The Notes are here at maths.ox.ac.uk/system/files/coursematerial/2011/2369/4/…. The thinning rule is presented on page 15. –  user35549 Sep 15 '12 at 13:29
Thanks for the link! Not good, I'm afraid. Note the use of MP, without comment, for two different rules -- an inference rule within a standard Hilbert-style axiomatic system (which doesn't have $\vdash$ as a symbol within it, though we might use that turnstile metalinguistically, from outside the system) and an inference rule within a small fragment of a sequent calculus where $\vdash$ is a symbol inside the calculus. I rest my case :-) –  Peter Smith Sep 15 '12 at 15:10

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.

-
Briefly 'cos of comment word limit. You are being led astray by those notes! They crash the gears, moving unannounced between talking abt a Hilbert system (inferences between propositions) and abt a sequent calculus (inferences between sequents). Your GR and TR are rules of a sequent calc: just fine!! But to develop a classical sequent calc for prop logic, you need TR there too. Consult any standard presentation. (And NB the sequent system which has $\vdash A$ for each of the stated axioms in the notes plus MP, GR and TR isn't complete. You can't even get $P \vdash P$.) –  Peter Smith Sep 17 '12 at 17:40