When and what must be present on the left-hand side of the turnstile in metalogics?

Question

Let me show the problem on an example...

An actual task from one of the former exams:

Consider a simple functional language:

$$e::= x|n|e_1e_2|\lambda x.e$$

With typing rules:

$$\tau ::= \mathtt{int} | \mathtt{foo} | \tau_1 \rightarrow \tau_2$$

$$\Gamma \vdash n : \mathtt{int}$$

$$\Gamma (x : \tau) \vdash x : \tau$$

$$\begin{array} {c} \Gamma(x : \tau) \vdash e : \rho \\ \hline \Gamma \vdash \lambda x.e : \tau \rightarrow \rho\end{array}$$

$$\begin{array}{c} \Gamma\vdash e_1:\tau\rightarrow \rho\quad\Gamma\vdash e_2:\tau \\ \hline \Gamma\vdash e_1e_2 : \rho\end{array}$$

$$\begin{array}{c}\Gamma\vdash e:\tau \\ \hline \Gamma\vdash e: \mathtt{foo}\end{array}$$

Where the environment $\Gamma$ is a partial function from the set of variables into the set of types and $\Gamma(x:t)$ denotes an environment that assignts the type $t$ to the variable $x$ and works like $\Gamma$ for all other variables.

Derive types for the following expressions:

(omitted for brevity)

Example: Type derivation for $\lambda x.\lambda y.x$:

$$\begin{array}{c}x:\alpha,\;y:\beta\vdash x:\alpha \\ \hline x:\alpha\vdash \lambda y.x:\beta\rightarrow\alpha \\ \hline \vdash\lambda x.\lambda y. x : \alpha \rightarrow (\beta\rightarrow\alpha) \end{array}$$

It is this example that perplexes me. Why is it necessary to put $x:\alpha$ on the left-hand side of $\vdash$ in the second step of the derivation? My thinking is that $\lambda x.y : \beta\rightarrow \alpha$ results from both $x:\alpha$ and $y:\beta$ so there's no reason to put $x:\alpha$ on the lhs of $\vdash$ but not $y:\beta$.

But $\begin{array}{c}x:\alpha,\;y:\beta\vdash x:\alpha,\; y:\beta \\ \hline x:\alpha,\; y:\beta\vdash \lambda y.x:\beta\rightarrow\alpha \end{array}$ is a tautology that brings in nothing, so we should instead simplify this to $\begin{array}{c}x:\alpha,\;y:\beta \\ \hline \vdash \lambda y.x:\beta\rightarrow\alpha \end{array}$. Note that this is precisely what the third step of derivation seems to be doing: $\begin{array}{c} x:\alpha\vdash \lambda y.x:\beta\rightarrow\alpha \\ \hline \vdash\lambda x.\lambda y. x : \alpha \rightarrow (\beta\rightarrow\alpha) \end{array}$ They simply put nothing on the left-hand side of the $\vdash$.

What am I missing here? Is this related to the form of the axiom that seems to be used here - $\begin{array} {c} \Gamma(x : \tau) \vdash e : \rho \\ \hline \Gamma \vdash \lambda x.e : \tau \rightarrow \rho\end{array}$ - where the environment used above the vertical line contains the assignment $x:\tau$ while the environment used below the vertical line is devoid of this assignment? Which is why in $x:\alpha\vdash \lambda y.x:\beta\rightarrow\alpha$ the assignment $x:\alpha$ must be present before the $\vdash$, but the assignment $y:\beta$ must not? Is my reasoning correct? But if it is, then why does the third step seem to differ and is of the form $\vdash\lambda x.\lambda y. x : \alpha \rightarrow (\beta\rightarrow\alpha)$ and not $\lambda y.x : \beta\rightarrow\alpha \vdash\lambda x.\lambda y. x : \alpha \rightarrow (\beta\rightarrow\alpha)$?

Or am I splitting hairs here? But my thinking is that I'm not certain what degree of accuratness is required by this professor so I wouldn't like to loose points on something of this sort... Could you clear my confusion?

Answer 1

Perhaps what you're missing (although you seem to suspect) is that the left hand side of the $⊢$ is not just for specifying what types variables have. In fact, as you've noted, it doesn't necessarily have all (or only) the variables on the right hand side (although in this situation it does only have variables, not things like $λy.x : α→β$).

What it's doing is keeping track of what are sometimes called the "free variables" on the right hand side, along with their specified types. The idea is essentially that there are actually no free variables in this formalism; variables are either bound by a $λ$ or in the context $Γ$. The lambda introduction rule:

$$\begin{array}{c}Γ(x:τ) ⊢ e : ρ \\ \hline Γ ⊢ λx.e : τ → ρ\end{array}$$

moves a variable from being bound in the context to being bound by a lambda. In some presentations this might even be written $λx:τ.e$ to still be explicit about what type $x$ has, but this is not really necessary when working with a derivation where the type is already recorded in the judgment (and there are other situations as well).

Of course, variables can go in the context even if they don't occur on the right hand side, like $y$ in your example. This allowed writing a constant function that doesn't actually use its argument.

One way to think about this is to read the tree bottom to top. We want to verify that $λx.λy.x$ has type $α→β→α$. The way we do this is to start in the empty context, and move upward. We use the lambda introduction rule to push lambda-bound variables into the context with an appropriate type, and eventually verify that $$x:α,y:β⊢x:α$$ holds. This is maybe more obvious if the variable rule has a line above it, allowing you to create a completed tree:

$$\begin{array}{c}\\ \hline x:α,y:β⊢x:α \\ \hline x:α ⊢ λy.x : β→α \\ \hline ⊢ λx.λy.x : α→β→α \end{array} $$

The root of the tree is our goal at the bottom, and the leaves at the top are all empty lines. $Γ$ is the local context in which we are verifying the inner parts of the lambda term, and its content is actually motivated by wanting to move under the lambda and verify the type of its body; it contains the variables and their types that have been brought into scope in that process.