Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It only takes a minute to sign up.
Sign up to join this community
I have two questions regarding the empty type, $0$, in Martin-Löf type theory:
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) $$
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.
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$.
