Weakening Rule

In logic and type theory, the weakening rule is a Structural Rule that lets you remove unused elements from the context.

For simply typed systems based off of Natural Deduction, weakening rules take the form of

Γ1,Γ2⊢e:BΓ1,x:A,Γ2⊢e:BprovessubscriptΓ1subscriptΓ2𝑒:𝐵:subscriptΓ1𝑥𝐴subscriptΓ2proves𝑒:𝐵\par\frac{\Gamma_{1},\Gamma_{2}\vdash e:B}{\Gamma_{1},x:A,\Gamma_{2}\vdash e:B}

For Sequent Calculi, we need both Left and Right weakening rules:

Γ1,Γ2⊢ΔΓ1,A,Γ2⊢ΔprovessubscriptΓ1subscriptΓ2ΔprovessubscriptΓ1𝐴subscriptΓ2Δ\displaystyle\frac{\Gamma_{1},\Gamma_{2}\vdash\Delta}{\Gamma_{1},A,\Gamma_{2}% \vdash\Delta}
Γ⊢Σ1,Σ2Γ⊢Σ1,A,Σ2provesΓsubscriptΣ1subscriptΣ2provesΓsubscriptΣ1𝐴subscriptΣ2\displaystyle\frac{\Gamma\vdash\Sigma_{1},\Sigma_{2}}{\Gamma\vdash\Sigma_{1},A% ,\Sigma_{2}}

A better presentation of weakening rules is to add Weakening Substitutions π : Γ , A → Γ : 𝜋 → Γ 𝐴 Γ \pi:\Gamma,A\to\Gamma and require that all your Judgements be stable under substitution. This is the version that scales well to dependent types, where we need the substitution for the rule to even make sense!

Γ⊢b:BΓ,a:A⊢b⁢[π]:B⁢[π]provesΓ𝑏:𝐵:Γ𝑎𝐴proves𝑏delimited-[]𝜋:𝐵delimited-[]𝜋\par\frac{\Gamma\vdash b:B}{\Gamma,a:A\vdash b[\pi]:B[\pi]}