3
$\begingroup$

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)

  • 0
    @user35549: exactly. Once it is out in the open that $\vdash$ might be inductively defined, rather than just meaning "there is a proof", the role of the "thinning rule" becomes much more clear. Peter Smith has commented in more detail in his answer.2012-09-17

3 Answers 3

8

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.

  • 4
    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 :-)2012-09-15
1

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.

  • 3
    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$.)2012-09-17
1

Following your own answer, we can use Derek Goldrei, Propositional and Predicate Calculus A Model of Argument (2005) for the right explanation.

He states a "standard" Hilbert-style propositional calculus; see page 87 for axioms, inference rule (only one : modus ponens) and the "basic" definition of the derivability property :

$\Gamma \vdash \varphi$ as a shorthand for ‘there is a derivation of $\varphi$ from $\Gamma$’.

Recall that :

Let $\Gamma$ be a set (possibly empty) of formulas and let $\varphi$ be a formula. A derivation of $\Gamma \vdash \varphi$ within $S$ is a finite sequence of formulas $φ_1, φ_2, φ_3, . . . , φ_n$, where the final formula $φ_n$ in the sequence is the formula $\varphi$ and the inclusion of each formula $φ_i$ can be explained in one of the following ways:

(i) $φ_i \in \Gamma$; [...]

Then see page 89 :

Theorem 3.1 (the thinning rule) : (ii) Suppose that there is a derivation of $\Gamma \vdash \varphi$ and that $\Delta$ is a set of formulas with $\Gamma ⊆ \Delta$. Then there is also a derivation of $\Delta \vdash \varphi$.

See the important note in the same page :

Theorem 3.1 is a theorem about a formal proof system, rather than a formal theorem of it. To help distinguish between these two uses of the word ’theorem’, a result about a formal system is often called a metatheorem.

Thus, as per Peter's comment, in an Hilbert-style presentation of propositional logic (like Goldrei's one) it is more correct to state the thinning rule as a meta-theore; ths means that it "works" ate the "meta-level" stating a property of the derivability relation and not at the level of the calculus (where modus ponens "works").

You are right in pointing at a difference between Goldrei's predicate calculus abd the propositional one. Consider the definition of derivation with the new generalization inference rule [page 221] :

(iv) $φ_i$ is of the form $∀xφ_j$, where $φ_j$ is a previous formula in the sequence, i.e. where $j < i$, and the quantified variable $x$ does not appear free in any formula in the set $\Gamma$.

In addition, if we have a derivation $\Gamma_0 \vdash φ$ obeying the conditions (i) to (iv) above for some subset $\Gamma_0$ of $\Gamma$, we shall also declare that $\Gamma \vdash φ$.

Thanks to this, if we have a derivation of $\Gamma \vdash φ$, this means that there is a derivation following conditions (i) to (iv) of $\Gamma_0 \vdash φ$ for some subset $\Gamma_0$ of $Γ$.

This is the thinning rule for the system. For propositional calculus this was a metatheorem about the system, but for predicate calculus it is built into the system.

The reason is explained in page 223, commenting the proof of $∀xφ(x) \vdash ∀yφ(y)$, for any formula $φ(x)$ in which $x$ appears as a free variable and for any variable $y$ which doesn’t appear in $φ(x)$.

Let’s use this derivation as an example to explain why we have built the thinning rule into the definition of $\Gamma \vdash φ$. If $x$ appears as a free variable in $φ(x)$ and $y$ doesn’t appear in $φ(x)$, then we have $∀xφ(x) \vDash ∀yφ(y)$.

This will follow from the soundness theorem for the system, but it is also easily verified directly from the definition of logical consequence. It follows straightforwardly from the properties of logical consequence that $\Delta, ∀xφ(x) \vDash ∀yφ(y)$ for any set of formulas $\Delta$ – we might say that the thinning rule applies to logical consequence – and it would then be desirable, given that we want a completeness theorem for the system, that $\Delta, ∀xφ(x) \vdash ∀yφ(y)$.

Without the thinning rule for the formal system, we would run into trouble if the set $\Delta$ contained any formulas involving $y$ as a free variable, for instance just the formula $φ(y)$. Our derivation of $∀xφ(x) \vdash ∀yφ(y)$ wouldn’t give a derivation of $φ(y), ∀xφ(x) \vdash ∀yφ(y)$ because the use of Gen on [one of the line of the derivation] would then quantify a variable appearing free in one of the assumptions, albeit an assumption not exploited anywhere in the derivation! But thanks to the thinning rule, we can say that $φ(y), ∀xφ(x) \vdash ∀yφ(y)$, because there is a derivation of $∀yφ(y)$ using a subset of the set of assumptions.