= Solution
The <thinning rule>, or <weakening>, is
$$
\boxed{\frac{\Gamma\vdash\alpha\qquad\Gamma\subseteq\Delta}{\Delta\vdash\alpha}.}
$$
It expresses that extra unused assumptions do not destroy a proof. In the context-sensitive predicate-calculus presentation it also allows a theorem first proved with a fresh <universal generalization rule>[generalization] variable to be used later in a context containing that variable free. Simply replaying the same <universal generalization rule>[generalization] under the larger context could violate its side condition. For instance a proof of $\forall x(x=x)$ from the empty context may generalize on $x$; it should remain available when an unused assumption $P(x)$ is added, even though that last <universal generalization rule>[generalization] could not be replayed with $P(x)$ open.
In propositional calculus the axiom schemes and <modus ponens rule>[modus ponens] have no analogous free-variable restriction. An induction on the original proof simply reuses each axiom, assumption and modus-ponens step under the enlarged assumptions, so <weakening> is admissible and need not be postulated separately. <Context-sensitive Hilbert weakening> concerns this proof presentation: systems already tracking only the assumptions on which each line depends can build admissible <weakening> into their treatment of predicate-calculus <universal generalization rule>[generalization] as well.
Back to article page
