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?
 A: 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.
