2
$\begingroup$

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.

$\endgroup$
1
  • $\begingroup$ 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. $\endgroup$
    – Rob Arthan
    May 3, 2015 at 16:26

1 Answer 1

3
$\begingroup$

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$.

$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .