A well-founded relation on set $X$ is a binary relation $R$ such that for all non-empty $S \subseteq X$ $$\exists m \in S\colon \forall s \in S\colon \neg(s\;R\;m).$$
A relation is well-founded when it contains no infinite descending chains.
I have read that for a finite directed acyclic graph (DAG) following relation is well-founded: $$a\;R\;b \text{ if and only if there is an edge from } a \text{ to } b. $$
It is clear that $R$ is not well-founded for an arbitrary DAG with infinite nodes. Consider the simple DAG $X=\{x_i\colon i \in \mathbb{N}\}$: $\forall i \in \mathbb{N}\colon x_{i+1} \to x_{i}.$ Since there is an infinite descending chain $R$ is not well-founded.
My question: Are the following conditions on the DAG $X$ sufficient for $R$ to be well-founded?
- there is an unique root $u \in X$, such that for all $a \in X$ there is a path from $u$ to $a$ and there is no path from $a$ to $u$.
- for all $a \in X$ there are only finitely many $b \in X\colon a\;R\;b$
- for all $b \in X$ there are only finitely many $a \in X\colon a\;R\;b$
- for all $a,b\in X$: every path from $a$ to $b$ has finite length.
Concretely, consider following DAG: $X = \{n_i\colon i \in \mathbb{N}\} \cup \{m_i\colon i \in \mathbb{N}\}$. For all $i \in \mathbb{N}$ we have the edges $n_i \to n_{i+1}$, $m_{i+1} \to m_i$, $n_i \to m_i$. $X$ fulfills the above conditions with $u=n_1$. Is $R$ well-founded on $X$?
EDIT: the concrete example is not well-founded since $m_{i+1} \to m_i$ is an infinite descending chain. Can we add assumptions on the DAG to make $R$ well-founded?
EDIT2: as mentioned by Misha, there are no infinite paths in graph theory. I guess with what I had in mind the condition can be written as:
- for all $a \in X$ the following statement is false: $$\forall i \in \mathbb{N}\colon \exists x_i \in X\colon x_{i+1}\;R\;x_i \land x_1\;R\;a$$ But this is precisely the definition of an infinite descending chain. Thus, no other conditions (like an unique root) are necessary.
