<p>The two inference rules are different, because the first requires that x:T_1 is the only assumption, while the second allows side assumptions.  This can have subtle effects of the consequence relation for the type theory prevents the type theory from modelling weakening by having as the hypothesis rule:</p>

<p>$$
\frac{}{\Gamma, x:A \vdash x:A}
$$</p>

<p>In your English gloss, I would have <em>under the sole assumption</em>, to avoid confusion with the assumption-gobbling inference rule:</p>

<p>$$
\frac{\Gamma, x:T_1 \vdash t_2 : T_2}{\vdash \lambda x:T_1.t_2:T_1\to T_2}
$$</p>

CC BY-SA 3.0
2013-08-13T07:35:18.533Z
2013-08-13T07:35:18.533Z
Charles Stewart
<p>I am currently trying to read up on type theory and have some quick questions on terminology. </p>

<p>In the following rule,</p>

<p>$$
\frac{x:T_1 \vdash t_2 : T_2}{\vdash \lambda x:T_1.t_2:T_1\to T_2}
$$</p>

<p>How would you write that in English? Would the following be correct?</p>

<blockquote>
  <p><em>If we have established that under the assumption that $x$ has type $T_1$, $t_2$ has type $T_2$; then we can derive that under the empty set of assumptions, $\lambda x.t_2$ has type $T_1\to T_2$.</em></p>
</blockquote>

<p>Is this just a shorthand for the following?</p>

<p>$$
\frac{\Gamma,x:T_1 \vdash t_2 : T_2}{\Gamma\vdash \lambda x:T_1.t_2:T_1\to T_2}
$$</p>

<p>Would this be read as <em>If we have established that under the assumptions of the type environment $\Gamma$ and the binding $x:T_1$, that $t_2$ has type $T_2$; then [$\ldots$]</em>?</p>

<lo.logic><type-theory><terminology><type-systems>
Typing relations terminology – how do I read typing relations?
beta
# Typing relations terminology – how do I read typing relations?

(Asked by: username_0 on 2013-08-12)

I am currently trying to read up on type theory and have some quick questions on terminology.

In the following rule,

$$
\frac{x:T\_1 \vdash t\_2 : T\_2}{\vdash \lambda x:T\_1.t\_2:T\_1\to T\_2}
$$

How would you write that in English? Would the following be correct?

> *If we have established that under the assumption that $x$ has type $T\_1$, $t\_2$ has type $T\_2$; then we can derive that under the empty set of assumptions, $\lambda x.t\_2$ has type $T\_1\to T\_2$.*

Is this just a shorthand for the following?

$$
\frac{\Gamma,x:T\_1 \vdash t\_2 : T\_2}{\Gamma\vdash \lambda x:T\_1.t\_2:T\_1\to T\_2}
$$

Would this be read as *If we have established that under the assumptions of the type environment $\Gamma$ and the binding $x:T\_1$, that $t\_2$ has type $T\_2$; then [$\ldots$]*?

**Tags:** lo.logic, type-theory, terminology, type-systems

---

## 1 answers

### Answer by username_1 on 2013-08-13. Score: 7 | Accepted answer

The two inference rules are different, because the first requires that x:T\_1 is the only assumption, while the second allows side assumptions. This can have subtle effects of the consequence relation for the type theory prevents the type theory from modelling weakening by having as the hypothesis rule:

$$
\frac{}{\Gamma, x:A \vdash x:A}
$$

In your English gloss, I would have *under the sole assumption*, to avoid confusion with the assumption-gobbling inference rule:

$$
\frac{\Gamma, x:T\_1 \vdash t\_2 : T\_2}{\vdash \lambda x:T\_1.t\_2:T\_1\to T\_2}
$$


---

