Skip to main content

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.

Simon Henry
  • 42.4k
  • 5
  • 107
  • 205