Typing relations terminology – how do I read typing relations?

Question

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$]?

Answer 1

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} $$