[19] We define a variant of the busy beaver function BB(n)

in Exercise 1.7.19 on page 45. Let BC(n) be the largest natural number m such that C(m) ≤ n. Let φ1, φ2,... be the standard effective enumeration of partial computable functions.

(a) Show that BC(n) > φ(n), where φ = φk, for all n ≥ C(k) − 4 log n.

(b) Show that BC(n) is not a computable function.

(c) Show that the incomputability of BC(n) can be used to prove the unsolvability of the halting problem (Lemma 1.7.5 on page 34) and vice versa.

(d) Let F be an axiomatizable sound formal theory that can be described completely (axioms, inference rules, . . . ) in m bits. Show that no provable true statement in F asserts “BC(n) = x” for BC(n) = x with any n>m + O(1).
Comments. Hint for Item (a): C(φ(n)) ≤ C(k, n)+O(1). Then, C(φ(n)) ≤
n − log n. Hence, BC(n) > φ(n). Hint for Item (b): It grows faster than any computable function. Hint for Item (c): If the halting problem were solvable, we could compute BC(n) from the outputs of all halting programs of length at most n. Conversely, every halting program p halts within BC(n) steps, for n ≥ l(p) + O(1). So computability of BC implies the solvability of the halting problem. This exercise is an application of Theorem 2.3.1, Item (iii). In fact, BC(n) is some sort of inverse function of m(n), the greatest monotonic increasing function bounding C(n) from below. Source: [G.J. Chaitin, pp. 108–111 in: Open Problems in Communication and Computation, T.M. Cover, B. Gopinath, eds., Springer-Verlag, 1988].