I try to understand the Löb-Wainer-hierarchy and one definition just doesn't open. I hope someone could clarify this to me.
A fundamental sequence to limit ordinal $\alpha$ is $\omega$-sequence $\{\alpha_i\}_{i\in\mathbb{N}}$ of ordinals such that for each $i\in\mathbb{N}$ we have $\alpha_i<\alpha_{i+1}<\alpha$ and $\lim_{i\in\mathbb{N}}\alpha_i=\alpha$.
For each countable limit ordinal $\beta$, let $\{\beta\}(i)$,$i\in\mathbb{N}$ denote a arbitrarily chosen fixed fundamental sequence to $\beta$. Define now $F_\alpha^n$ such that
- $F_0^n(x)=(n+1)(x+1)$
- $F_{\alpha+1}^0(x)=F_{\alpha}^x(x)$
- $F_\beta^0(x)=F^0_{\{\beta\}(x)}(\varrho_\beta(x))$ where $\beta$ is a limit ordinal
- $F_\gamma^{n+1}(x)=F_\gamma^0(F_\gamma^n(x)),\gamma\neq 0.$
Here for limit ordinal $\beta$ we have:
- $\varrho_\beta(0)=0$,
- $\varrho_\beta(m+1)=\mu_z(z>\varrho_\beta(m)\ \&\ (i)_{\leq m}(F_{\{\beta\}(m+1)}^0(z)>F_{\{\beta\}(i)}(z)))$.
I don't understand the definition of $F_\beta^0(x)$. It seems a sort of diagonalisation process (does it?) but the notation with a weak understanding of ordinal numbers (I'm working on the latter at the very moment) are giving me hard time. I guess $\mu_z$ refers to smallest $z$ such this-and-that, but I don't quite understand the overall construction.
What the definition says?
In the second page is says that $\mu_z(\ldots)$ is the least $z$ such that $\ldots$ (i.e. the "least ..." operator)
As remarked by Brian M. Scott and Andres Caicedo $(i)_{\le m}$ it the set $\{0,\ldots,m\}$.
The definition is pretty much straightforward in the non-limit cases, so we only need to take care of the $\beta$ limit case.
Indeed as noted in the paper, and in your question, this is a form of diagonalization.
$\varrho_\beta$ is defined to return some "quickly" increasing sequence, so we could ensure some uniform behaviour with respect to the fundamental sequence that we've chosen in advance.
We want $\varrho_\beta(m+1)$ (assuming $x\neq 0$) to be a number $z$ such that:
Taking the least $z$ with these properties is only a simple way of defining a choice function. It might be the case that the least-ness of $z$ is used later on, though.
Now, from this we can define $F^0_\beta(x)$. It is $F^0_{\{\beta\}(x)}(x)$. This ensures that $F^0_\beta$ is in a sense some sort of limit of the $F^0_{\{\beta\}(i)}$, which is what is usually wanted from transfinite sequences.
If you have further questions, I'd be glad to try and answer them.