Weakening lemma
Weakening is the property of a hypothetical judgment that if Γ ⊦ J, then Γ, A ⊦ J. That is, if a judgment holds in a context Γ, then it holds in Γ extended with additional hypotheses. Weakening holds for most logics, but its absence is central to the formulation of substructural logics such as linear logic.
Often, we represent an an object-language hypothetical judgement by using LF binding to model hypotheses. When a judgement is represented in such a fashion, weakening comes “for free” from the LF representation. In particular, we may weaken a derivation by wrapping LF lambdas around it.
For example, consider the following simply typed λ-calculus:
%% Syntax%sort tp %.%term tp/unit tp %.%term tp/arrow %pi tp %-> tp %-> tp %.%sort exp %.%term exp/unit exp %.%term exp/lam %pi tp %-> (%pi exp %-> exp) %-> exp %.%term exp/app %pi exp %-> exp %-> exp %.%% Typing%sort of {_ exp} {_ tp} %.%term of/unit of exp/unit tp/unit %.%term of/lam %pi (of (exp/lam T E) (tp/arrow T T')) %<- ({x exp} %pi (of x T) %-> (of (E x) T')) %.%term of/app %pi (of (exp/app E1 E2) T') %<- (of E2 T) %<- (of E1 (tp/arrow T T')) %.Object-language typing is a hypothetical judgement; we represent it using LF variables to model hypotheses (see Representing the judgements of the STLC for more discussion of this representation).
We can prove weakening for this hypothetical judgement as a metatheorem:
(options removed from twelftag: check=“true”)
%sort wkn {T' tp} {_ of E T} {_ {x} %pi (of x T') %-> (of E T)} %.%mode wkn %in %in %out %.%term _ wkn T' D1 ([x] [dx of x T'] D1) %.%block of-block [T] {x exp} {dx of x T}%.%worlds (of-block) (wkn _ _ _) %.%total {} (wkn _ _ _) %.The proof is direct: given any derivation D1, we can wrap LF lambdas around it to create a derivation under the necessary hypotheses. The fact that this works corresponds to the fact that weakening is admissible for LF, which is why we say that the object language inherits the hypothetical structure of the meta-language.
Although we proved weakening as a metatheorem here for illustrative purposes, in practice it is unnecessary to write such proofs. Uses of weakening can be “inlined” by simply introducing LF lambdas when necessary.