{"id":710,"date":"2011-07-21T16:35:59","date_gmt":"2011-07-21T21:35:59","guid":{"rendered":"https:\/\/scottaaronson.blog\/?p=710"},"modified":"2017-01-12T16:31:26","modified_gmt":"2017-01-12T21:31:26","slug":"rossers-theorem-via-turing-machines","status":"publish","type":"post","link":"https:\/\/scottaaronson.blog\/?p=710","title":{"rendered":"Rosser’s Theorem via Turing machines"},"content":{"rendered":"

(Thanks to Amit Sahai for spurring me to write this post!)<\/em><\/p>\n

The Background<\/strong><\/span><\/p>\n

We all remember G\u00f6del’s First Incompleteness Theorem<\/a> from kindergarten.\u00a0 This is the thing that, given a formal system F, constructs a sentence G(F) that’s a mathematical encoding of<\/p>\n

“This sentence is not provable in F.”<\/p>\n

If F proves G(F), then F proves both that F proves G(F) and that F doesn’t prove G(F), so F is inconsistent (and hence also unsound).\u00a0 Meanwhile, if F proves Not(G(F)), then it “believes” there’s a proof of G(F).\u00a0 So either that proof exists (in which case it would render F inconsistent, by the previous argument), or else it doesn’t exist (in which case F is unsound).\u00a0 The conclusion is that, assuming F is powerful enough to express sentences like G(F) in the first place, it can’t be both sound<\/em> and complete<\/em> (that is, it can’t prove all and only the true arithmetical statements).<\/p>\n

OK, but the way most people like to state G\u00f6del’s Theorem is stronger than that: no sufficiently-powerful formal system F can be both complete and consistent<\/em>.<\/strong>\u00a0 Note that soundness implies consistency, but not vice versa.\u00a0 (If I believe that there’s a giant purple boogeyman on the moon, then presumably my belief is unsound<\/em>, but it might be perfectly consistent<\/em> with my various other beliefs about boogeymen.)<\/p>\n

Unfortunately, neither G\u00f6del’s original proof, nor computer scientists’ favorite alternative proofs, actually give you the stronger statement about completeness and consistency<\/em>.\u00a0 And this has been a persistent problem when I teach\u00a0G\u00f6del in my undergraduate computability and complexity class.<\/p>\n

Where’s the catch in\u00a0G\u00f6del’s argument?\u00a0 It’s in the case where F proves Not(G(F)) (i.e., that G(F) is provable), even though in reality G(F) is true (i.e., G(F) isn’t<\/em> provable).\u00a0 In that situation, F would clearly be unsound<\/em>, but it might not contain any contradiction<\/em>—basically because, no matter how long you looked, you could never rule out F’s (false) belief that G(F) is provable.\u00a0 Indeed, F would be what I like to call a self-hating theory<\/em>: a theory, like F+Not(Con(F)), that pessimistically believes in its own inconsistency, even though in fact it’s perfectly consistent.\u00a0 (By contrast, if F arrogantly believes in its own consistency<\/em>, then it can’t<\/em> be consistent by the Second Incompleteness Theorem!\u00a0 There’s a lesson there somewhere…)<\/p>\n

The way G\u00f6del himself solved this problem was by introducing a new concept called \u03c9-consistency<\/a>, which is intermediate between consistency and soundness.\u00a0 He then showed that F can’t be both complete and \u03c9-consistent.\u00a0 (Why didn’t G\u00f6del simply talk about soundness?\u00a0 Because unlike consistency or \u03c9-consistency, soundness is a “metatheoretic” concept that’s impossible to formalize in F.\u00a0 So, if he used soundness, then the First Incompleteness Theorem couldn’t even be stated<\/em>, let alone proved, in F itself, and that in turn would create problems for the proof of his Second<\/em> Incompleteness Theorem.)<\/p>\n

Anyway, from the standpoint of an undergrad class, the fear is that, once you start talking about “\u03c9-consistency,” all the romance and self-referential magic of\u00a0G\u00f6del will vanish in a morass of technicality.<\/p>\n

So surely we can dot the i’s here (or rather, put the umlauts on the \u00f6’s), and prove the stronger, cleaner statement that F can’t be both complete and consistent<\/em>?<\/p>\n

Yes we can—but to do so we need Rosser’s Theorem<\/a>: a strengthening of G\u00f6del’s Theorem from 1936 that’s much less well-known among the nerd public than it ought to be.\u00a0 In Rosser’s proof, we replace G(F) by a new sentence R(F), which is a mathematical encoding of the following:<\/p>\n

“For every proof of this sentence in F, there’s a shorter disproof.”<\/p>\n

If F proves R(F), then it also proves that there’s a disproof<\/em> of R(F) that’s shorter than the proof of R(F) whose existence we just assumed.\u00a0 So we can look<\/em> for that disproof (since there are only finitely many strings of symbols to check), and either we’ll find it or we won’t—but in either case, we’ll have revealed F to be inconsistent.\u00a0 Meanwhile, if F proves Not(R(F)), then it proves that there is<\/em> a proof of R(F) with no shorter disproof.\u00a0 So in particular, it proves that there’s a proof of R(F) that’s no longer<\/em> than the proof of Not(R(F)) whose existence we just assumed.\u00a0 But once again, we can look<\/em> for that proof (there are only finitely many strings to check), and either we’ll find it or we won’t, and in either case, F is revealed to be inconsistent.<\/p>\n

Notice what the Rosser sentence accomplishes: it creates a symmetry<\/em> between the cases that R(F) is provable and R(F) is dis<\/em>provable, correcting the asymmetry between the two cases in G\u00f6del’s original argument.<\/p>\n

Alright, so then why don’t I just teach Rosser’s Theorem in my undergrad class, instead of G\u00f6del’s?<\/p>\n

I’ll tell you why: because, when <\/em>I teach G\u00f6del to computer scientists, I like to sidestep the nasty details of how you formalize the concept of “provability in F.”\u00a0 (From a modern computer-science perspective, G\u00f6del numbering<\/a> is a barf-inducingly ugly hack!)<\/p>\n

Instead, I simply observe G\u00f6del’s Theorem as a trivial corollary of what I see as its conceptually-prior (even though historically-later) cousin<\/em>: Turing’s Theorem on the unsolvability of the halting problem.<\/a><\/p>\n

For those of you who’ve never seen the connection between these two triumphs of human thought: suppose we had a sound and complete (and recursively-axiomatizable, yadda yadda yadda) formal system F, which was powerful enough to reason about Turing machines.\u00a0 Then I claim that, using such an F, we could easily solve the halting problem.\u00a0 For suppose we’re given a Turing machine M, and we want to know whether it halts on a blank tape.\u00a0 Then we’d simply have to enumerate all possible proofs in F, until we found either<\/em> a proof that M halts, or<\/em> a proof that M runs forever.\u00a0 Because F is complete, we’d eventually find one or the other, and because F is sound, the proof’s conclusion would be true<\/em>.\u00a0 So we’d decide whether M halts.\u00a0 But since we already know (thanks to Mr. T) that the halting problem is undecidable, we conclude that F can’t have existed.<\/p>\n

“Look ma, no\u00a0G\u00f6del numbers!”<\/p>\n

The “New” Observation<\/strong><\/span><\/p>\n

The above discussion leads to an obvious question:<\/p>\n

Is there also a proof of Rosser’s Theorem<\/em> that uses only Turing machines—analogous to the computer-scientist-friendly proof we just gave for the “original” Incompleteness Theorem?<\/strong><\/p>\n

My initial worry was that the answer would be no.\u00a0 For not only is Rosser’s sentence more complicated than\u00a0G\u00f6del’s, but it depends essentially on an ordering<\/em> of proofs—and it’s not clear what such an ordering would correspond to in the world of Turing machines.<\/p>\n

Why did this worry me?\u00a0 Because it threatened my conviction that computer programs are “really” at the core of G\u00f6del’s Theorem, whatever any tradition-minded philosopher or logician might claim to the contrary.\u00a0 If even the modest step from G\u00f6del to Rosser required abandoning the computability perspective, then my faith in the Almighty Turing Machine would be shaken.<\/p>\n

But never fear!\u00a0 A few months ago, I found a short, simple, Turing-machine-based proof of Rosser’s Theorem.\u00a0 While this seemed too small to write up as a paper, I’d never seen it before (please let me know if you have!)<\/del>, so I thought I’d share it here.\u00a0 (Update:<\/strong><\/span> Makoto Kanazawa points me to a basically-similar argument in Kleene’s 1967 textbook<\/a>.\u00a0 So, you can consider what follows to be a “popularization” of Kleene.)<\/p>\n

The first step is to define the following variant of the halting problem:<\/p>\n

The Consistent Guessing Problem<\/strong><\/p>\n

Given as input a description of a Turing machine M:<\/em><\/p>\n

    \n
  1. If M accepts on a blank tape, then accept.<\/em><\/li>\n
  2. If M rejects on a blank tape, then reject.<\/em><\/li>\n
  3. If M runs forever on a blank tape, then either accept or reject, but in any case, halt!<\/em><\/li>\n<\/ol>\n

    It’s easy to show that there’s no Turing machine to solve the Consistent Guessing Problem, by a modification (arguably, even a simplification) of Turing’s original argument for the halting problem.\u00a0 Indeed, I put the unsolvability of the Consistent Guessing Problem on last semester’s midterm, and at least half the students got it.\u00a0 (Damn!\u00a0 I guess I can’t use that one again.)<\/p>\n

    See it yet?\u00a0 No?\u00a0 Alright, so let P be a Turing machine that solves the Consistent Guessing Problem.\u00a0 Then we can easily modify P to produce an new Turing machine Q that, given as input a description \u27e8M\u27e9 of another Turing machine M:<\/p>\n