= Context-sensitive Hilbert weakening
{title2=$\Gamma\vdash\alpha,\ \Gamma\subseteq\Delta\ \Longrightarrow\ \Delta\vdash\alpha$}
= Thinning rule
{synonym}
Thinning enlarges the assumptions without changing a conclusion. In a predicate-calculus presentation with context-sensitive <universal generalization rule>[generalization], a <universal generalization rule>[generalization] valid before adding an unused assumption may not be replayable with that assumption open. An explicit <weakening> step nevertheless imports the already proved conclusion. In propositional calculus with only axiom schemes and <modus ponens rule>[modus ponens], <weakening> is admissible by replaying the proof. The need for a separately stated rule depends on how proof dependencies are represented.
Back to article page
