How can we know we're not accidentally talking about non-standard integers?

Question

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?

Answer 1

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

Answer 2

We know that any formal system cannot completely pin down the natural numbers.

Incidentally, I said exactly this here. Besides what I said in that post, I wish to elaborate on the following points:

• A generalized version of the Godel-Rosser incompleteness theorem shows convincingly that there is no practical formal system that can pin down the natural numbers. Specifically, we can easily write a program that, given any proof verifier program for any formal system that interprets arithmetic, will produce an explicit arithmetical sentence that can neither be proven nor disproven by that system. How convincingly? If we phrase the incompleteness theorem in a certain way, it can be proven even in intuitionistic logic. But we still need to work in some meta-system that 'has access to' a model of PA or equivalent, otherwise we cannot even talk about finite strings, which are the basic building blocks of any practical formal system.

• The philosophical issue is that as far as the real-world is concerned, the empirical evidence suggests that there is no real-world model of PA, due partly to the finite size of the observable universe, but also the fact that a physical storage device with extremely large capacity (on the order of the size of the observable universe) will degrade faster than you can use it! So there is a weird philosophical problem with the preceding point, because if one does not believe that the collection of finite strings embeds into the real-world, then the incompleteness theorems do not actually apply...

• On the other hand, there is undeniably huge empirical evidence that the theorems of PA when translated into statements about real-world programs are correct at human scales. Just for example, there is no known counter-example to the theorems underlying RSA decryption, which depend on Fermat's little theorem among other basic number-theoretic theorems applied to natural numbers on the order of $2^{2048}$. So one still has to explain the incredible accuracy of PA at small scales even if it cannot have a real-world model.

---

But suspending philosophical disbelief, and working in a weak formal system called ACA that practically every logician believes is sound (with respect to the real world), there are many things we can in fact say for sure (besides the incompleteness theorem), that would answer your question (if ACA is sound).

Suppose that for some particular Turing machine $Z$, I have proven that $Z$ halts [after some number $N$ of steps. H]ow can I know for sure that $N$ is a standard natural number and not a nonstandard one?

Your proof is done within some formal system $S$. If $S$ is $Σ_1$-sound (with respect to the real-world) then you can know for sure that $Z$ really halts. It is entirely possible that $S$ is not $Σ_1$-sound, and that you can never figure it out. For example, given any practical formal system $S$ that interprets arithmetic, let $S' = S + \neg \text{Con}(S)$. If $S$ is consistent, then $S'$ is also consistent but $Σ_1$-unsound. In particular, it proves that the proof verifier for $S$ halts on some purported proof of contradiction over $S$, which is exactly the type of question you are concerned about!

Worse still, the arithmetical unsoundness of a formal system can lie at any level of the arithmetical hierarchy, as constructively shown in this post. Precisely, if $S$ is $Σ_n$-sound then there is a $Σ_n$-sound extension of $S$ that is $Σ_{n+1}$-unsound.

These imply that it may be difficult to have confidence in the soundness of a formal system without some philosophical justification. Firstly, unsoundness cannot be detected by checking for a proof of inconsistency. Now, if $S$ is sufficiently expressive, we may be able to state "$S$ is arithmetically sound" over $S$, in which case we can check for a proof of its negation over $S$, and if so we know something is really wrong. But even for mere consistency, if we enumerate (endlessly) all possible proofs and never find a contradiction, we still have only enumerated an 'infinitesimal' fraction of all possible proofs, far too little to be sure that there really is no contradiction.

It gets worse. Consider the following:

Let $Q$ be some $Π_1$-sentence such that $S$ proves ( $Q$ is true iff there is no proof of $Q$ over $S$ with less than $2^{10000}$ symbols ).

It turns out that we can indeed easily construct such a sentence $Q$, using the standard Godel-coding tricks and the fixed-point theorem. What may be shocking to those unfamiliar with this is that $Q$ is actually quite short (less than a billion symbols if $S$ is something like ZFC), and if $S$ is $Σ_1$-complete, then $Q$ is provable over $S$ (because $S$ can check every possible proof with less than $2^{10000}$ symbols) but its shortest proof has at least $2^{10000}$ symbols!

