Let me interpret the question asking about what is true in the
standard model $\langle\newcommand\N{\mathbb{N}}\N,+,\cdot,0,1,<\rangle$, which
avoids the non-absoluteness issues mentioned in the comments. In
this case, the definition is well-defined and sensible. We define that $\Phi(n)$
is the largest number $m$ definable in the structure by a formula
of length at most $n$.

I view the topic here as an analogue of the busy-beaver problem for arithmetic truth.

**Theorem.** The function $\Phi(n)$ eventually dominates every
arithmetically definable function.

**Proof.** Suppose that $f:\N\to\N$ is an arithmetically definable
function, so that the relation $f(x)=y$ is definable in the
structure by some formula $\varphi(x,y)$.

Notice that with the powers of two, we can easily define large
numbers with comparatively small formulas. For example, $2^n$ is
definable by a formula of size $n+c$ for some constant $c$. Put
differently, and by iterating this, for any sufficiently large $k$
we can define a number $k^+$ larger than $k$ with a formula smaller than
$\log(\log(k))$.

Therefore, if $k$ is very large with respect to these constants and
the size of the definition of $f$, then we can define $\max_{x\leq
k^+}f(x)$ using a formula of size less than $k$. Thus,
$f(k)\leq\Phi(k)$, as desired. **QED**

Meanwhile, the function is Turing computable from $0^{(\omega)}$,
the $\omega$-jump of the halting problem, since that oracle is able
to compute first-order arithmetic truth. So you have a function
that is not computable from any finite jump $0^{(n)}$, but it is
computable from the $\omega$-jump.

I claim that the converse is also true. Your function is
essentially equivalent to arithmetic truth.

**Theorem.** The function $\Phi$ you have defined is Turing
equivalent to an oracle for arithmetic truth.

**Proof.** I've already pointed out that $\Phi$ is computable from
arithmetic truth.

Conversely, suppose that we have an oracle for your function
$\Phi$. I claim that we can compute arithmetic truth. The reason is
that we shall be able to compute Skolem witnesses. For example, to
compute the halting problem for a program $p$ on input $n$, we need
only express the formula "$y$ is the length of the compution of $p$
on $n$" and then apply the function $\Phi$ to get an upper bound
for the length of the computation. If the program doesn't halt by
then, then it won't ever halt, since the length of the computation
is definable.

We can systematically iterate this idea up the arithmetic
hierarchy. Namely, working from the atomic formulas up, every
assertion $\exists x\
\varphi(x,\dots)$ is replaced with the assertion $\exists
x<\Phi(k)\
\varphi(x,\dots)$, where $k$ is the size of the expression
appearing to the right. By using a term for $\Phi(k)$, and iteratively applying this procedure to higher quantifiers, in the case that they were nested, we thereby get a computable expression that is equivalent to the original
formula. In this way, arithmetic truth reduces to a computable
process with the function $\Phi$. **QED**

4more comments