Intuitionistic “atomic” proof of negation?

Question

In the view of logic in terms of type theory (cf. the Curry-Howard correspondence), the type $\neg P$ is defined as $P\to False$, and a proof of $\neg P$ is therefore a function that takes a proof of $p$ and outputs an element of $False$.

It is easy to see how one might prove a negation $neg P$ from for example a negation $t_1:\neg Q$ and $t_2:P\to Q$: simply compose the two proofs: $t_3:\neg P := \lambda p:P, t_1 (t_2 (p))$.

But how do you prove the “first” negation, which cannot make use of other proofs of negation? To make it concrete, how do we prove $1\neq 2$? (Where $1$ is defined as $succ(0)$ and $2$ as $succ(succ(0))$ in a standard inductive definition of the natural numbers).

Answer 1

If two terms are equal, then they have the same properties. Let me state this more formally. Recall that equality satisfies the following elimination principle (the Leibniz principle, sometimes called transport) in Martin-Löf Type Theory: if $x = y : A$ and $\varphi : A \rightarrow \mathcal{U}$ is a predicate, then $\varphi(x) \rightarrow \varphi(y)$. You can either take this as one of the axioms of Martin-Löf Type Theory, or if you want to be really redundant, you can prove it immediately by applying Equality Axiom J (see slide 7 for a statement) to the term $\lambda x:A. \lambda x:A. \lambda p:x=y. \varphi(x) \rightarrow \varphi(y)$.

Now, take any two types $A,B:\mathcal{U}$ and assume that $A=B$. By Leibniz's principle, for any predicate $\varphi: \mathcal{U} \rightarrow \mathcal{U}$ we have $\varphi(A) \rightarrow \varphi(B)$. So set $\varphi$ to $\lambda x: \mathcal{U}. x$ to get that $A \rightarrow B$. Discharging the assumption, we have that $(A = B) \rightarrow (A \rightarrow B)$ for any two types $A,B$.

Setting $A$ to $\top$ and $B$ to $\bot$ yields $(\top = \bot) \rightarrow (\top \rightarrow \bot)$. But by the introduction principle for $\top$, we have $(\top = \bot) \rightarrow \top$ as well. Hence, $(\top = \bot) \rightarrow \bot$ holds as I claimed.

Using the Leibniz principle, we can prove the following congruence theorem: if $x=y:A$ and $f: A \rightarrow \mathcal{U}$, then $f(x) = f(y) : \mathcal{U}$. To do this, set $\varphi$ to $\lambda z. f(x) = f(z)$ in Leibniz's principle. We obtain that if $x=y$, then $f(x) = f(x) \rightarrow f(x) = f(y)$. But $f(x)=f(x)$ holds by the reflexivity of equality, so we can conclude $f(x) = f(y)$.

Now, we can apply the trick from L. Garde's answer: define the function $g: \mathbb{N} \rightarrow \mathcal{U}$ that sends zero to $\top$ and everything successor to $\bot$ (use the induction principle for $\mathbb{N}$ to obtain this function), then use the congruence theorem on $g$ to obtain $(0 = 1) \rightarrow (\top = \bot)$. We already know that $(\top = \bot) \rightarrow \bot$, so we conclude that $(0 = 1) \rightarrow \bot$ as well.

Answer 2

The idea to prove $1 \neq 2$ is to define a function that sends $1$ to a certain type or term, and $2$ to another type or term that you know cannot be equal.

You can prove $0 \neq 1$ easily by defining by induction a function that sends $0$ to the type $\mathbf{0}$ and all other natural numbers to the type $\mathbf{1}$. Then $0=1$ implies $\mathbf{0}=\mathbf{1}$. $\mathbf{1}$ is inhabited, so $\mathbf{0}=\mathbf{1}$ implies $\mathbf{0}$ is inhabited, and therefore $0 \neq 1$.

In the same way, you can define by induction a function that sends $0$ and $1$ to $\mathbf{0}$, and all other integers to $\mathbf{1}$. It results that $1\neq 2$.

There is a more systematic approach with the encode-decode method, that you can find for instance in the Chapter 2.13 of the HoTT book.