Existence properties for first-order number theory are all finitely checkable

OK, that's a mouthful.

I wrote an answer to How can I show that a function is not computable over at Quora, which brought up the Busy Beaver function.

BB(n) is a typical example of a non-computable function. But, it's a perfectly well-defined one. BB(n) is the maximum number of steps that an n-state Turing machine that halts can perform, when started on an empty tape. To date, we know the first four values, and some lower bounds on the next two: https://oeis.org/A060843

So, suppose you want to know whether some integer exists: an odd perfect number. A counterexample to Goldbach's conjecture. A counterexample to something equivalent to the Riemann Hypothesis. Integers can be proofs too. Maybe you want an integer that encodes a proof of Fermat's Last Theorem, or that P != NP.

Write a Turing machine that does the following:

1. Start with X = 0
2. Check whether X satisfies the property you want
3. If not, increment X by one and repeat

If the counterexample/proof/whatever exists, then this algorithm finds it. Moreover, it's a Turing machine with N states, so it must take less than BB(N) steps to find the the number, if it exists. Because, once we go past BB(N) steps, the Turing machine can't halt.

Therefore, any property that can be expressed in this form can be proven by checking only finitely many examples.

Unfortunately "finitely many" here means "incomprehensibly huge." BB(n) grows faster than any computable function, so it's faster than tetration, faster than any Knuth arrow notation, faster than TREE.

BB(6) > 8,690,333,381,690,951

and it's pretty much impossible to do 8 quintillion of anything, let alone the truly monstrous numbers we would be dealing with on a nontrivial Turing machine.

Still, it's a little strange. It doesn't look like the Goldbach conjecture has anything to do with computational complexity theory; but theory gives us a bound anyway.