1
$\begingroup$

I'm currently trying to learn type theory from the first chapter of HoTT. It is remarked that we cannot prove $\neg\neg A \rightarrow A$, when $A$ is interpreted as a proposition, or, equivalently, we cannot construct an element of $((A\rightarrow\mathbf{0})\rightarrow \mathbf{0})\rightarrow A$, when $A$ is interpreted as a type. However, can we prove from within type theory that this is unprovable? In other words, can we construct an element of the following type?

$$\Bigg(\prod_{A:\mathcal{U}} \big(((A\rightarrow\mathbf{0})\rightarrow \mathbf{0})\rightarrow A\big)\Bigg)\rightarrow \mathbf{0}$$

If so, what is such an element? I've been struggling to explicitly construct one myself, to no avail.

$\endgroup$
6
  • 9
    $\begingroup$ You are not asking us whether we can prove it’s unprovable. You are asking whether we can prove it’s false, which we cannot do. $\endgroup$
    – Mark Saving
    Jan 21 at 22:54
  • 2
    $\begingroup$ Note that in HoTT, you can prove what you actually wrote using univalence, because you have not limited it to homotopy propositions $A$. $\endgroup$
    – Dan Doel
    Jan 21 at 23:10
  • $\begingroup$ @MarkSaving Hmm. How would you formulate the proposition that it's unprovable (but not necessarily false) as a type? $\endgroup$
    – Franklin Pezzuti Dyer
    Jan 21 at 23:15
  • $\begingroup$ @DanDoel I'm not that far into the book yet :( $\endgroup$
    – Franklin Pezzuti Dyer
    Jan 21 at 23:16
  • 2
    $\begingroup$ @FranklinPezzutiDyer One customary way to approach this sort of thing is with Gödel numbers. You would essentially encode type theory derivations as numbers. You could then phrase (in the language of first-order Peano arithmetic) the statement “There is some term $t$ and some derivation of the fact that $t : T$”. You would seek to prove the proposition that if Double Negation Elimination is provable, then $0$ is provable, which you can carry out in Peano arithmetic (and, if you work very hard, likely in something even weaker like PRA). $\endgroup$
    – Mark Saving
    Jan 21 at 23:31

2 Answers 2

Reset to default
4
$\begingroup$

As @DanDoel noticed, you can construct an element of $\big(\prod_{A:U}(\neg\neg A\to A)\big)\to \mathbb{0}$, this is Theorem 3.2.2 of the HoTT book.

If you restrict it to propositions, $\prod_{A:U}\big(\text{isProp}(A)\to(\neg\neg A\to A)\big)$ is the law of double negation, and is equivalent to the law of excluded middle LEM.

It is not possible to prove LEM in HoTT, but it can be admitted as an axiom, so $\text{LEM}\to \mathbb{0}$ is not provable either. This is discussed in §3.4.

$\endgroup$
0
$\begingroup$

Just because something is unprovable doesn't mean it is false. For example, if $\phi$ is unprovable it means there exists both a model of your theory validating $\phi$ and one that validates $\neg\phi$. In particular this means you could add either as an axiom and your theory will be consistent (for example commutativity in group theory).

Now as already pointed out, your statement is indeed provable using univalence, but not for propositions.

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