Axiom:Axiom of Dependent Choice

From ProofWiki
Jump to navigation Jump to search

Axiom

Left-Total Form

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

Suppose that:

$\forall a \in S: \exists b \in S: a \mathrel \RR b$

that is, that $\RR$ is a left-total relation (specifically a serial relation).


The axiom of dependent choice states that there exists a sequence $\sequence {x_n}_{n \mathop \in \N}$ in $S$ such that:

$\forall n \in \N: x_n \mathrel \RR x_{n + 1}$


Right-Total Form

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

Suppose that:

$\forall a \in S: \exists b \in S: b \mathrel \RR a$

that is, that $\RR$ is a right-total relation.


The axiom of dependent choice states that there exists a sequence $\sequence {x_n}_{n \mathop \in \N}$ in $S$ such that:

$\forall n \in \N: x_{n + 1} \mathrel \RR 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

  • Results about Axiom of Dependent Choice can be found here.