Proof that Axiom of Dependent Choices is equivalent to a statement about posets I'm trying to show that the Axiom of Dependent Choices (DC) is equivalent to the following statement about posets:
A partial order is well-founded iff it has no infinite descending chains.
I understand how DC implies the statement about posets, but I am not sure how to show the reverse implication. How do I do it?
Note that I am trying to do this assuming ZF.
Here I define DC by the following:
Let $A$ be a set. Suppose $a\in A$, and $R$ is a relation on $A$ such that $(\forall x\in A)(\exists y\in A)$ such that $xRy$. Then there exists a function $f:\Bbb N \rightarrow A$ such that $f(0) = a$ and $(\forall n \in \Bbb N)[f(n)Rf(n+1)]$
 A: The thing to remember about these kind of proofs is that the failure of the choice principle usually means that there is some object satisfying the hypothesis, but not the conclusion. From that object we should find a counterexample to the equivalence statement (in this case about well-founded posets).
The failure of the version of $\sf DC$ given here means that there is some non-empty set $A$ and a relation $R$ whose domain is $A$; but there is no function from $\Bbb N$ to $A$ which gives us an $R$-sequene.
But now that by [a choice-free] induction we can still show that there are arbitrarily long finite $R$-sequences. If $a_0,\ldots,a_n$ is an $R$-sequence (namely $a_i\mathrel{R}a_{i+1}$), then by the fact $a_n$ is in the domain of $R$, there is some $b\in A$ such that $a_n\mathrel{R}b$. Pick such $b$ to be $a_{n+1}$, and this shows that if there are sequences of length $n$, there are sequences of length $n+1$.
Of course, moving from the above induction to a full-blown $\Bbb N$-long sequence is exactly what $\sf DC$ guarantees. And we assumed that $R$ was a counterexample to that! So there is no such sequence.
Therefore, look at the collections $T$ of finite $R$-sequences, ordered by reverse end-extension (namely, $\vec a\leq_T\vec b$ if $\vec b$ is an initial segment of $\vec a$). And show that $T$ is indeed a counterexample to the equivalence about posets.
