2
$\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
2
$\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$ – LE Anh Dung Feb 23 '18 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 '18 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 '18 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$ – LE Anh Dung Feb 23 '18 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 '18 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$ – LE Anh Dung Feb 23 '18 at 8:02
  • $\begingroup$ Yes, it uses the existence part of that theorem. $\endgroup$ – Daniel Schepler Feb 23 '18 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$ – LE Anh Dung Feb 23 '18 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 '18 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 '18 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.