Reply to Platonism

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

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

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

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

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

1Since 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


3 thoughts on “Reply to Platonism

  1. Wow, thanks: I think I’ve grokked it now :) (although I’m still a bit fuzzy
    about the details, but I believe that this is not substantial). To whom it
    interests, here is my current understanding. The key was to differentiate
    between the different worlds we talk about (physical universe, PA, ZFC) and to
    realize that objects of some system A can not simply be compared with objects
    of a different system B — the Goodstein sequences of PA are not the same
    Goodstein sequences as these of ZFC. For a summary, jump to the part marked
    with “##############”.

    Consider the real, physical, every-day world. In this universe, objects which
    exist include desks, books, and Linux computers. Objects which do not exist
    include numbers, sequences, sets, and Turing machines.

    In this world, it is possible to write a Haskell program which enumerates (what
    we think is) the* Goodstein sequence of some large number (I mean bit pattern,
    of course), say, 10^1234. When we run this program and come back a day later,
    there are two possibilities:

    1. Our Haskell program exit()ed. or:
    2. Our Haskell program did not yet exit().

    What conclusions about the* Goodstein sequence on 10^1234 can we draw from
    either possibility? None! The real, physical, every-day world — the universe
    which we’re considering at the moment — is not an idealized mathematical
    model; bugs and hardware errors etc. (insert your favourite eventuality here)
    are all possible and might have influenced the run of our program.

    Of course, such an answer (to recall, the answer is “we can not say anything
    about the* Goodstein sequence on 10^1234”) is unsatisfactory. Therefore we
    invent idealized mathematical models:

    Consider the world of PA. In this universe, objects which exist include
    natural numbers, Goodstein sequences, and Turing machines**. Objects which do
    not exist include ordinal numbers and desks, books, etc.

    In this universe, it’s possible to give the definition of a Turing machine
    which will (similar to our Haskell program) enumerate the PA-Goodstein sequence
    on the PA-natural number 10^1234; let’s name this Turing machine T.

    As PA does not have an in-built notion of “halting”, we (/we/!) have to make up
    a definition of halting; let’s define: We say that a PA-Turing machine M halts
    iff: exists n. stateAfterRunningForNSteps(M, n) = HALT_STATE (hand-waving a

    Let’s assume that PA can not prove that T halts, i.e. (per our definition
    above) that exists n. stateAfterRunningForNSteps(T, n) = HALT_STATE. What
    conclusions about the PA-Goodstein sequence on PA-natural 10^1234 can we draw
    from this? None — PA is consistent with both T halting and T not halting, i.e.
    PA is independent from the haltingness of T.

    We can, however, create a new system, based on PA, which includes “T halts”*** as
    an additional axiom; call this system PA1. In this world, a PA1-Turing machine
    which enumerates the PA1-Goodstein sequence on PA1-natural 10^1234 halts. (And
    this proposition can be proved trivially by using the newly-added axiom.)

    It’s also possible to create a new system (termed S+NG in your post), which
    includes “T does not halt” as additional axiom; call this system PA0. The
    PA0-Turing machine which enumerates the PA2-Goodstein sequence on PA0-natural
    10^1234 does not halt, and again, this proposition can be trivially proven.


    For me it was very important to realize that the PA1-Goodstein sequences are
    not the same as the PA0-Goodstein sequences! This is, in retrospect, very
    obvious: Mathematical objects do not exist “on their own”, in a “Platonist
    heaven” — they /depend on a given (formal) system/! Also, the notion of
    existence of a mathematical object is a man-made definition.**** (I think this is
    exactly the point you were making. :))

    Solely to drive the point home, let’s consider the world of ZFC (in which
    ZFC-numbers, ZFC-sets, ZFC-ordinals, ZFC-Turing machines, etc. exist and in
    which desks, bookes etc. do not exist): The ZFC-Goodstein sequences (which are
    to be distinguished from the PA-, PA1- and PA0-Goodstein sequences) can be
    proven to ZFC-halt, where “ZFC-halt” is defined as exists n \in N = {0,1,…}.
    zfcStateAfterRunningForNSteps(T, n) = HALT_STATE.

    So, when Wikipedia says, “Goodstein’s theorem is a statement about the natural
    numbers that is unprovable in Peano arithmetic but can be proven to be true
    using the stronger axiom system of set theory”, what is actually meant is the

    * PA-Goodstein sequences can not (in general) be proved to be finite.
    * PA1-Goodstein sequences can be trivially proven to be finite.
    * PA0-Goodstein sequences can be trivially proven to be infinite.
    * ZFC-Goodstein sequences can be proven to be finite (using cool ordinal

    Sloppy speaking (i.e. not using “PA-“, “ZFC-” prefixes) results in the
    (mis-)belief that proofs of properties of ZFC-Goodstein sequences would
    automatically apply to PA-Goodstein sequences, while this is (in general) not
    the case. (Am I correct?) [Of course, some proofs can be “ported”, for example
    from systems A to systems B, where B is a conservative extension of A.]

    Thank you very much! (Even in the case that there are terrible errors in my
    reasoning, I still had fun thinking about and writing this :))


    PS. I think a bit of Platonism (if I understand it correctly) can be rescued
    by dividing the absolute Platonist heaven (which is, as you point out, a
    non-sustainable notion) into several, separate heavens for each formal system
    (i.e. the PA-heaven, the ZFC-heaven etc.)

    PPS. Propositions which are independent of one’s favourite system — like
    Goodstein’s theorem in PA — remind me a bit of non-falsifiable (and
    non-verifiable) theories like “the physical world came into existence ten
    minutes ago” (name this theory F): As such theories are non-falsifiable and
    non-verifiable, they are not (modulo meta-considerations) interesting.
    Questioning “is F true?” is equally pointless as questioning “are all
    PA-Goodstein sequences finite?”, as both questions are inherently
    un-answerable. (I do not mean “pointless” in a dismissive sense, but I lack a
    better word.)

    Footnotes (probably only understandable after having read the rest):

    * With “the” Goodstein sequence, I mean a REALWORLD-Goodstein sequence. (Where
    “REALWORLD” is the identifier for the physical, real world system (like “PA” is
    for Peano Arithmetic).)

    ** I don’t think that Turing machines can be constructed in PA, as the usual
    definitions of Turing machines require the notion of a set (e.g. the alphabet
    set etc.). But, as I understand it, at least comparable things can be
    constructed. I think that this problem is not substantial to my reasoning.

    *** With “T” in ‘”T halts”‘ I mean the analogon of PA-T in PA1, i.e. PA1-T.

    **** For example (warning, hand-waving here), in intuitionistic reasoning, one
    has to give an explicit construction of an object x to show that it exists,
    while in classical reasoning it’s sufficient to prove that the proposition “x does not
    exist” causes a contradiction.

  2. My comment was stripped by copy-&-pasting smart quotes.

    What I was saying is that negation does not flip quantifiers in intuitionistic logic, so the negation of a universal is not simply an existential, since existentials require witnesses.

    There are statements that are true-but-not-provable in intuitionistic logic such that making an axiom of the negation is inconsistent. An example of this is the Law of Excluded middle, where the law itself is not provable, but the double negation of it is.

Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out /  Change )

Google+ photo

You are commenting using your Google+ account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )


Connecting to %s