4
$\begingroup$

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?

$\endgroup$
0

1 Answer 1

12
$\begingroup$

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.
$\endgroup$
2
  • $\begingroup$ 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. $\endgroup$ Nov 7, 2014 at 15:02
  • 1
    $\begingroup$ 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. $\endgroup$ Nov 7, 2014 at 21:23

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.