Question: What are some natural examples of recursive pseudowellorderings?
By natural, I mean in the style of reasonable ordinal notation systems as opposed to dependent on a Gödel numbering or an enumeration of Turing machines.
A recursive pseudowellordering is a non-well-founded recursive linear order that does not have hyperarithmetic infinite descending sequences. Its significance is that its initial well-founded segment has order type $ω_1^{\mathrm{CK}}$, which is above all recursive ordinals. In a way, it acts as a universal ordinal notation system because we can specify an initial well-founded segment and get an ordinal notation system with arbitrary recursive length, with the notation of an ordinal independent of the segment used (and unlike Kleene's $\mathcal{O}$, a recursive pseudowellordering is recursive). (However, my guess is that it will be impractical, and in particular that if $α$ is too large, its notation size will in a sense be related to a fast-growing function based on $α$.)
Using Gödel numbering, here is an example recursive pseudo-well-ordering (quoted from a Wikipedia article but originally written by me):
Let S be ATR0 or another recursively axiomatizable theory that has an $ω$-model but no hyperarithmetical $ω$-models, and (if needed) conservatively extend $S$ with Skolem functions. Let $T$ be the tree of (essentially) finite partial $ω$-models of $S$: A sequence of natural numbers $x_1,x_2,...,x_n$ is in $T$ iff $S$ plus $∃m \, φ(m) ⇒ φ(x_{⌈φ⌉})$ for the first $n$ formulas $φ$ with one free numeric variable ($⌈φ⌉$ is the Gödel number) has no inconsistency proof shorter than $n$. Then the Kleene–Brouwer order of $T$ is a recursive pseudowellordering.
In a sense, we can almost get natural recursive pseudowellorderings. Given a typical natural theory $S$ and a reasonable ordinal notation system $A$ for its $Π^1_1$ proof ordinal, $S$ is consistent with $A$ being a recursive pseudowellordering. The reason is that well-foundness of $A$ will typically be unprovable even in $S$ augmented with all true $Σ^1_1$ statements, and nonexistence of hyperarithmetical infinite descending paths is $Σ^1_1$. This construction (and its conjectured extension to nonrecursive ordinals) is a key building block for the question Ordinal analysis and nonrecursive ordinals.
Thus, we have a dichotomy. We have reasonable recursive ordinal notation systems for (somewhat) strong theories (which consistent with those theories are pseudowellorderings), but unless this question is answered, no known actual natural recursive pseudowellorderings. I would argue that this asymmetry is fundamental, and is related to that if a large cardinal axiom does not appear to have an easy inconsistency, then it is likely $Π^1_1$ sound (and more): If something natural looks like a well-ordering, then typically it either is a well-ordering or has a simple infinite descending path. However, answers to this question may provide a cautionary tale on this point as well as insights into recursion theory.
