nLab decidable choice

Context

Foundations

foundations

The basis of it all

 Set theory

set theory

Foundational axioms

foundational axioms

Removing axioms

Contents

 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. 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 January 3, 2023 at 04:33:06. See the history of this page for a list of all contributions to it.