# Axiom:Axiom of Dependent Choice

## Axiom

### Left-Total Form

Let $\mathcal R$ be a binary relation on a non-empty set $S$.

Suppose that:

- $\forall a \in S: \exists b \in S: a \mathrel{\mathcal R} b$

that is, that $\mathcal R$ is a left-total relation (specifically a *serial relation*).

The **axiom of dependent choice** states that there exists a sequence $\left\langle{x_n}\right\rangle_{n \in \N}$ in $S$ such that:

- $\forall n \in \N: x_n \mathrel{\mathcal R} x_{n+1}$

### Right-Total Form

Let $\mathcal R$ be a binary relation on a non-empty set $S$.

Suppose that:

- $\forall a \in S: \exists b \in S: b \mathrel{\mathcal R} a$

that is, that $\mathcal R$ is a right-total relation.

The **axiom of dependent choice** states that there exists a sequence $\left\langle{x_n}\right\rangle_{n \in \N}$ in $S$ such that:

- $\forall n \in \N: x_{n+1} \mathrel{\mathcal R} x_n$

## Also known as

Some sources call this the **Axiom of Dependent Choices**, reflecting the infinitely many choices made.

This axiom can be abbreviated **ADC** or simply **DC**.

## Also see

- This axiom is a weaker form of the axiom of choice, as shown in Axiom of Choice Implies Axiom of Dependent Choice.

- This axiom is also a stronger form of the axiom of countable choice, as shown in Axiom of Dependent Choice Implies Axiom of Countable Choice.

- Dependent Choice (Fixed First Element) shows that it is possible to choose any element of the set to be the first element of the sequence.