Take the 2-minute tour ×
Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.

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

  1. $F_0^n(x)=(n+1)(x+1)$
  2. $F_{\alpha+1}^0(x)=F_{\alpha}^x(x)$
  3. $F_\beta^0(x)=F^0_{\{\beta\}(x)}(\varrho_\beta(x))$ where $\beta$ is a limit ordinal
  4. $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?

share|improve this question
Where did you find this definitions? –  Asaf Karagila Sep 6 '11 at 15:02
I cannot find the paper (not even behind a paywall), however the definition of $\varrho$ is very blurred to me. By $\&$ do you mean $\land$? What do you mean by $(i)_{\le m+1}$? Etc. etc. Could you please turn that into a list as well, may ease the readability. –  Asaf Karagila Sep 6 '11 at 15:16
The definition of $\varrho$ is corrected in the second link. I have edited that into your post. –  Asaf Karagila Sep 6 '11 at 16:29
Look again. It appears on the second paper as a correction. –  Asaf Karagila Sep 6 '11 at 16:53
@Asaf: Since ‘$(x)$’ is another notation for ‘$\forall x$’, I suspect that ‘$(i)_{\le m+1}$’ is ‘$\forall i \le {m+1}$’; it makes sense in this context. –  Brian M. Scott Sep 6 '11 at 22:03

1 Answer 1

up vote 2 down vote accepted

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:

  • $z>\varrho_\beta(m)$;
  • For all $i<m$ we have that $F^0_{\{\beta\}(m+1)}(z)>F^0_{\{\beta\}(i)}(z)$, which by previous definition means $F^z_{\{\beta\}(m)}(z)>F^z_{\{\beta\}(i-1)}(z)$, of course for $i>0$.

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.

share|improve this answer
Asaf: $(i)_{\le m}$ means $\forall i\le m$. It used to be standard (but ugly) notation in some places. –  Andres Caicedo Sep 7 '11 at 4:38
@Andres: Thanks, Brian M. Scott remarked that on the main question already. :-) –  Asaf Karagila Sep 7 '11 at 5:52

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.