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?

  • 1
    $\begingroup$ It is probably best to specify that you are interested in discussing first-order logic. $\endgroup$ – hardmath Mar 5 '18 at 3:02
  • 3
    $\begingroup$ Ultimately, it comes down to whether the axioms you've used in your proof are sound - that is, if they are all true statements about the natural numbers. (Here for simplicity, and I think this matches your OP, I'm taking a somewhat Platonist stance and assuming that "the natural numbers" is a thing that makes sense.) $\endgroup$ – Noah Schweber Mar 5 '18 at 3:02
  • 1
    $\begingroup$ @CarlMummert It's not really an answer, though, since it just pushes the question back: how do we know that the axioms we use are correct? $\endgroup$ – Noah Schweber Mar 5 '18 at 3:41
  • 2
    $\begingroup$ @Shufflepants: "rules out most" is incorrect; please read my answer. Every consistent practical formal system $S$ (namely one that has a proof verifier program and interprets arithmetic, such as PA) has a non-standard model, since $S + \neg \text{Con}(S)$ is consistent but arithmetically unsound. In fact, it is easy to prove that every such $S$ has uncountably many non-standard countable models! $\endgroup$ – user21820 Mar 6 '18 at 13:14
  • 2
    $\begingroup$ @Shufflepants: You used the term "non-standard" wrongly, because it has an established meaning in mathematical logic. And this question is about "non-standard models" with the established meaning, so frankly your comment remains irrelevant to this question. It may be interesting looking at how induction over PA− restricts the possible models, but it is simply not what this question is about. (And saying that 3 of 4 infinite kinds is most is just wrong; cardinality of number of countable models is still the same with or without induction...) $\endgroup$ – user21820 Mar 6 '18 at 16:07

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

  • $\begingroup$ +1. One comment on the first sentence - I think it is possible to separate the existence of a unique intended interpretation from the general soundness of a theory. For example, each model of ZFC determines its own set of natural numbers, but that model also satisfies "Peano Arithmetic is a sound theory". So in principle someone could choose any model of ZFC to be their standard model, choose ZFC to be their metatheory, and then prove that PA is sound for their model using their metatheory. This would be compatible with weaker forms of Platonism and even with some kinds of formalism. $\endgroup$ – Carl Mummert Mar 5 '18 at 4:10
  • $\begingroup$ Right, I think is the right answer. (+1, and possible future accept.) Then to answer the question in my final sentence, the answer would be "proofs made in some more powerful system such as ZFC, for which the idea of a canonical 'standard model' is less clear cut than for PA; but there is no precise place in which we can draw the line." This is unsatisfying but unavoidable. $\endgroup$ – Nathaniel Mar 5 '18 at 10:03
  • $\begingroup$ (I'm not at all sure I do believe that the standard natural numbers "exist" in any sense, but I suppose I was implicitly assuming that for the sake of the question.) $\endgroup$ – Nathaniel Mar 5 '18 at 10:03
  • $\begingroup$ @Nathaniel: The answer to your final sentence is as stated in my answer. Note that one cannot meaningfully talk about a "canonical standard model" of ZFC in the same way (we believe) we 'know' the canonical standard model for PA, because it cannot be described in any non-circular sense. For PA, we have the 'option' of resorting to describing a real-world interpretation of PA, which while vague at the least reduces the philosophical problem a lot. And as I explained, it is not about having a model; being $Σ_1$-sound is sufficient. $\endgroup$ – user21820 Mar 5 '18 at 10:14
  • 1
    $\begingroup$ @Nathaniel: If ZFC is $Σ_1$-sound, then it does not matter whether ZFC proves rubbish about set-theoretic sentences, and it does not matter even if ZFC proves a false $Σ_2$-sentence, because it will still hold that if ZFC proves that a program halts on an input then it really does halt. $\endgroup$ – user21820 Mar 5 '18 at 10:16

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


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.

  • $\begingroup$ Thank you so much for this answer. There is a lot to read through and digest in the links, as well as in the answer itself; you've given me a lot to think about. $\endgroup$ – Nathaniel Mar 5 '18 at 12:04
  • $\begingroup$ @Nathaniel: You're welcome! And feel free to come to the Logic chat-room for any logic discussion. $\endgroup$ – user21820 Mar 5 '18 at 12:36

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.


The statement that we cannot pin down natural numbers does not mean that we cannot check to see whether the axioms you used in your proof hold for standard integers or not.

  • 1
    $\begingroup$ Can we, though? The theory of arithmetic is undecidable, so that's a bold claim ... $\endgroup$ – Noah Schweber Mar 5 '18 at 3:16
  • 1
    $\begingroup$ I don't think the statement I wrote is incorrect (without making the claim you mentioned). What I had in mind writing that statement is that we cannot pin down integers, because any finite set of axioms we choose leads to the undecidability of some statements. However, when we use an axiom in a proof, we normally know whether it holds for standard integers or not. Of course, you could pick an arbitrary statement as an axiom and use it in a proof, but that is never done in practice. Am I wrong? $\endgroup$ – stochastic Mar 5 '18 at 3:46
  • 5
    $\begingroup$ I'm not certain whether I agree with the statement "However, when we use an axiom in a proof, we normally know whether it holds for standard integers or not." For example, ZFC proves the consistency of theories which I'm not fully confident are consistent, so I'm not fully confident in ZFC's consistency, let alone its arithmetical soundness. But the ZFC axioms are of course widely used (including by me!). So I'm not sure that we are always justified in our confidence in the arithmetical soundness of the axioms we use. $\endgroup$ – Noah Schweber Mar 5 '18 at 3:51

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!

  • 2
    $\begingroup$ I don't think this is quite answering the question, which is how we can be certain that the result we've proved holds in the standard model. $\endgroup$ – Noah Schweber Mar 5 '18 at 3:32

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.