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).