7
$\begingroup$

In (constructive) homotopy type theory, the law of excluded middle is not derivable. Moreover, assuming parametricity it is refutable.

But, one can work inside the double negation modality to obtain (a form of) the law of excluded middle.

The question now is, can the same be done to obtain the axiom of choice? To be exact, is there a modality M such that the type $\Pi x : A. \|\Sigma y : B. R(x, y)\| \to M \|\Sigma f : A \to B. \Pi x : A. R (x, f(x))\|$ is inhabited?

$\endgroup$
  • $\begingroup$ This is a good question, for which I don't know the answer. But let me share my intuition that no such modality exists: As you say, by exploiting the double negation modality, we can eliminate the law of excluded middle from proofs (at the cost of also modifying the claimed statements). But no similarly general technique for eliminating the axiom of choice is known. (Of course there are several specialized techniques, for instance employing generic models which live in classifying toposes or employing the dynamical methods in algebra, but these are not based on a modality.) $\endgroup$ – Ingo Blechschmidt Sep 26 at 15:11
  • $\begingroup$ Waht is $\|{-}\|$? Shouldn't the modal AC read $(\Pi (x : A) . M(\Sigma (y : B) . R(x,y))) \to M (\Sigma (f : A \to B) . \Pi (x : A) . R(x, f(x)))$? And while you're at it, what does "modality" mean for you? Like the ones in the HoTT book? $\endgroup$ – Andrej Bauer Sep 26 at 19:26
  • $\begingroup$ @AndrejBauer $\|-\|$ is propositional truncation but I think the other point, defining modality, as also Mike Shulman points out in his answer below, is more challenging. Initially I meant the terms in HoTT book, yes. I posed this question from an undergraduate view, and as of now, I think the question is ill-posed. There is definitly a lot to unpack for me already. I believe a better question for now (homework for me) would be "why, exactly, is the double negation modality so useful". The reason I asked was to get a sense how to translate a proof using AC into HoTT language. $\endgroup$ – WorldSEnder Sep 26 at 21:53
5
$\begingroup$

There is a trivial sense in which the answer is yes. For any proposition $P$, there's a modality $O_P$ called the open modality determined by $P$, defined by $O_P(X) \equiv (P\to X)$. If you take $P$ to be the statement of the axiom of choice (relative to some universe), then for $M=O_P$ the type you showed is inhabited, since you get to use the axiom of choice in proving the conclusion.

However, this is not as useful as the double-negation modality for LEM. To see why, notice that there is an even more trivial sense in which the answer is yes, namely when $M$ is the trivial modality, $M_{\rm triv}(X) \equiv \mathbf{1}$. Obviously that's not very interesting. The point is that $M_{\rm triv} = O_{\mathbf{0}}$, and if we don't know whether $P=\mathbf{0}$ (such as when $P=\rm AC$), then we don't know whether $O_P = M_{\rm triv}$. (And in fact, in models where $\rm AC$ is refutable, we do have $O_{\rm AC} = M_{\rm triv}$.) The same argument applies to $P=\rm LEM$, of course; but $O_{\rm LEM}$ is not the same as double-negation, and we can prove that double-negation is always nontrivial (e.g. $\neg\neg \mathbf{0} = \mathbf{0}$). So this "answer" is not really telling us anything.

As Ingo says, it seems unlikely that we can construct any provably-nontrivial modality with this property. I don't know how to prove that we can't, but I think I can prove that no such lex modality can be constructed in the absence of univalence. Take a model of ZF that doesn't satisfy AC. Then its topos of sets is a model of MLTT with function extensionality, propositional extensionality, propositional truncation, and propositional resizing, in which lex modalities correspond to geometric subtoposes; but it has no proper nontrivial geometric subtoposes.

It should be possible to include Univalence as well, but I'm hazy on the necessary details. Voevodsky's original simplicial model of HoTT has no nontrivial proper lex modalities, but its construction uses AC. More recent cubical-type models of HoTT are constructive, but many of them do have nontrivial proper lex modalities. Possibly the recent "equivariant" cartesian cubical model would work: it exists constructively, and classically is Quillen equivalent to the simplicial model and hence has no nontrivial proper lex modalities; but I'm not quite sure whether the latter equivalence uses AC or only LEM.

Relaxing lexness is going to be trickier, since even the classical simplicial model has lots of nontrivial proper non-lex modalities, like the $n$-truncations for all $n$. I don't know whether there's any classification of all such modalities, or any other way to verify that none of them make AC true.

$\endgroup$
  • $\begingroup$ One other thing I meant to mention but forgot: in addition to the actual double-negation modality $\neg\neg$, at least if we have propositional resizing we can form the double-negation-sheafification modality by localizing at all the double-negation-closed propositions. The latter is lex and hence yields an entire "world" in which LEM holds, whereas for $\neg\neg$ itself the only modal types are the double-negation-closed propositions themselves. $\endgroup$ – Mike Shulman Sep 27 at 19:19
  • $\begingroup$ That's a lot of input for me. I will mark this as an answer even if I know that my question is not really precise enough to give a definite one. I appreciate the effort. $\endgroup$ – WorldSEnder Sep 29 at 2:28

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.