Grounded for Math

In this post, I would like to briefly define a googological function designed to be a computable variant of the Busy Beaver function: the Cautious Cat function. \(CC(n)\) is the maximum number of \(1\)s written by any Turing machine whose halting can be proven in \(ZFC\) using at most \(n\) symbols.

Recently, I've become interested in googology. The Busy Beaver function, \(BB(n)\), has been of particular interest. It is defined as the maximum number of \(1\)s written by any halting \(n\)-state Turing machine. A natural extension of the Busy Beaver function is to replace Turing machines with a more powerful construct, such as augmenting a Turing machine with a halting oracle. I develop such an extension below.