This question is mostly from pure curiosity.
We know that any formal system cannot completely pin down the natural numbers. So regardless of whether we're reasoning in PA or ZFC or something else, there will be nonstandard models of the natural numbers, which admit the existence of additional integers, larger than all the finite ones.
Suppose that for some particular Turing machine $Z$, I have proven that $Z$ halts, but that it does so only after some ridiculously huge number of steps $N$, such as $A(A(A(10)))$, where $A$ is the Ackermann sequence. My question is, in a case like this, how can I know for sure that $N$ is a standard natural number and not a nonstandard one?
Of course, in principle I could just simulate the Turing machine until it halts, at which point I would know the value of $N$ and could be sure it is a standard natural number. But in practice I can't do that, because the universe would come to an end long before I was finished. (Let's suppose, unless this is impossible, that there is no way around this for this particular Turing machine; that is, any proof of the exact value of $N$ has a length comparable to $N$.)
If $N$ does turn out to be a nonstandard number then the Turing machine does't halt after all, since when simulating it we would have to count up through every single standard natural number before reaching $N$. This would seem to put us in a tricky situation, because we've proven that some $N$ exists with a particular property, but unless we can say for sure that $N$ is a standard natural number then we haven't actually proven the Turing machine halts at all!
My question is simply whether it's possible for this situation to occur, or if it's not, why not?
I appreciate that the answer to this might depend on the nature of the proof that $Z$ halts, which I haven't specified. If this is the case, which kinds of proof are susceptible to this issue, and which are not?
Best Answer
[I will take for granted in this answer that the standard integers "exist" in some Platonic sense, since otherwise it's not clear to me that your question is even meaningful.]
You're thinking about this all wrong. Do you believe the axioms of PA are true for the standard integers? Then you should also believe anything you prove from PA is also true for the standard integers. In particular, if you prove that there exists some integer with some property, that existence statement is true in the standard integers.
To put it another way, anything you prove from your axioms is true in any model of the axioms, standard or nonstandard. So the existence of nonstandard models is totally irrelevant. All that is relevant is whether the standard model exists (in other words, whether your axioms are true for the standard integers).
Now, I should point out that this notion is a lot slipperier for something like ZFC than for something like PA. From a philosophical standpoint, the idea that there actually exists a Platonic "standard set-theoretic universe" that ZFC is correctly describing is a lot less coherent than the corresponding statement for integers. For all we know, ZFC may actually be inconsistent and so it proves all sorts of false statements about the integers. Or maybe it is consistent, but it still proves false statements about the integers (because it only has nonstandard models). But if you do believe that the ZFC axioms are true in their intended interpretation, then you should believe that any consequences of them are also true (including consequences about the integers).