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$
1
  • $\begingroup$ First-order Heyting arithmetic has decidable equality without excluded middle, so it is a reasonable combination. $\endgroup$
    – user44143
    Nov 20, 2022 at 20:39

2 Answers 2

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 = \mathsf{True}$ or $U \neq \mathsf{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 your 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, 2021 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$ May 5, 2021 at 18:44
5
$\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$ May 12, 2021 at 15:51
  • 2
    $\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$ May 12, 2021 at 17:42

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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