Platonism

Studying all this decidability theory is fundamentally changing my view of the universe. In particular, I am losing my Platonism.

It all begins with the halting problem, which isn’t so much a problem anymore as a result. It states that there is no computer program which can tell whether another computer program will ever finish. The proof is so remarkably simple that I will paraphrase here:

Suppose there were such a program. Call it infinitely_loops(prog, input). It uses a magical complicated procedure to analyze prog and determine whether, when input is fed as the input to prog, prog will get into an infinite loop or not. Now let’s write a new program, called gah, which takes as input input, which is the source code for a program:

    // include source code for infinitely_loops here so we can use it
    if (infinitely_loops(input, input)) {
        exit();            // (a) finish immediately
    }
    else {
        while (true) { }   // (b) infinite loop
    }

Just to be clear: gah takes a program as input and then asks whether, when you feed it its own source code as input, whether it gets into an infinite loop. If it does, then gah exits immediately. If it doesn’t, then gah itself gets into an infinite loop.

Finally, we ask the question: what is the value of infinitely_loops(gah, gah)? That is, does gah get into an infinite loop when you feed it its own source code? Well, there are two possibilities;

  1. It does get into an infinite loop. But then look at the if statement above. We gave gah itself as input, so input = gah. Substituting, the if statement reads if (infinitely_loops(gah, gah)), which is what we’re asking about. The condition would be true, in which case our program would take branch (a) and exit immediately. But that’s no infinite loop, that’s definitely finishing. So there’s a contdadiction, which leaves only the remaining alternative:
  2. It does not get into an infinite loop. But in that case, in the if statement above, our program would have taken branch (b), so it would have entered the infinite loop we wrote there. Another contradiction!

So, since it can’t infinite loop, and it can’t not infinite loop, we have a contradiction, so our only assumption that the program infinitely_loops exists must have been false. There is no such program!

Okay, that was a little longer than I remember it. Still, the logic is simple and there is nothing magical about it.

I understood the halting problem even when I was in high school. I understood it, but I did not grok it. I thought it was totally neat that, after being introduced to programming and feeling like I could do anything, that there were computer programs which were impossible to write. Well, of course there are such programs: you can’t write a program which will tell you what will happen tomorrow. But this was a program which you could ask a real question to, a question which had an absolute, definite yes or no answer, and the program would not be able to answer it. That’s cool, isn’t it? It kinda gives meaning to being human, a kind of irreplacability, right?

Well, that’s what I thought at the time. I continued in college to study set theory and decidability theory, where I learned about Gödel’s incompleteness theorem. Unfortunately, that proof is not simple enough to repeat here :-). His theorem says that no matter how many assumptions you make, there will always be a statement in math which you cannot prove true or false. I’m not going to go into detail, but essentially he wrote down a logical statement which meant “such-and-such computer program eventually finishes”. Keep in mind that it’s very easy to write a computer program which will eventually write down everything that is provable (careful with the precedence there: it runs forever, writing down statements; it means that if you give me any provable statement, it will eventually write it down in its sequence). A proof is just a sequence of letters, and a computer is capable of checking whether a proof is valid. So just enumerate proofs, one-by-one (in practice this is completely infeasable, but we’re theorists!), check if it’s a valid proof, if so, write down what it proved. So if you could prove Gödel’s statement for any machine, then you could easily write a program which decided whether other programs infinite loop or not. But we just showed that that’s impossible, so it must also be impossible to prove Gödel’s statement.

This is when my mind started collapsing. The halting problem is not about what computers can do. It talks about all of mathematics. It means that determining whether computer programs infinite loop is a mathematically impossible problem, for both humans and computers. There are computer programs which the greatest mathematicans and programmers in the world could look at for years and never be able to determine whether or not it ends, without just running it (and if you run it, then you can wait until it ends and say “yes! it ends”; but if it doesn’t, you can wait forever until you die, never knowing whether it’s going to end or not).

Well, maybe it’s a problem in our reasoning skills. Maybe our logic is consistent, but it’s missing something that would conclude these things. Well, it turns out no. Gödel, the genius he was, also proved that if in every logically consistent world (“world” defined loosely, “mathematical system” is more accurate) a statement is true, then our proof system will be able to prove it. So then the halting problem becomes even more mind-boggling: there is some phantom statement we could add to logic that would allow us to prove that the machine does stop, and another phantom statement we could add that would allow us to prove that it does not. We hope (though, due to Gödel again, cannot prove) that our logic is consistent and represents the structure of information in the world. So how can whether this machine stops or not depend on which logic we use? It’s a fact! It either stops or it doesn’t!

