What is a term of the type $\bot\rightarrow A$?

Question

The sentence $\bot\rightarrow A$ is provable in intuitionistic logic for any type $A$. The proof is trivial:

\begin{align} \bot&\vdash\bot \\ \hline \bot&\vdash A \\ \hline &\vdash\bot\rightarrow A \end{align} It means there has to be a lambda term with this type (the type has to be inhabited). What is it?

Answer 1

There are several ways of writing such a term, depending on how we write the proof terms for the elimination rule for $\bot$, which is $$\frac{\quad\bot\quad}{A}$$ The corresponding rule in $\lambda$-calculus is $$\frac{\Gamma \vdash e : \bot}{\Gamma \vdash \mathtt{absurd}_A(e) : A}.$$ (We call $\mathtt{absurd}_A$ an eliminator.) Thus, the term of type $\bot \to A$ you seek is simply $$\lambda x : \bot \,.\, \mathtt{absurd}_A(x).$$ Another way of writing the same thing is with a $\mathtt{match}$ statement. To see how this works, let us first consider a $\mathtt{match}$ statement for disjunctions. The elimination rule for $\lor$ is $$\frac{A \lor B \qquad {\begin{matrix}A \\ \vdots \\ C\end{matrix}} \qquad {\begin{matrix}B \\ \vdots \\ C\end{matrix}}}{C}$$ The corresponding term constructor for $\lambda$-calculus can be written as $$\frac{\Gamma \vdash e_1 : A+B \qquad \Gamma, x : A \vdash e_2 : C \qquad \Gamma, y : B \vdash e_3 : C}{\Gamma \vdash (\mathtt{match}\;e_1\;\mathtt{with}\;\mathtt{inl}(x) \to e_2 \mid \mathtt{inr}(y) \to e_3 \; \mathtt{end}) : C}$$ In general, the $\mathtt{match}$ statement which eliminates an $n$-fold sum $A_1 + A_2 + \cdots + A_n$ has $n$ cases.

The empty type $\bot$ is like a nullary sum, so it corresponds to a $\mathtt{match}$ statement with zero cases: $$\frac{\Gamma \vdash e : \bot}{\Gamma \vdash (\mathtt{match}\;e\;\mathtt{with}\;\mathtt{end}) : C}$$ Indeed, this is how you can do it in Coq:

Definition ex_falso_quodlibet (A : Set) (x : Empty_set) : A :=
    match x with end.