8
$\begingroup$

I have a basic question about propositional truncation $||$-$||$ and double negation $\neg\neg$.

According to the recursion rule of $||$-$||$, $A\rightarrow B=||A||\rightarrow B$ as long as $B$ is a mere proposition (i.e., proof-irrelevant). Now let $B=\neg\neg A$, since $\neg\neg A$ is a mere proposition, and $A\rightarrow\neg\neg A$ is a tautology, we naturally conclude that

$$||A||\rightarrow\neg\neg A.\quad\quad(1)$$

Since $||A||\rightarrow\neg\neg A$ is a tautology, then $\neg\neg(||A||\rightarrow\neg\neg A)$ is also a tautology. Since $\neg\neg$ distributes over $\rightarrow$, we get the following

$$\neg\neg||A||\rightarrow\neg\neg A.\quad\quad(2)$$

Therefore, the following is also true:

$$\neg\neg(||A||\rightarrow A).\quad\quad(3)$$

But (3) looks quite crazy because it's almost the inverse of $A\rightarrow||A||$, though under $\neg\neg$. I don't know if these are all correct. I would appreciate if someone can tell if it's correct or if there is anything wrong with my derivations.


More: Since there is a mapping for $A\rightarrow||A||$, its double negation $\neg\neg(A\rightarrow||A||)$ is also a tautology. Together with (3), we have $\neg\neg(A\leftrightarrow||A||)$. Is there any place wrong with my derivation?

$\endgroup$
9
  • $\begingroup$ What do you mean by "$\neg\neg$ distributes over $\to$"? $\endgroup$ Jul 11, 2020 at 17:14
  • $\begingroup$ @MikeShulman Thanks for the reply. It's $\neg\neg(\phi\rightarrow\psi)\leftrightarrow(\neg\neg\phi\rightarrow\neg\neg\psi)$. $\endgroup$
    – Emini Jask
    Jul 11, 2020 at 17:26
  • $\begingroup$ That's not immediately obvious to me; why is it true? $\endgroup$ Jul 11, 2020 at 18:15
  • $\begingroup$ @MikeShulman Hi Mike, you can take a look at Lemma 6.2.2 in van Dalen's textbook Logic and Structure (Click the link. It's an electronic version). The proof for this equivalence in intuitionistic logic is given on pages 159-160. $\endgroup$
    – Emini Jask
    Jul 11, 2020 at 19:22
  • 1
    $\begingroup$ Regarding craziness, even having a function $\Vert A \Vert \to A$ for all $A$ would not be an inverse of $A\to \Vert A \Vert$, only a section of it. That's essentially a strong axiom of choice, "every inhabited type has a specified element" -- strong enough to contradict univalence, but consistent to assume under UIP. Note that the weaker statement that $\Vert (\Vert A \Vert \to A)\Vert$ holds for all $A$ is not contradictory, and indeed follows from LEM, but is still not constructively provable. $\endgroup$ Jul 12, 2020 at 23:03

2 Answers 2

6
$\begingroup$

Your arguments are correct as stated. It is indeed the case that the ($\Pi$-closures of the) types $\neg\neg (||A|| \rightarrow A)$ and $\neg\neg (||A|| \leftrightarrow A)$ are inhabited, and for the reasons outlined above.

The second part of your question far subtler: it asks about the "craziness" of the fact that these types are inhabited. I'm not sure how to answer this (although I suspect that a good answer is possible, and will eventually be penned by someone else). In the meantime, I offer a few remarks.

It's not surprising that we have functions $|| \bot || \rightarrow \bot$ or $||\mathbb{N}|| \rightarrow \mathbb{N}$ for fixed types $\bot, \mathbb{N}$. However, we certainly would not expect any term to inhabit $\Pi A:\mathbf{U}.||A|| \rightarrow A$. However, actually proving that there is no term of that type seems like a task that would involve fairly elaborate semantic reasoning (assuming that this is indeed the case; I might ask a followup question about this later).

The fact that we can construct an inhabitant of the type $\Pi A:\mathbf{U}.\neg\neg (||A|| \rightarrow A)$ is a pleasant surprise, but it does not say much about the inhabitedness of the former, as we still can't prove $\neg\neg \Pi A:\mathbf{U}.(||A|| \rightarrow A)$. In fact, there is a fairly direct proof of $\Pi A:\mathbf{U}.\neg\neg(||A|| \rightarrow A)$ that does not invoke the distributivity of $\neg\neg$, and might illuminate what's going on.

We can prove $\Pi A:\mathbf{U}.\neg(||A|| \rightarrow A) \rightarrow \neg A$ simply by taking $f : \neg(||A|| \rightarrow A)$ and $a : A$, and constructing $f(\lambda x.a) : \bot$. Similarly, we can prove $\Pi A:\mathbf{U}. \neg A \rightarrow ||A|| \rightarrow A$ since given $a : || A ||$ and $f: A \rightarrow \bot$ we can get $\mathrm{squashrec}(f): || A || \rightarrow \bot$, and then $\mathrm{squashrec}(f)(a) : \bot$. Putting these together we have a term of type $\Pi A:\mathbf{U}.\neg(||A|| \rightarrow A) \rightarrow || A || \rightarrow A$, from which $\Pi A:\mathbf{U}.\neg\neg(||A|| \rightarrow A)$ readily follows.

$\endgroup$
2
  • 1
    $\begingroup$ "I suspect that a good answer is possible, and will eventually be penned by someone else" -- indeed, it looks like one might have appeared while I was writing this answer. $\endgroup$
    – Z. A. K.
    Jul 11, 2020 at 22:40
  • 2
    $\begingroup$ One can prove internally that $\Pi A:\mathbf{U}. \Vert A\Vert\to A$ contradicts the univalence axiom; this is Exercise 3.11 in the HoTT Book. Thus, since the univalence axiom is consistent (which might be considered "elaborate semantic reasoning"), that type is uninhabitable. $\endgroup$ Jul 12, 2020 at 22:58
5
$\begingroup$

Everything you’ve said works, and there’s a simple intuition for it all: $\neg\neg\cdot$ is a modality, and so is $\Vert\cdot\Vert$, and the latter is a “loosening” of the former. Specifically, they’re equivalent under the former (that is, $\prod_{A : \mathcal{U}} \neg\neg (\Vert A\Vert \simeq \neg\neg A)$), because we can prove $\mathrm{LEM}_{\neg\neg} :\equiv \prod_{A : \mathcal{U}} \neg\neg (A + \neg A)$. So if we assume $\mathrm{LEM}_{-1} :\equiv \prod_{A : \mathcal{U}} \mathrm{isProp}(A) \to \left\Vert A + \neg A\right\Vert$, then the two modalities are purely equivalent too.

The way I like to think about this is that, in a classical setting, propositional truncation is just the same thing as double negation, which is already well known to produce a classical environment in an otherwise constructive setting. So in the general constructive-by-default setting of MLTT and its descendants, propositional truncation isn’t automatically equivalent to double negation, but you also can’t prove that it’s disequivalent without an explicit anticlassicality principle—and they’ll always be equivalent in the “forced classical” environment underneath double negation.

$\endgroup$

You must log in to answer this question.

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