While studying theoretical computer science the following problem about ordinals came up:
Define the operations of multiplication $(n*m)$, exponentiation $(n^m)$ and integer part of the logarithm in base 2 $(\lfloor log_2 n \rfloor)$ over the ordinals (successor).
I think I could define multiplication and exponentiation in a way similar to what we do for the sum. However, I would like some help defining the integer part of the logarithm in base 2.
Having previously defined the sum of ordinals as:
$\alpha + 0 = \alpha$
$\alpha + (\beta+1) = (\alpha + \beta) + 1$
$\alpha + \beta = sup\{\alpha + \delta \ | \ \delta < \beta\} $ if $\beta$ is a limit ordinal.
multiplication was defined as:
$\alpha * 0 = 0$
$\alpha * (\beta+1) = (\alpha * \beta) + \alpha$
$\alpha * \beta = sup\{\alpha * \delta \ | \ \delta < \beta\} $ if $\beta$ is a limit ordinal.
and exponentiation was defined as:
$\alpha^0 = 1$
$\alpha^{(\beta+1)} = (\alpha^\beta) * \alpha$
$\alpha^\beta = sup\{\alpha^\delta \ | \ \delta < \beta\} $ if $\beta$ is a limit ordinal.
Can anyone give me a hint on how to define $\lfloor log_2 n \rfloor$? I have a guess that I may need to start by defining $\lfloor \frac{n}{2} \rfloor$, but I am not sure how I would do that. Thanks in advance.
@aschepler gave me the hint I was looking for in his comment, which I am writing as an answer so I can accept it. There is no need to consider $\lfloor \frac{n}{2} \rfloor$. Instead, since we have already defined exponentiation, we should consider the set $\{\beta \ | \ 2^\beta \leq n \}$.