$\newcommand\toward{\rightharpoonup}$It would help me to understand something in a current research project if someone could provide an example of directed graph $\langle G,\toward\rangle$ with the following properties
- The graph is connected.
- Every node $x$ points at exactly one parent node $y$, via $x\toward y$. Thus, the underlying relation is a tree.
- The relation $\toward$ is well-founded, so that every nonempty subset $X\subset G$ has an $\toward$-minimal element $x\in X$, meaning that $y \not\!\toward x$ for all $y\in X$. In the presence of DC, this is equivalent to saying that there is no infinitely receding sequence $\cdots\toward x_3\toward x_2\toward x_1\toward x_0$.
- Finally, the key part, there are two elements $a$ and $b$ with $a\toward b$, such that $a$ and $b$ realize exactly the same type in $\langle G,\toward\rangle$. That is, $G\models\varphi(a)\leftrightarrow\varphi(b)$ for any assertion $\varphi$ in the digraph language.
Can this happen?
Note that there can be no automorphism mapping $b$ to $a$, for in this case, we could iterate it to produce a receding chain, contrary to the well-founded hypothesis.
Also, since $b$ is not minimal, neither can $a$ be minimal, and if there is a path from a minimal element to $a$ of length $k$, then there is one to $b$ of length $k+1$, and so if the types are the same, there is a path to $a$ of length $k+1$, and so on. So both $a$ and $b$ will have infinite rank with respect to the well-founded relation. And I think one can carry that reasoning much further.
In my actual application, there is a lot more structure, and I consider $a$ and $b$ to realize the same assertions in a much stronger language, one that includes second-order logic and more. But I realized I don't have a complete grasp even on this "easy" case. What are types like in these well-founded digraph trees?