# Finite verification for theorems due to Busy Beaver numbers

I recently learned about the Busy Beaver function, and a formulation of it that essentially tells us if a turing machine of $$n$$ states takes over $$BB(n)$$ steps, it will never halt.

One consequence I thought of this, is that if we're able to construct say a turing machine that checks that every even number one by one is a sum of two primes, we would only need to run this machine for a finite number of steps before being sure of Goldbach's conjecture.

Because of this, we can write the following statement: $$\exists N. (\text{All even numbers greater than 2 and \leq N are a sum of two primes} \implies \text{All even numbers greater than two are a sum of two primes})$$ This seems like a fairly nontrivial statement, and could be replicated with other important theorems as well. My question is, is something like this provable without delving into the theory of computation (i.e with just properties of first order logic or similar).

• Here's maybe a different way to think about things, that shows this isn't really about Turing machines or Goldbach's conjecture or whatever. Suppose we have some logical formalism where mathematical statements and their proofs can be represented by finite strings. For each $n$, there must be some $N$, so that all statements of length $n$ have either a proof of length $N$ or a disproof of length $N$, or are independent of our formal system. If we knew what this $N$ was in terms of $n$ we could simply check all proofs/disproofs of our statement, which is a "finite" and "automatic" thing to do. Commented Jul 13 at 16:44
• I think it is better to ask for a constructive proof of your statement, since non-constructive proofs trivialize matters. Also, I think one can even present matters in classical $\sf PA$, we describe $\sf GC_n$ up to metatheoretic $n$ to mean every even number up to $\sf SSS....S_n(0)$ that is greater than $4$ is the sum of two even numbers. Commented Jul 13 at 21:54
• Continuation... This way we assure matters be confined to standard naturals. Then ask if $\sf PA$ can prove an inference rule $I_n$ for some metatheoretic $n$, where $I_n$ is the rule: $${\sf GC}_n \\ \overline{\forall x \in N: {\sf GC}(x)}$$ Where ${\sf GC}(x)$ is the usual statement of Goldbach's conjecture (here $x$ range over all naturals standard and non-standard). Commented Jul 13 at 21:54
• I think the statement in the opening post is trivially true: If Goldbach's Conjecture ist true, any N works. If the Conjecture is false, then take N as the smallest counter example. Commented Jul 14 at 22:41
• Yes, it turns out the statement is trivial, but the "nontrivial intuition" the question is trying to capture is interesting, and addressed nicely in Sam Hopkins' comment. Namely, if we had an oracle for BB(n), we could automate the proof/disproof of any well-defined claim.
– usul
Commented Jul 15 at 16:19

I would like to elaborate on an idea at the end of one of Z. A. K.'s comments above. The following quote is from Scott Aaronson's "The Busy Beaver Frontier" (2020):

As we’ll see in Section 5.2, there happens to be a Turing machine with $$27$$ states, which given a blank input, runs through all even numbers $$4$$ and greater, halting if it finds one that isn’t a sum of two primes. This machine halts if and only Goldbach’s Conjecture is false, and by the definition of $$BB$$, it halts in at most $$BB(27)$$ steps if it halts at all. But this means that knowing the value of $$BB(27)$$ would settle Goldbach's Conjecture—at least in the abstract sense of reducing that problem to a finite, $$BB(27)$$-step computation.

If Goldbach's conjecture is false, the smallest counterexample $$n$$ must be at most $$2\cdot BB(27)+2$$, since the machine will find the counterexample and halt after checking $$\frac{n-2}{2}$$ numbers, and this number must be at most $$BB(27)$$. If Goldbach is true, then as pointed out by Hamkins, any number $$N$$ will work, including $$2\cdot BB(27)+2$$. So $$2\cdot BB(27)+2$$ is an "explicitly" written down constant $$N$$ with the property you desire.

I say explicit in quotes since I argue that choosing $$BB(27)$$ for such a constant $$N$$ is essentially a repackaging of a trivial solution like "$$N$$ is $$2$$ if Goldbach is true, and the least Goldbach counterexample if Goldbach is false". Consider the set $$S$$ of $$27$$-state Turing machines which are inequivalent to the $$27$$-state Goldbach conjecture machine in Aaronson's paper under permuting states and mirroring the move instructions. Define the number $$N'$$ to be the supremum of the halting times of members of $$S$$ that halt on blank inputs. Also let $$f$$ be a computable function such that $$f(k)$$ is the number of steps it takes for the $$27$$-state Turing machine to check whether $$k$$ is a Goldbach counterexample or not, and that the machine has some constant number of setup steps $$c$$. Then $$BB(27)$$ is essentially "$$c+\sum_{2\leq k\leq n,\; k\text{ even}}f(k)$$ if this number is greater than $$N'$$, and $$N'$$ otherwise". In particular it will not be possible to get a nontrivial upper bound on $$BB(27)$$ until Goldbach is resolved.

