Quote from Sieg/Parsons commentary on Gödel's Zilsel lecture:
...it has to be clarified how to grasp ... specific countable ordinals ... That can be archieved in the system $S_1$ with function parameters, by considering definable linear orderings $\prec$ of the natural numbers such that, for a definable functional $\Phi$ and for all functions $f$, $S_1$ proves:
$$ \neg { f (\Phi(f) + 1) \prec f (\Phi(f)) }; $$
i.e., $\prec$ is provably well-founded.
I don't understand why this formula expresses well-foundedness of $\prec$. Any help?
Edit: OK, I think I see the light. If $\prec$ is not well-founded, then there is an infinite decreasing sequence of its elements, hence there would be an $f$ such that for any $n$, $f(n+1) \prec f(n)$. But then there cannot be a $\Phi$ satisfying the above condition.