# Two questions about the empty type

I have two questions regarding the empty type, $0$, in Martin-Löf type theory:

1. I was reading that, in intuitionistic logic, one has $\neg\neg\neg P\rightarrow \neg P$. This amounts to finding a term of $$(P\times 0\times 0\rightarrow 0)\rightarrow (P \rightarrow 0)$$

2. Is it true that $0\rightarrow P$ for any $P$? If $P$ is inhabited, then we have $p:P$ and we can just define the constant function. If $P=0$, then identity works. But, I can't seem to find a general proof of this fact.

• What you say in 1 is wrong: $\lnot\lnot\lnot P$ is $((P \rightarrow 0) \rightarrow 0) \rightarrow 0$. This is not the same as $P \times 0 \times 0 \rightarrow 0$, which is the uncurrying of $P \rightarrow (0 \rightarrow (0 \rightarrow 0))$, where by convention you can omit the brackets. May 3, 2015 at 16:26

In intuitionsitic logic we have the rule :

$\bot \vdash P$, for $P$ whatever

i.e. form the "falsum" (a contradiction) we can derive a proposition whatever.

Thus, by $\rightarrow$-introduction, follows that :

$\vdash \bot \rightarrow P$.

With $\bot$, the negation is defined as

$\lnot P := P \rightarrow \bot$.

In Martin-Löf's Type Theory, the empty set ($\{ \}$ or $\Lambda$) takes the role of $\bot$ and we have that $\lnot P := P \rightarrow \{ \}$.

Thus, we must have also $\{ \} \rightarrow P$, for every $P$.