Many years ago I was at a party in Berkeley and found myself standing in a group of fellow graduate students listening to Hendrik Lenstra, the famous number theorist, holding court.

Someone asked about the twin-primes conjecture, and whether there were infinitely many, and Lenstra said that he did not know the answer. However, he had a curious observation to offer. Namely, there was a particular number $$N$$, he claimed, such that if there were any twin primes above this number, then there would be infinitely many. So if we could somehow know this number, then even a single twin prime instance above it would imply that there must be infinitely many twin primes. Amazing!

We all stood around, pondering this profound announcement. But then he said, as he smiled, "It is completely trivial." And he waited. I felt that it was a kind of challenge he was making to us, the new students. And as a teacher I have now come to learn the profound importance of simply waiting in this way after a question, often awkwardly.

So we were all standing there, and I thought for a bit and said: Well, if there are only finitely many twin primes, then any $$N$$ above them all will do. And if there are infinitely twin primes, then any number $$N$$ will do.

Lenstra replied, "Perfectly so. So as I said — completely trivial!" This trick stuck with me since that party.

It is the same thing going on with your question, which has nothing to do with BB or computation or provability. It's just that if there were a counterexample, then any $$N$$ above the first counterexample would work. And if there is no counterexample, then any $$N$$ will work. (And this is exactly the same argument as Will provided in his answer, but I wanted to tell the Lenstra story, since I always think of that moment when I use this trick, with Lenstra smiling and nodding as he says "completely trivial!")

• I heard this argument from a graduate student of Peter Sarnak, who said that he stated the theorem "There exists an (ineffective) $\sigma>1/2$ such that if the Riemann zeta function has no zeroes with real part $>\sigma$ then the Riemann hypothesis is true" as an example of the weakness of results with ineffective constants. I don't know if this kind of idea is particularly common among number theorists. Commented Jul 13 at 19:04
• See also the drinker's paradox: en.wikipedia.org/wiki/Drinker_paradox. In any nonempty bar, there is a person, such that if that person is drinking at that moment, then everyone is drinking at that moment. Commented Jul 13 at 19:07
• @ZuhairAl-Johar I disagree. The question has nothing to do with intuitionistic logic, which definitely does not settle any nontrivial values of the BB function in any case---they are all independent of ZFC even, and there is no hope of constructive proofs of these things without settling the underlying question constructively as Will describes. The question and answers rather are about this certain trivial form of argument, a special proof by cases that is sometimes confusing for beginners, but which is also entirely a classical logic phenomenon. Commented Jul 13 at 21:56
• @IvanGalakhov: There need not be a constructive proof of $\exists N. (\forall x < N. P(x)) \rightarrow \forall x. P(x)$ even if $P(-)$ is very simple, e.g. computable. In fact a sufficiently constructive theory (e.g w/ numerical existence property) can't prove this for a computable predicate $P$ unless it also proves one of $\forall x. P(x)$ or $\neg \forall x. P(x)$. The way to think about it is not so much "it's enough to check if Goldbach holds up to $BB(n)$ for some $n$" and much closer to "we'd have to first settle Goldbach to pin down the value of $BB(n)$ for large enough $n$". Commented Jul 14 at 3:11
• @GeoffreyIrving: You can easily define "*$x$ is the $n$th Busy Beaver number*" in all constructive foundational systems (HA, MLTT, CZF) in widespread use, and then use this definition to pin down small values of $BB$, for example that 6 is the 2nd Busy Beaver number. You can't normally construct $BB : \mathbb{N} \rightarrow \mathbb{N}$ as a bona fide total function, since these system usually only construct computable $\mathbb{N} \rightarrow \mathbb{N}$ functions, which $BB$ isn't. Commented Jul 14 at 15:08

Yes, this can be proven directly.

Suppose all even numbers greater than two are a sum of two primes. Then $$N=2$$ works, so the statement is true.

Suppose not all even numbers greater than two are a sum of two primes. Let $$n$$ be an even number greater than two that is not a sum of two primes. Then $$N =n$$ works, so the statement is true.

Since the statement is true in either case, it is true.

The method of proof makes clear that (1) this can be replicated with other important theorems but (2) the statement you wrote is not as powerful as it seems at first.