The analytical beaver functions

Rayo's function is based on the language of first-order set theory, which is rather powerful. I think it would be interesting to take a step back to a weaker language: second-order arithmetic.

Let

$\mathcal N$ be the standard model of second order arithmetic. We say that a formula

$\phi$ that takes one argument defines a natural number

$k$ if

$\forall j \in \mathbb N. (j = k \iff \mathcal N \models \phi(j))$ . That is,

$k$ is the unique natural number that satisfies

$\phi$ in the standard model. We define the analytical beaver function

$\operatorname{AnaB}_{\Delta^2_0}(n)$ to be the the largest natural number definable by a formula that is less than

$n$ symbols long plus 1 (or 0 if there is no such number). Since there are only finitely many such formulas, and each formula defines at most one number, this is well defined. As to define a concrete number, we will define the analytical beaver number to be

$\operatorname{AnaB}_{\Delta^2_0}(10^{100})$ . Now, you may be wondering what

$\Delta^2_0$ is doing there? Well, that symbol denotes the set of all formulas in the language of second order arithmetic. In general, we define

$\operatorname{AnaB}_S(n)$ to be the largest natural number definable definable by a formula in the set

$S$ that is less than

$n$ symbols plus 1 (or 0 if there is no such number). Some interesting sets of formulas are those in the analytical hierarchy (which includes the arithmetical hierarchy). We will also define the combination beaver

$\operatorname{AnaB}_{S_1, S_2, \dots, S_q}(n)$ to be the largest natural number definable definable by a formula from each of the sets

$S_1, S_2, \dots, S_q$ that is less than

$n$ symbols plus 1 (or 0 if there is no such number). By convention, we define the analytical beaver for a

$\Delta$ level to be the combination of the corresponding

$\Sigma$ and

$\Pi$ levels. For example,

$\operatorname{AnaB}_{\Delta^0_4} := \operatorname{AnaB}_{\Sigma^0_4, \Pi^0_4}$ .

We can also consider analytical beavers based on expansions of second order arithmetic. By convention, the analytical beaver of a relativized level of the hierarchy is defined this way.

Question: It is clear that

$\operatorname{AnaB}_{\Delta^2_0}$ is not in the analytical hierarchy itself. However,

$\operatorname{AnaB}_S$ is, for any other

$S$ in the analytical hierarchy. Where do such

$\operatorname{AnaB}_S$ fall in the hierarchy? We know they would not fall in

$S$ , for example.