basic constructions:
strong axioms
further
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.
Last revised on February 23, 2024 at 23:29:16. See the history of this page for a list of all contributions to it.