0
$\begingroup$

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

$\endgroup$
4
  • $\begingroup$ There are lots of negative statements in the background you can use to get your “first” negation. For instance, $\top \ne \bot$ in the type of truth values. $\endgroup$
    – Zhen Lin
    Oct 21, 2020 at 15:02
  • $\begingroup$ Where does $\top \neq \bot$ come from? (It seems to me that this is a statement analogous to $1\neq 2$. I might as well have asked, how do we prove $\top\neq \bot$) $\endgroup$
    – user56834
    Oct 21, 2020 at 15:13
  • $\begingroup$ Given a proof that two types $A,B$ are equal, we can construct (using the induction principle for equality) a proof of $A \rightarrow B$. In particular $(\top = \bot) \rightarrow (\top \rightarrow \bot)$. But we can prove $\top$ (by the induction principle for $\top$) so we get $(\top = \bot) \rightarrow \bot$, i.e. $\top \neq \bot$. $\endgroup$
    – Z. A. K.
    Oct 22, 2020 at 2:26
  • $\begingroup$ @Z.A.K., Thanks! This together with L. Garde's answer seems like it answers the question. Maybe you should turn it into an answer? Together with an explanation of exactly how to construct an element of $\top \to \bot$ from $\top = \bot$. $\endgroup$
    – user56834
    Oct 22, 2020 at 3:39

2 Answers 2

3
$\begingroup$

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.

$\endgroup$
2
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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