I originally wrote about twice as much as you see here, but I realized that I wasn’t saying much, just going in circles. Essentially the whole idea of facts is vanishing from my world model. There are things that are true, and there are things that are false, and then there is fantasy. I don’t think our logic has holes, things that are true but it can’t prove given the proper assumption. It’s more like we’re asking questions about whether something will happen in the future, and in the case that it will, we will know only when it does. Notice that I didn’t consider the case that it won’t… because that case doesn’t even make sense :-).

About these ads

5 thoughts on “Platonism

  1. Sounds like yer ready to abandon the idealist Platonic perspective and embrace Aristotle… which means just this: how can you know anything absolutely when your only method of knowing is mediated by your senses?

  2. But, /please/, could you answer your own question, “So how can whether this machine stops or not depend on which logic we use? It’s a fact! It either stops or it doesn’t!”, (or give pointers to papers)?

    I myself, in my argumentations, came to this question many times but very never able to answer it…

  3. Okay, since this is a weekday, let’s go back to Platonism and assume that either the machine (call it M) halts or it doesn’t. If it does halt, then there is a proof that it does halt (just show when it does). The only case we have to worry about is when it doesn’t. Now, let’s again resort to Platonism and say “there is no proof that it doesn’t halt”. This is that ugly case where the machine transcends finite methods, the machine we know exists but which we will never be able to identify.

    It is easy to see how it would be consistent if we added the statement “M does not halt”. We would not find a contradiction. A little bit more subtle is the statement “M does halt”, which, more mathematically stated would read “there exists an n such that M halts in n steps”. Because of the completeness theorem, this won’t lead to a contradiction either. But n is fantastic; it is not a concrete number; it cannot be written 1+1+1+1+1+1+… some finite amount of times. Such “nonstandard integers” are allowed to exist, in that they can’t be proven not to from within PA. In the same way, M cannot be proven not to halt from within PA. That’s just an example though, you can use other systems (like ZFC) to ask the same questions, and you will get other independent constructions that weasel out of answering them.

    And back to the point of the post: all these Platonic assumptions don’t really even make sense. M neither does nor does not actually halt. If you’re using PA to ask, then it depends on whether you accept nonstandard integers in your model of PA or not. If you’re using “the real world” to ask, you just have to realize that M is just as much a figment of our imaginations as PA and ZFC are, and all “real” machines halt when they decay into heat energy.

    And do keep asking questions if something is unclear. By writing this response I realized the connection between nonstandard integers and the halting problem, so we’re learning together.

  4. Thanks for your detailled reply, and sorry for not answering earlier…

    Your post provoked quite a bit of thinking :) I still don’t quite grok it,
    though. I’ll first show the specific place I get stuck (aka a short version),
    and then formalize my thoughts (aka a long version), in the hope that a
    formalization will expose my problem(s) more exactly than intuitive reasoning
    could.

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

    In my thinking, a number of steps always needs to be a (plain normal standard)
    natural number. I can’t make sense of a sentence like “M halts in alpha steps”,
    where alpha is some nonstandard number you alluded to. (As an aside, is there a
    relationship between your nonstandard naturals and simple ordinals (with
    “simple” I mean ordinals I’m currently familiar with :), i.e. 0..epsilon_0,
    epsilon_0 excluded)?)

    Now to a formalization of my thoughts. (Sorry for the long post…)

    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:

    data Exp = Var String | App Exp Exp | Lam String Exp
    data Val = …
    eval :: Exp -> Val
    eval = …
    — eval is the standard eval function.

    — 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 evalutes to some value if G(n) is
    finite and bottoms otherwise…
    — eval (exampleExp n) terminates iff G(n) is finite.

    Now my question (I really apologize for the length…): 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.

    Where is my error in reasoning? (This comment has 56 lines. I feel really bad
    now, sorry…)

Leave a Reply

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

WordPress.com Logo

You are commenting using your WordPress.com 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 )

Google+ photo

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

Connecting to %s