Here’s a reply to a comment

that was left about my recent post “Platonism”. The discussion is

getting long and involved, so I thought I’d make a new post. And to

anonymous (the poster), don’t worry about the comment length. I’m only

posting anew to draw attention to the interesting discussion.

So, without further ado, the short version: For me, the n of your

sentence ‘But n [declared via 'there exists an n such that M halts in n

steps'] is fantastic; it is not a concrete number; it cannot be written

1+1+1+1+1+1+… some finite amount of times.”, needs to be a plain

normal standard natural number (i.e. element of N = { 0, S(0), S(S(0)),

… }), as you’ve introduced n as giving the /number of steps/.

But in the context of that definition, we were still working in PA,

which is *incapable* of saying “*n* is a standard natural”

without giving some other kind of constraint (for example, being less

than a number written S(S(S(…S(0))))). I’ll go into more detail when

I discuss Goodstein’s Theorem below, which actually provides a nice

context for discussing nonstandard naturals.

As meta language, I’ll use a Haskell-like language which does not

have ordinals (this will become relevant in a second). As object

language, I’ll use the untyped lambda calculus. Without further

ado:

-- I'll use Goodstein's Theorem
-- as example. Briefly, it
-- states that every Goodstein sequence terminates, i.e. that G(n) is finite
-- for all n in N = { 0,1,... }. It is unprovable in PA, but can be proved with
-- cool ordinal arithmetic.
exampleExp :: Nat -> Exp
exampleExp n = ...lambda expression which evaluates to some value if G(n) is
finite and bottoms otherwise...
-- eval (exampleExp n) terminates iff G(n) is finite.

Now my question: In my opinion, eval (exampleExp n) halts for every

n::Nat, as we know that every Goodstein sequence is finite. But from

what I understand of your reply, adding the axiom “eval (exampleExp n)

does not halt for some n :: Nat” would be consistent, as we cannot prove

the finiteness of all Goodstein sequences, as our meta language does not

have ordinals.

In short, I see the finiteness of all Goodstein sequences as an

absolute truth; I accept this truth even if we cannot prove it in some

formal systems.

First things first, the problems I was talking about are

fundamentally different from this question in that the halting problem

is not solvable by *any* formal system (assuming Church’s thesis).

But there’s still a lot of interesting stuff to be reaped from your

question.

Just because your meta language doesn’t have ordinals doesn’t mean

Goodstein’s theorem is not provable (well, unless Goodstein’s theorem

gives rise to ordinals :-). But what we can say is that if Goodstein’s

theorem is unprovable in your meta language, then it is consistent with

nonstandard naturals; i.e. Nat might denote more than just the set of

things in { 0, 1, 2, … }.

We can see this by looking at the negation of Goodstein’s theorem,

which looks like “exists n. forall k. not Goodstein(n,k)” (where

Goodstein(n,k) means the Goodstein sequence starting at n reaches 0 in k

steps). Let’s call this sentence NG, and your meta language S. If S

does not prove Goodstein’s theorem, then S+NG is consistent (if not,

that would be a proof). By the completeness theorem, then, S+NG has a

model in ZFC. And what the heck is n from “exists n. …” in that

model? It had better not be one of { 0, 1, 2, … }. So the model of

Nat in S+NG can’t be isomorphic to the set N from set theory; i.e. S+NG

actually *asserts* the existence of nonstandard naturals.

It is useless to think of the nonstandard naturals as actually

existing, though. *n* is merely a figment of the finite reasoning

available to the proofs in S. If proofs could be infinitely long, then

NG would be inconsistent with S (as well as a myriad of other things,

such as PA being complete (and thus inconsistent? I don’t know if the

incompleteness theorem applies if proofs are allowed to be

infinite)).

So now the difference between the halting problem and Goodstein’s

theorem: PA does not “know” that Goodstein’s theorem applies to it, but

ZFC knows. That is, assuming ZFC is consistent, then Goodstein’s

theorem about PA is true. But ZFC does not know everything about PA.

I seem to recall a game-theoretic theorem in PA which employed a large cardinal

axiom. But it’s pretty easy to show that there are statements in PA

that ZFC cannot prove true or false about its model of PA^{1}. ZFC’s also has got its own bundle of undecidable issues, the continuum hypothesis to name one. But we can use a bigger system that models ZFC and possibly prove the continuum hypothesis one way or the other.

And now I just had an ephiphany… I was going to say “you can keep

expanding the system up and making more and more abstract axioms, but

there is a single Turing machine which evades them all”. That is not

true though. Obviously, you can add axioms “such-and-such Turing

machine does not ever halt”, and if it actually doesn’t (Platonically

speaking), then of course that is consistent. Then it seems possible

that we may find more and more “obvious truths” about mathematics, and

those will start proving that more and more Turing machines don’t halt.

For any given Turing machine, we may eventually find a “natural” axiom

which proves it doesn’t halt. If that were the case, it would mean that

the set of axioms about the universe is not only infinite, but

non-recursive. Knowing the universe, that seems reasonable :-).

If not, though, then there is a Turing machine which evades all of

our reasoning. This also seems reasonable, since there are machines as

small as 5 states and 2 symbols whose halting problems are yet unknown,

for example:

State Read 0 Read 1
-------------------------
a 1 L b 1 R b
b 1 R c 0 L e
c 0 R d 0 L a
d 1 L a 0 R d
e -halt- 0 L c

(Marxen &

Buntrock)

I hope that cleared some of the blocks making you believe that this area is in any way clear :-).

To answer another question, nonstandard naturals have very little to do with the ordinals from

set theory. All countable nonstandard models of arithmetic are isomorphic, so we know that the

nonstandards we got from negating Goodstein’s theorem are the same ones we get by standard application

of the compactness theorem. There’s

no least nonstandard natural (as omega is to the ordinals); rather, they look like the lexographic

ordering of Q × Z; for each rational number there is a copy of the integers (both positive

and negative). Of course they are all greater than the standard naturals. They satisfy

*every* first-order sentence provable by PA. A classic example is that the twin prime conjecture

is true if and only if there is a nonstandard twin prime, because the twin prime conjecture is

stated as “forall a. exists b > a. ‘b and (b+2) are prime’”, which,

if true, must hold for nonstandard a’s as well.

Funny coincidence, a program computing the Goodstein sequence of a number was one of the

first Haskell programs I ever wrote. :-)

^{1}Since PA is turing complete, it can embed the axioms of

ZFC as Gödel numbers. You can thus construct a statement of PA

that says “ZFC is consistent”. And of course, because of the

incompleteness theorem, ZFC cannot prove this statement true or

false.