<p>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 <em>eliminator</em>.)
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.</p>

<p>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:</p>

<pre><code>Definition ex_falso_quodlibet (A : Set) (x : Empty_set) : A :=
    match x with end.
</code></pre>

CC BY-SA 3.0
2014-11-07T15:02:56.457Z
So it seems it is not pure lambda calculus, but something I'd call $\lambda$-absurd calculus, right? And getting falsum in pure lambda is impossible.
Mateusz Grotek
CC BY-SA 3.0
2014-11-07T21:23:03.817Z
Well, whenever you add a new type or a new constructor to type theory, you should not be surprised by the addition of new terms, namely those that correspond to the introduction and elimination rules on the logic side of things. You make it sounds like this is a bad thing, but it is completely expected. You wouldn't be suprised to get wet when you go swimming, either.
Andrej Bauer
CC BY-SA 3.0
2014-11-02T20:06:39.763Z
2014-11-02T22:01:35.880Z
2014-11-02T22:01:35.880Z
Andrej Bauer
<p>The sentence $\bot\rightarrow A$ is provable in intuitionistic logic for any type $A$. The proof is trivial:</p>

<p>\begin{align}
\bot&amp;\vdash\bot \\
\hline
\bot&amp;\vdash A \\
\hline
&amp;\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?</p>

<lo.logic><lambda-calculus><typed-lambda-calculus>
What is a term of the type $\bot\rightarrow A$?
Mateusz Grotek
# What is a term of the type $\bot\rightarrow A$?

(Asked by: username_0 on 2014-11-02)

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?

**Tags:** lo.logic, lambda-calculus, typed-lambda-calculus


---

## 1 answers

### Answer by username_1 on 2014-11-02. Score: 12 | Accepted answer

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.

> **Comments:**
> **username_0**: So it seems it is not pure lambda calculus, but something I'd call $\lambda$-absurd calculus, right? And getting falsum in pure lambda is impossible.  
> **username_1**: Well, whenever you add a new type or a new constructor to type theory, you should not be surprised by the addition of new terms, namely those that correspond to the introduction and elimination rules on the logic side of things. You make it sounds like this is a bad thing, but it is completely expected. You wouldn't be suprised to get wet when you go swimming, either.  

---

