Axiom:Axiom of Dependent Choice
(Redirected from Axiom:Axiom of Dependent Choices)
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
- The Axiom of Dependent Choice is a weaker form of the Axiom of Choice, as shown in Axiom of Choice Implies Axiom of Dependent Choice.
- The Axiom of Dependent Choice 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.
- Results about Axiom of Dependent Choice can be found here.