Are these two notions of weak well-foundedness equivalent?

Question

Background (optional): I have a state transition system $Q$ with two "kinds" of transitions: progress-making ($\delta_P : Q \times \Sigma \rightarrow Q$) and non-progress making ($\delta_N : Q \times \Sigma \rightarrow Q$). I want to say that it is not possible for the system to undergo a progress making transition infinitely many times without ever terminating. However, in my case, it would be much simpler to deal with a well-founded relation on an encoding of the state which always decreases when progress is made.

I have simplified the mathematical content of my situation into the following: suppose we have two relations on $Q$: $\approx$ and $>$ (despite the notation, they are not necessarily transitive, reflexive, etc.). Are the following two equivalent:

1. There is no infinite sequence $q_1 > q_2 \approx q_3 \approx q_4 > q_5 > \cdots$ where each $q_{i+1}$ is either $q_i > q_{i+1}$ or $q_i \approx q_{i+1}$, and $q_i > q_{i+1}$ infinitely often.

2. There is some function $f : Q \rightarrow R$ and a relation $>_R$ on $R$ such that

   • $>_R$ is well-founded in the usual sense
   • for any $q_a > q_b$, we have $f(q_a) >_R f(q_b)$
   • for any $q_a \approx q_b$, either $f(q_a) >_R f(q_b)$ or $f(q_a) = f(q_b)$

It is clear that (2) implies (1), since any sequence $q_1 > q_2 \approx q_3 > \cdots$ would satisfy $f(q_1) >_R f(q_2) = f(q_3) >_R \cdots$. Even after contracting the equalities, which are a subset of the relations that were originally $\approx$, we are still left with an infinite decreasing sequence, contradicting $>_R$'s well-foundedness.

On the other hand, I'm not sure that (1) implies (2). In the third bullet point, if we disallow $f(q_a) >_R f(q_b)$, for example, then $R$ is essentially forced to be $Q/\approx$, and there is the following counter example:

*     * --> *
|     |     |       ...
V     V     V 
* --> *     * --> *

In the example above, all the vertical arrows are part of the $\approx$ relation, while the horizontal arrows are part of the $>$ relation. These relations satisfy (1), because the maximum length of any $>,\approx$-path is 3, but if we merged the top and bottom lines, there would be an infinite descending sequence so we cannot have $R = Q/\approx$. However, it is not a counterexample because we can instead choose $R = Q$ and let $>_R$ be the union of the two relations $>$ and $\approx$.

If (1) is indeed weaker than (2), is it possible to modify the third bullet point in a natural way so that they become equivalent?

Answer 1

It seems to me that (1) implies (2).

Suppose $\approx$ and $\gt$ are binary relations on a set $Q$ such that (1) holds. For $x,y\in Q$ define $x\succ y$ to mean that for some $n\ge0$ there are $x_1,\dots,x_n\in Q$ such that $$x\approx x_1\approx x_2\approx\cdots\approx x_n\gt x_{n+1}.$$

For ordinal $\alpha$ define a set $Q_\alpha\subseteq Q$ by transfinite recursion: $$Q_\alpha=\left\{x\in Q:\forall y\in Q\left[x\succ y\implies y\in\bigcup_{\beta\lt\alpha}Q_\beta\right]\right\}.$$ Plainly $\gamma\lt\alpha\implies Q_\gamma\subseteq Q_\alpha$. Moreover, (1) implies that $Q_\lambda=Q$ for some ordinal $\lambda$, so we can define $f:Q\to\lambda+1$ by setting $f(x)=\min\{\alpha:x\in Q_\alpha\}$.

Now $x\gt y\implies x\succ y\implies f(x)\gt f(y)$, and $x\approx y\implies f(x)\ge f(y)$.