nLab dependent choice

Dependent choice

Dependent choice


 In set theory

In set theory, the axiom of dependent choice (DC) states that if XX is a nonempty (inhabited) set and if RR is a total binary relation on XX, then there exists a sequence x:Xx\colon \mathbb{N} \to X such that (x n,x n+1)(x_n, x_{n+1}) belongs to RR for all nn \in \mathbb{N}. It is strictly weaker than the full axiom of choice, but strictly stronger than the axiom of countable choice. It is called dependent choice because the available choices for x n+1x_{n+1} depend on the choice of x nx_n made at the previous stage.

 In dependent type theory

In dependent type theory, the axiom of dependent choice states that if AA is an inhabited set and if RR is a entire relation on AA, then then there exists a sequence a:Aa:\mathbb{N} \to A such that for all n:n:\mathbb{N}, R(a(n),a(n+1))R(a(n), a(n + 1)) holds.

ΓAtypeΓx:A,y:AR(x,y)typeΓDC A:(isSet(A)×[A])( x:A( y:AisProp(R(x,y)))×y:A.R(x,y))a:A. n:R(a(n),a(n+1))\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash x:A, y:A \vdash R(x, y) \; \mathrm{type}}{\Gamma \vdash \mathrm{DC}_\mathbb{N}^A:(\mathrm{isSet}(A) \times [A]) \to \left(\prod_{x:A} \left(\prod_{y:A} \mathrm{isProp}(R(x, y))\right) \times \exists y:A.R(x, y)\right) \to \exists a:\mathbb{N} \to A.\prod_{n:\mathbb{N}} R(a(n), a(n + 1))}


Typical applications of dependent choice include Kőnig's lemma? and the Baire category theorem for complete metric spaces.


For a number of schools of constructive mathematics, dependent choice is considered an acceptable alternative to full AC, and the principle holds (assuming that it holds in Set) in quite a few toposes of interest in which full AC doesn’t hold, including all presheaf toposes and the effective topos. In fact, it follows from the stronger presentation axiom, which holds in many of these toposes and also has a constructive justification.

Like countable choice, it fails for sheaves over the space of real numbers.


Last revised on November 8, 2023 at 17:21:39. See the history of this page for a list of all contributions to it.