5
$\begingroup$

The law of excluded middle in homotopy type theory is a term of $$\prod_{A:\mathcal{U}}\Big(\mathrm{isProp}(A)\to(A+\neg A)\Big).$$What if we assume a term of$$\prod_{A:\mathcal{U}}\Big(\mathrm{isSet}(A)\to\prod_{x,y:A}\big((x=y)+\neg (x=y)\big)\Big)$$instead?

Is this a strictly weaker axiom than LEM? Is it useful? Are there any philosophical reasons to accept this axiom but not LEM?

EDIT: If we only assume a term of$$\prod_{A:\mathcal{U}_0}\Big(\mathrm{isSet}(A)\to\prod_{x,y:A}\big((x=y)+\neg (x=y)\big)\Big)$$does that change much?

$\endgroup$
6
$\begingroup$

Decidability of every set implies the law of excluded middle as soon as there is a "subobject classifier".

Indeed, for every proposition $U$, the fact that "$U = True$ or $U \neq True$" is exactly the same as $U$ or not $U$.

Regarding your edit: it depends. If you include some axiom of 'Propositional resizing' in HoTT (which is quite common) then the type of all propositions will be (equivalent to a type) in $\mathcal{U}_0$, then the argument above still apply and your axiom is equivalent to LEM.

Without any form of propositional Resizing, I think you're axiom is indeed strictly weaker than LEM. (Edit: as pointed out in aws answer below, having some higher inductive type and assuming they are in $\mathcal{U}_0$ also allows to deduce LEM from your axiom)

Now, it is still a very non-constructive principle, remember (for example, it let you decide whether $\forall n, f(n) =0$ holds or not for any function $f: \mathbb{N} \to \mathbb{N}$, which is pretty much what people interested in constructivity for philosophical reason don't want). So I can't think of any good reason to really distinguish this axiom, but of course, that's only my opinion.

$\endgroup$
2
  • $\begingroup$ Is $U$ a term of a set? $\endgroup$ – Mallon May 5 at 18:42
  • $\begingroup$ I'm using that the type of all propositions is a set, that's what I mean by a "subobject classifier". U is a proposition. $\endgroup$ – Simon Henry May 5 at 18:44
4
$\begingroup$

In addition to Simon Henry's proof you can also use suspensions to show that decidable equality implies the law of excluded middle. Given a proposition $A : \mathrm{hProp}$ you can show using an encode-decode argument that the suspension $\Sigma A$ is a set and that the equality $N = S$ is equivalent to $A$. So decidable equality for every set of the form $\Sigma A$ implies the law of excluded middle.

$\endgroup$
2
  • 3
    $\begingroup$ Note that $\Sigma A$ is the same set that appears in the Diaconescu-Goodman-Myhill proof that the axiom of choice implies excluded middle. $\endgroup$ – Mike Shulman May 12 at 15:51
  • 1
    $\begingroup$ @MikeShulman: and indeed the D–G–M proof can usefully be factored as “If all subsets of A satisfy choice, then A has decidable equality” (which doesn’t need general quotients/suspension, just propositional truncation) and “if all sets have decidable equality, then LEM holds” (using set quotients/suspension as you say). $\endgroup$ – Peter LeFanu Lumsdaine May 12 at 17:42

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.