Choice needed in equiv. of two definitions of well-founded set

Question

(old question: the usual proof of Well-founded induction uses Dependent choice. Is it necessary? I've heard that Well-founded induction is equivalent to dependent choice - I highly doubt that, but I couldn't find any references.)

EDIT: Hagen's answer suggests, that I have a different definition of well-founded set and my question is - at the end of the day - about their equivalence. I should've been more precise in my original question, let me correct that.

We work with a set with a binary relation $(X, R)$, let's assume $R$ is irreflexive for it makes things technically smoother.

(Hagen's) $(X, R)$ is well-founded, when every nonempty subset $S\subseteq X$ has a minimal element, meaning an element $m$ such that there's no $s\in S$ satisfying $sRm$.

(Mine) $(X, R)$ is well-founded, when there's no infinite sequence $(a_i)_{i=0}^{\infty}$ such that $$\dots Ra_1Ra_0.$$

To get from the first to the second is obvious, the first take on the other direction uses dependent choice. This really should be the question:

How much choice do we need to make these definitions equivalent? Is the full dependent choice necessary?

Just for the completeness, the well-founded induction: Let $P$ be a property on elements of a well-founded set $(X,R)$, then $$\forall x.(\forall y.(yRx\implies P(y))\implies P(x)) \implies \forall x.P(x).$$ This is a very general version of induction principle, generalizing transfinite or structural induction.

Answer 1

The assumption that those two definitions of "well-founded" are equivalent implies the axiom of dependent choice. I will show the contrapositive; assuming the failure of dependent choice, there is a partially ordered set which is well-founded in one sense but not the other.

Let $X$ be a nonempty set and let $R$ be a binary relation on $X$ such that, for each $a\in X,$ there exists $b\in X$ such that $a\ R\ b;$ and suppose there is no infinite sequence $a_1\ R\ a_2\ R\ a_3\ R\cdots.$

Let $P$ the the set of all finite sequences $(a_1,a_2,\dots,a_m)$ such that $a_1\ R\ a_2\ R\cdots R\ a_m.$

For $(a_1,a_2,\dots,a_m),\ (b_1,b_2,\dots b_n)\in P,$ define $(b_1,b_2,\dots,b_n)\lt(a_1,a_2,\dots,a_m)$ to mean that $(b_1,b_2,\dots,b_n)$ is a proper end-extension of $(a_1,a_2,\dots,a_m),$ i.e., $m\lt n$ and $(a_1,a_2,\dots,a_m)=(b_1,b_2,\dots,b_m).$

Then $P$ is nonempty and has no minimal element, but it contains no strictly decreasing infinite sequence.

Answer 2

Recall that we define a set $X$ to be well-founded by the binary relation $R$ if every non-empty subset $Y\subset X$ has an $R$-minimal element, i.e., there exists $a\in Y$ such that $R^{-1}a\cap Y=\emptyset$. (Here, we write $R^{-1}a:=\{\,x\in X\mid xRa\,\}$).

The principle of well-founded induction states: Let $X$ be well-founded by $R$ and let $Z\subseteq X$ be a set with $$\forall a\in X\colon (R^{-1}a\subseteq Z\to a\in Z).$$ Then $Z=X$.

The proof that this principle is valid is simple: Let $Y=X\setminus Z$. Assume $Y\ne \emptyset$. Then $Y$ has an $R$-minimal element $a$. But $R^{-1}a\cap Y=\emptyset$ means $R^{-1}a\subseteq Z$, hence $a\in Z$, contradicting $a\in Y$. We conclude that $Y=\emptyset$, $Z=X$.

This does not require choice (even if it looks as if we "pick" some $a$ as $R$-minimal element).

Answer 3

I think you may be thinking of the following theorem:

A relation $R$ on a set $A$ is well-founded if and only if there is no infinite descending chain $\dots a_n \,R\, a_{n-1} \,R\, a_{n-2} \,R\,\dots \,R\,a_2 \,R\, a_1 \,R\, a_0$ — in other words, iff there is no function $f\colon\omega\to A$ such that for all $n\lt\omega,$ $f(n+1)\,R\,f(n).$

The implication from right to left requires the axiom of dependent choices (DC), although the implication from left to right is provable in ZF alone.