nLab decidable choice




The basis of it all

 Set theory

set theory

Foundational axioms

foundational axioms

Removing axioms



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


Last revised on February 23, 2024 at 23:29:16. See the history of this page for a list of all contributions to it.