nLab decidable choice

 Idea

In constructive mathematics, the axiom of decidable choice ought to be a weak form of the axiom of choice which states that every set with decidable equality is a projective object in Set.

Decidable choice implies countable choice because the natural numbers have decidable equality. By BauerSwan18 there is a topos (the function realizability topos, which moreover satisfies Markov's principle and other axioms) in which all sets with decidable equality are countable (admit a surjection from a decidable subset of $\mathbb{N}$), so decidable choice coincides with countable choice. Conversely, in the context of excluded middle, decidable choice is the same as the full axiom of choice, because every set has decidable equality in the context of excluded middle.

 See also

• axiom of choice
• countable choice

 References

• Andrej Bauer and Andrew Swan, Every metric space is separable in function realizability, 2018, arxiv