  We show some incompleteness results a la Chaitin using the busy beaver
functions. Then, with the help of ordinal logics, we show how to obtain a
theory in which the values of the busy beaver functions can be provably
established and use this to reveal a structure on the provability of the values
of these functions.