Now let $T = S + \neg Q$, where $S$ has any reasonable deductive system. Firstly, $T$ is inconsistent. Secondly, the shortest proof of its inconsistency is on the order of $2^{10000}/len(Q)$, because it can be converted into a proof of ( $\neg Q \to \bot$ ) over $S$, which after a finite number of extra steps would give a proof of $Q$ over $S$.

In conclusion, a formal system could have a rather small description, but have an inconsistency whose proof is so long that we can never ever store it in the physical world...

---

Finally:

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?

It should be clear from all the above that it is indeed the case. To repeat, you need the proof that $Z$ halts to be done within a formal system that is $Σ_1$-sound. How could you know that? Well we cannot know any such thing for sure. Almost all logicians believe that ACA is arithmetically sound, but different logicians start doubting soundness at different points as you climb up the hierarchy of formal systems. Some doubt full second-order arithmetic, called Z2, because of its impredicative comprehension axiom. Others think it still is fine, but doubt ZFC. Some think that ZFC is fine, but doubt some large cardinal axioms.

Answer 3

In order to talk about "standard" integers, someone needs to already have some collection of "integers" that they think are the "standard ones". Of course, they may not know everything about these integers, but they do need to think that there is some particular collection of objects which are the "standard integers". Similarly, someone might have a collection of objects that they believe is the "standard" model of set theory.

We use the term sound about a set of axioms to mean that the axioms are true in our preferred "standard model" (as in the previous paragraph). This is a different meaning of soundness than in the soundness theorem for first-order logic.

For example, the axioms of Peano Arithmetic (PA) are usually taken to be sound about the standard natural numbers, and the axioms of ZFC are taken to be sound about the standard model of set theory. That is the basic answer to the question: if we prove that a Turing machine halts using a sound theory, then the Turing machine actually halts, because by definition each statement provable in a sound theory is true about the corresponding standard model.

We could push farther and ask: how can we prove this soundness? One option is a direct, informal appeal to intuition. Another option is to prove the soundness of one axiom system in another formal axiom system - a metatheory.

This leads to a situation similar to the well-known problem of proving the consistency of a foundational system of axioms. Gödel's incompleteness theorems show that our main foundational theories cannot prove their own consistency. Similarly, these theories cannot prove (cannot even express) their own soundness. However, if we assume a sufficiently strong metatheory, we can use the metatheory to prove the soundness of a foundational theory.

For example, ZFC proves that Peano Arithmetic is sound, and Morse-Kelley set theory proves that ZFC set theory is sound. The challenge here, as with consistency, is that there is a kind of regress. To prove that Morse-Kelley set theory is sound, we would need to assume a yet stronger metatheory, and to prove that is sound we need to assume an even stronger one than that.

This is when the "direct appeal to intuition" option becomes more attractive. Just as we might believe that the axioms of Euclidean Geometry are true about the plane $\mathbb{R}^2$ without proving this in any particular metatheory, we could in principle believe that PA and ZFC are sound without worrying about which metatheory the soundness can be proved in. This would depend on us believing that the axioms of these formal systems are all true statements about our preferred "standard" models.

Answer 4

Because you have an explicit formal description of (how to encode) Turing machines and their execution.

Among the features of this formal description are:

• the places on the tape are indexed by the natural numbers
• the steps of an execution trace are indexed by natural numbers
• the interpretation of strings as numbers produces natural number output

So, you can be confident that whatever model of analysis^* you took as input to the theory of computation, the numbers your machine will output will all be the natural numbers of that model.

_{*: By "model of analysis" I basically mean the model of whatever limited amount of set theory / type theory / higher order logic / whatever you need to reason with.}

---

You can, however, develop the theory of computation in a nonstandard model of analysis. The natural numbers such a machine can compute are, of course, quite capable of being nonstandard.

It should be possible, though, to take a standard Turing machine and convert it into a nonstandard one. And it is quite possible to have a situation where you have a standard Turing machine and a nonstandard model of analysis for which the standard machine might run forever but the nonstandard version of it halts.

I think it's even possible that some nonstandard model says your standard machine halts, and some other nonstandard model says that the machine not only runs forever, but it will run forever in every nonstandard extension of that model!