3
$\begingroup$

Axiom of Choice:

Given a collection $A$ of nonempty sets, there exists a function $$c: A \to \bigcup_{A_{i} \in A}A_{i}$$ such that $c(A_{i})\in A_{i}$ for all $A_{i} \in A$.

Axiom of Dependent Choice:

Given a nonempty set $A$ and a binary relation $\mathcal{R}$ on $A$ such that for all $a\in A$, there exists $b\in A$ such that $a\mathcal{R}b$. There exists a sequence $$(a_{n})_{n\in \mathbb{N}}$$ such that $a_{n}\mathcal{R}a_{n+1}$ for all $n \in \mathbb{N}$.

Here is my incomplete proof that Axiom of Choice implies Axiom of Dependent Choice:

For $a\in A$, let $R(a)=\{b\in A\mid a\mathcal{R}b\}\implies R(a)\neq\varnothing$ for all $a\in A$.

Using Axiom of Choice for the indexed family of sets $(R(a))_{a\in A}$, there exists a mapping

$$f:A\to A$$ such that $$\forall a\in A:f(a)\in R(a)$$

$\text{That is }\forall a\in A:a\mathcal{R}f(a)$. Let $B=\{(a,f(a))\mid a\in A\}$

I don't know how to proceed to prove the existence of the required sequence $(a_{n})_{n\in \mathbb{N}}$ from set $B$.

Please help me complete my proof! Many thanks for you!

$\endgroup$
1

3 Answers 3

Reset to default
3
$\begingroup$

You're basically done already: pick some $a\in A$ and consider the sequence $$a, f(a),f(f(a)), f(f(f(a))), ...$$ The $f$ that choice provides us is exactly the "strategy" we use to build the desired sequence.

$\endgroup$
24
  • $\begingroup$ I think your "strategy" looks like defining a sequence recursively. Is it true that your "strategy" implicitly appeals to Theorem of Recursion (wikiwand.com/en/Recursion#/The_recursion_theorem)? $\endgroup$
    – Akira
    Feb 23, 2018 at 1:27
  • $\begingroup$ @leanhdung No, actually! It follows just from the Separation axiom: we pick $a\in A$ and let $B$ be the set of $b\in A$ such that there is a finite chain of $f$-applications linking $a$ to $b$. This doesn't need the recursion theorem at all. (And incidentally, the recursion theorem doesn't need choice, so even if it was necessary that would be fine.) $\endgroup$
    – Noah Schweber
    Feb 23, 2018 at 1:34
  • $\begingroup$ The key point that lets us avoid the recursion theorem (that is, that makes this argument work in the axiom system Z, which is ZF minus Replacement and within which the recursion theorem is not provable) is that everything is taking place inside a fixed set $A$. $\endgroup$
    – Noah Schweber
    Feb 23, 2018 at 1:35
  • $\begingroup$ Yes, we only need Axiom of Separation to form such sets $R(a)=\{b\in A\mid a\mathcal{R}b\}$ for all $a\in A$, but what I meant is that you must use Recursion Theorem at the end to form $(a_{n})_{n\in \mathbb{N}}$ from mapping $f:A\to A$. $\endgroup$
    – Akira
    Feb 23, 2018 at 7:58
  • $\begingroup$ @leanhdung No, you don't - you can just use Separation. The application of Separation is a bit more complicated, as my comment says above. The recursion theorem is not needed here. $\endgroup$
    – Noah Schweber
    Feb 23, 2018 at 11:39
2
$\begingroup$

Once you have $f$, use the assumption that $A$ is nonempty to choose $x \in A$. Now, you can define a sequence recursively by $a_0 = x$, $a_{n+1} = f(a_n)$. (So for example, $a_1 = f(x)$, $a_2 = f(f(x))$, $a_3 = f(f(f(x)))$, etc.)

$\endgroup$
2
  • $\begingroup$ Since your answer mentions "define a sequence recursively", is it true that you implicitly appeal to Recursion Theorem (wikiwand.com/en/Recursion#/The_recursion_theorem)? at the end to form $(a_{n})_{n\in \mathbb{N}}$? $\endgroup$
    – Akira
    Feb 23, 2018 at 8:02
  • $\begingroup$ Yes, it uses the existence part of that theorem. $\endgroup$
    – Daniel Schepler
    Feb 23, 2018 at 17:32
1
$\begingroup$

I think you're almost there: now define $$ a_0 := a, a_n := f^n(a)$$ for some $a \in A$.

$\endgroup$
3
  • $\begingroup$ The way you acquire $(a_{n})_{n\in \mathbb{N}}$ makes me feel like you implicitly appeal to Recursion Theorem (wikiwand.com/en/Recursion#/The_recursion_theorem). Is my understanding true? $\endgroup$
    – Akira
    Feb 23, 2018 at 8:13
  • $\begingroup$ I don't think so. $f^n$ is a well-defined function for all $n \in \mathbb{N}$, so I am defining $a_n$ "explicitly". But I might be wrong, I am not an expert in set theory. $\endgroup$
    – 57Jimmy
    Feb 23, 2018 at 8:42
  • $\begingroup$ I am not sure, but isn't the theorem more focused on uniqueness than on existence? Here we don't need uniqueness, and existence is clear from the definition of $f^n$ (I think) $\endgroup$
    – 57Jimmy
    Feb 23, 2018 at 8:48

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.