The set of largest numbers definable by formulas in different lengths Let $n=\phi(l)$ to be the largest number definable by a first order arithmetic formula $f(x)$ having length at most $l$. By "$n$ is definable by formula $f(x)$" I mean $\mathcal{N}\vDash f(a)$ iff $a=n$, where $\mathcal{N}$ is a structure of natural numbers with the standard interpretation (if it's necessary to be specific, think of it as $\mathcal{N}=\{\mathbb{N}|+,*,1\}$). This function  is well-defined. My question is, how fast does it grow? Can we put it in some appropriate framework and say something more about it?  
One observation I can make is that no first order arithmetic formula defines the function $n=\phi(l)$, i.e., there exists no formula $\psi(x,y)$ such that $\mathcal{N}\vDash \psi(n,l)$ iff $n=\phi(l)$. This means the set $\{n,l|n=\phi(l)\}$ is beyond arithmetic hierarchy, where I have only very limited knowledge.  

Edit: Issues mentioned in the comments are addressed.
 A: 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
