From "Type Theory and Formal Proof" by Rob Nederpelt and Herman Geuvers:

Definition 2.4.2

(1) A statement is of the form $M : \alpha$, where $M \in \Lambda_{\mathbb{T}}$ and $\sigma \in \mathbb{T}$. In such a statement, $M$ is called the subject and $\alpha$ the type.

(2) A declaration is a statement with a variable as subject.

(3) A context is a list of declarations with different subjects.

Definition 2.4.5 (Derivation rules for $\lambda \to$)

(var) $\Gamma \vdash x : \alpha$ if $x : \alpha \in \Gamma$

(appl) $\Gamma \vdash M : \alpha \to \tau \quad \Gamma \vdash N : \alpha \implies \Gamma \vdash M N : \tau$

(abst) $\Gamma, x : \alpha \vdash M : \tau \implies \Gamma \vdash \lambda x : \alpha . M : \alpha \to \tau$

Definition 2.10.1

(2) Context $\Gamma'$ is a subcontext of context $\Gamma$, or $\Gamma' \subseteq \Gamma$, if all declarations occurring in $\Gamma'$ also occur in $\Gamma$, in the same order.

Lemma 2.10.5

(1) (Thinning) Let $\Gamma'$ and $\Gamma''$ be contexts such that $\Gamma' \subseteq \Gamma''$. If $\Gamma' \vdash M : \alpha$, then also $\Gamma'' \vdash M : \alpha$.

Note: I replaced the horizontal bar between the premisses and conclusion in the derivation rules with $\implies$ since I could not get the bar to typeset as intended.

Suppose I assign the following in Lemma 2.10.5:

$\Gamma' = y : B$

$\Gamma'' = x : C, y : B$

$M = \lambda x : A . y$

$\alpha = A \to B$


$\Gamma' \vdash M : \alpha = y : B \vdash \lambda x : A . y : A \to B$

$\Gamma'' \vdash M : \alpha = x : C, y : B \vdash \lambda x : A . y : A \to B$.

For a derivation of the first I have:

(i) $y : B, x : A \vdash y : B$ (var)

(ii) $y : B \vdash \lambda x : A . y : A \to B$ (abst on i)

I am unable to find a derivation for the second as the lemma implies. Is there a derivation, or am I missing something else?


This may just be a consequence of Convention 1.7.2 From now on, we identify α-convertible λ-terms.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.