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.

• "Definable by a formula in a theory" is unclear. A formula of first-order arithmetic has a meaning in $\mathbb{N}$ (the natural model) without any reference to a theory. Do you mean to impose that the theory proves the existence of a unique $n$ satisfying the formula, or something of the sort? – Gro-Tsen Feb 21 '17 at 10:59
• I don’t see how this is well-defined either. Even if the theory proves there exists a unique $n$ satisfying the formula, this does not mean that it gives it a definite finite value. For example, consider the formula “$x$ is the length of the shortest proof of contradiction in PA, or $0$ if no such proof exists”. Then PA proves that this formula defines a unique integer, but it does not prove its value to be equal to any fixed numeral. – Emil Jeřábek Feb 21 '17 at 11:35
• @Gro-Tsen,Emil, you are correct. I edited the question and hopefully it'll be more clear to understand now. – Eric Feb 21 '17 at 13:13
• An EXPLICIT definition would be fun! We'd have an ever growing table of records. And more people would bother to think about your strategic question on the whole function. – Włodzimierz Holsztyński Feb 21 '17 at 17:40
• @WłodzimierzHolsztyński, in your case k=33 (every symbol counts if by k you mean the length of the formula), and the number definable by your formula in that length is 81. – Eric Feb 22 '17 at 0:02

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

• Thank you. I edited the question while you were answering it, as you interpret it. – Eric Feb 21 '17 at 13:56
• Yes, I noticed that after having posted. Nice question! I think the busy-beaver analogy may be a fruitul perspective, since the argument that BB is not computable and is Turing equivalent to the halting problem is basically similar to the arguments I gave that your function is not arithmetic and is Turing equivalent to arithmetic truth. – Joel David Hamkins Feb 21 '17 at 14:10
• The point is that the least $n$ for which $\varphi(n)$ holds will be definable. The standard model has definable Skolem functions---there are always definable witnesses for existential assertions, since you can take the least one, and that one is definable by being least. – Joel David Hamkins Feb 21 '17 at 16:28
• We have the same understanding of what it means to be definable. I am saying that if you have an existential assertion $\exists x\varphi(x)$, then the least such $x$, if there is one, is definable. It is the unique $x$ such that $\varphi(x)\wedge \forall y<x\ \neg\varphi(y)$. In this way, we can use your function $\Phi$ to help us bound our existential searches, thereby making them computable. Since it takes a few symbols to say that $x$ is least, in my proof, you have to let $k$ be a little bigger than just what comes after: let it be the size of what it takes to describe the least witness. – Joel David Hamkins Feb 22 '17 at 2:32
• @FFF, Goodstein squence is computable, hence definable in first order arithmetic. It's way below $\Phi$, which is not definable in first order arithmetic. – Eric Feb 22 '17 at 9:52