# Higher-order Busy Beaver functions and the language of first-order set theory

I have a question, but before asking this question, it is required to ask the preliminary question: is it possible to define a particular higher-order Busy Beaver function by a formula (of finite length) in the language of first-order set theory (based on ZFC)?

If yes, then suppose we have defined (by two formulas) two different Busy Beaver functions $f(n) = BB_{\alpha}(n)$ and $g(n) = BB_{\beta}(n)$, where $\alpha$ and $\beta$ are two different ordinal numbers (ordinal notations) such that $f(n)$ dominates $g(n)$, that is, there exists some number $x$ such that $f(n) > g(n)$ for all $n \geq x$.

The main question: does there exist a proof (of finite length) in ZFC that $f(n)$ dominates $g(n)$?

EDIT

Higher-order Busy Beaver function can be defined as the maximum number of non-blank cells that any halting $n$-state $\alpha$-th-order Turing machine can output (after halting), assuming that the input is infinitely blank. The description of $\alpha$-th-order Turing machines can be found, for example, here:

With the help of ordinal numbers we can continue this method further, and we could define $\text{TM}_\alpha$ for any countable ordinal number $\alpha$. However, due to the increasing complexity of encodings of high order oracles this becomes very impractical to work with, which is why mathematicians have been considering different ways of extending the notion of computability.

(These functions are also mentioned in this question).

NOTE

In any case, the exact definition of any particular higher-order Busy Beaver function depends on the model of Turing machines, the oracle that these machines are equipped with etc. This question is about the definability of such functions by formulas in the language of first-order set theory, and the provability (by a formula of finite length in the same language) that a particular function dominates another function. That is, if we have two formulas that define two different functions $f$ and $g$, then what do we need to prove that $f$ dominates $g$? Or maybe proof of domination is not always possible?

• What is a Busy Beaver function? – Taroccoesbrocco Sep 19 '18 at 12:58
• @Taroccoesbrocco en.wikipedia.org/wiki/… – Alex Kruckman Sep 19 '18 at 13:42
• What exactly does "higher-order Busy Beaver function" mean? (And as per usual, whatever it is will probably be indexed by ordinal notations, not ordinals ...) – Noah Schweber Sep 19 '18 at 14:00
• Here are some things I do not understand about the question: You say that your functions are defined by a formula. So, I would expect that we would see functions $f_\varphi$, where $\varphi$ is a formula. Instead, you have $f_\alpha$, where $\alpha$ is an ordinal. How can this be? Perhaps you mean that $\alpha$ is definable, and by $f_\alpha$ you really mean $f_{\varphi_\alpha}$, where $\varphi_\alpha$ is a formula in one free variable defining $\alpha$ (in what theory?). Is this independent of the defining formula, as the notation suggest? Or maybe you mean something else entirely. – Andrés E. Caicedo Sep 19 '18 at 17:01
• Anyway, I do not understand what a "higher-order Busy Beaver" is. This would suggest the existence of "higher-order Turing machines". What do you mean by that? Also, you write that these functions are defined "by the formula ...". Do you perhaps mean "by a formula..." or did you forget to include the specific formula you have in mind? – Andrés E. Caicedo Sep 19 '18 at 17:38

Your question as it stands is quite unclear, but let me take a stab at it; based on your previous questions, if nothing else I think you'll find this interesting.

The simplest interpretation of your question is to look for an analogue of the Busy Beaver function for iterates of the Turing jump through the ordinals. Such a thing does exist, although - as usual, and along similar lines to some of your previous questions - we have to index by ordinal notations instead of ordinals per se, and we run into trouble when we try to continue past the computable ordinals (see chapter $1$ of Sacks' book for the relevant background; on the other hand, see Hodes' paper on mastercodes for ideas on how to go even further):

• For $l$ a notation for a computable limit ordinal, we get a sequence $(n_i)_{i\in\omega}$ of notations forming a canonical sequence for $\vert l\vert_\mathcal{O}$ (where "$\vert k\vert_\mathcal{O}$" denotes the ordinal $k$ is a notation for). The $l$th Busy Beaver function, $BB_l$, is then defined by

$$BB_l(x)=1+\sum_{i\le x}BB_{n_i}(x).$$

• For $m$ a notation for a successor ordinal, we let $n$ be the canonical "predecessor notation" of $m$, and define $BB_m$ as the sum of $BB_n$ and the usual Busy Beaver function with oracle $BB_n$.

The $\mathcal{O}$-indexed "hierarchy" so defined has a number of nice properties. in particular, there is also a very tight connection with iterates of the Turing jump (as alluded to above): $BB_k$ is Turing-equivalent to $0^{(\vert k\vert_\mathcal{O})}$ for every notation $k$.

It turns out that this computation power carries over to domination: given any function $f$ dominating a Busy Beaver function with index a notation for a computable ordinal $\alpha$, we have $f\ge_T0^{(\alpha)}$.

Surprisingly, the degree $0^{(\alpha)}$ makes sense for $\alpha$ a computable ordinal, not just a notation - if $i,j$ are notations for computable ordinals, then the potentially-different sets $0^{(\vert i\vert_\mathcal{O})}$ and $0^{(\vert j\vert_\mathcal{O})}$ are of equal Turing degree.

This, in turn, lets us prove the desired domination result that $$\vert i\vert_\mathcal{O}<\vert j\vert_\mathcal{O}\implies BB_i\prec BB_j,$$ where "$\prec$" means "dominates: we argue by induction that for any notation $k$ the higher Busy Beaver function $BB_k$ dominates every function computable from $0^{(\alpha)}$ for any $\alpha<\vert k\vert_\mathcal{O}$.

This naturally suggests the question of what sets can be computed from fast-enough functions. A beautiful theorem of Solovay says that basically the situation above is the only way this can happen:

Given a set $A$, the following are equivalent: $(i)$ $A$ is hyperarithmetic, $(ii)$ there is some function $f$ such that every function dominating $f$ computes $A$.

The observation we've made about the $BB_i$s forms the $(i)$-to-$(ii)$ direction (the other direction requires a nice forcing argument). See Peter Gerdes' thesis for further work on the topic.

• But can we define such functions by formulas in the language of FOST? And if yes, and we are given two formulas that define two functions $f$ and $g$ such that $f$ dominates $g$, is there a proof (of finite length) that $f$ dominates $g$? – lyrically wicked Sep 20 '18 at 4:45
• @lyricallywicked The definitions/arguments I've given above go through without a problem in ZFC; what's the hitch? Remember that set theory definitely supports definition by transfinite recursion, which is exactly what's going on here. (In fact, everything above can be carried out just in the vastly-vastly-weaker system ATR$_0$.) – Noah Schweber Sep 20 '18 at 17:46