Weakening lemma

From The Twelf Project
(Redirected from Weakening)
Jump to: navigation, search

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

tp : type.
tp/unit  : tp.
tp/arrow : tp -> tp -> tp.
exp : type.
exp/unit : exp.
exp/lam  : tp -> (exp -> exp) -> exp.
exp/app  : exp -> exp -> exp.

%% Typing 

of : exp -> tp -> type.
of/unit : of exp/unit tp/unit.
of/lam  : of (exp/lam T E) (tp/arrow T T')
           <- ({x:exp} of x T
                -> of (E x) T').
of/app  : 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 in the tutorial Proving metatheorems with Twelf for more discussion of this representation).

We can prove weakening for this hypothetical judgement as a metatheorem:

wkn : {T':tp}
       of E T
       -> ({x} of x T' -> of E T)
       -> type.
%mode wkn +T' +D1 -D2.

- : wkn T' D1 ([x][dx:of x T'] D1).

%block of-block : some {T} block {x : exp} {dx : of x T}.
%worlds (of-block) (wkn _ _ _).
%total {} (wkn _ _ _).
See Twelf's output

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.

This article or section needs example of using weakening in another proof..

See also

Read more Twelf tutorials and other Twelf documentation.