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

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.

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

bit)

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

following:

* 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

arithmetic).

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.

As a side note, I don’t think your analysis applies to intuitionistic logic. You say

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.