{"id":697,"date":"2011-06-28T07:09:52","date_gmt":"2011-06-28T12:09:52","guid":{"rendered":"https:\/\/scottaaronson.blog\/?p=697"},"modified":"2017-01-12T18:41:00","modified_gmt":"2017-01-12T23:41:00","slug":"what-alan-t-did-for-his-phd","status":"publish","type":"post","link":"https:\/\/scottaaronson.blog\/?p=697","title":{"rendered":"What Alan T. did for his PhD"},"content":{"rendered":"

We’ve all been there before: by the time you start graduate school in Princeton, you’ve already invented the Turing machine, pioneered the concept of computational universality, and proved the unsolvability of Hilbert’s Entscheidungsproblem<\/em>.\u00a0 A few years from now, you’re going to return to England to make decisive contributions to the breaking of the Enigma and the winning of World War II.\u00a0 Your problem is, what do you do for the couple years in between?\u00a0 (Keep in mind that you have a PhD thesis<\/em> to submit, and the Turing machine is already old hat by now!)<\/p>\n

The answer, apparently, is to tackle a neat problem in logic, one version of which was asked three weeks ago<\/a> by a Shtetl-Optimized<\/em> commenter named Schulz.\u00a0 Not knowing the answer, I posted Schulz’s problem to MathOverflow<\/a>.\u00a0 There, Fran\u00e7ois Dorais and Philip Welch quickly informed me that Turing had already studied the problem in 1939, and Timothy Chow pointed me to Torkel Franzen’s book Inexhaustability: A Non-Exhaustive Treatment<\/a>, which explains Turing’s basic observation and the background leading up to it in a crystal-clear way.<\/p>\n

The problem is this: given any formal system F that we might want to take as a foundation for mathematics (for example, Peano Arithmetic or Zermelo-Fraenkel set theory), G\u00f6del tells us that there are Turing machines that run forever, but that can’t be proved<\/em> to run forever in F.\u00a0 An example is a Turing machine M that enumerates all the proofs in F one by one, and that halts if it ever encounters a proof of 0=1.\u00a0 The claim that M doesn’t halt is equivalent to the claim that F is consistent—but if F is indeed consistent, then the Second Incompleteness Theorem says that it can’t prove its own consistency.<\/p>\n

On the other hand, if we just add the reasonable axiom Con(F) (which asserts<\/em> that F is consistent), then our new theory, F+Con(F), can<\/em> prove that M runs forever.\u00a0 Of course, we can then construct a new Turing machine M’, which runs forever if and only if F+Con(F)<\/em> is consistent.\u00a0 Then by the same argument, F+Con(F) won’t be able to prove that M’ runs forever: to prove that, we’ll need a yet stronger theory, F+Con(F)+Con(F+Con(F)).\u00a0 This leads inevitably to considering an infinite tower of theories F0<\/sub>, F1<\/sub>, F2<\/sub>, …, where each theory asserts the consistency of the ones before it:<\/p>\n

F0<\/sub> = F<\/p>\n

Fi<\/sub> = Fi-1<\/sub> + Con(Fi-1<\/sub>) for all i\u22651<\/p>\n

But there’s no reason not to go further, and define another theory that asserts the consistency of every<\/em> theory in the above list, and then another theory that asserts the consistency of that<\/em> theory, and so on.\u00a0 We can formalize this using ordinals:<\/p>\n

F\u03c9<\/sub> = F + Con(F0<\/sub>) + Con(F1<\/sub>) + Con(F2<\/sub>) + …<\/p>\n

F\u03c9+i<\/sub> = F\u03c9+i-1<\/sub> + Con(F\u03c9+i-1<\/sub>) for all i\u22651<\/p>\n

F2\u03c9<\/sub> = F\u03c9<\/sub> + Con(F\u03c9<\/sub>) + Con(F\u03c9+1<\/sub>) + Con(F\u03c9+2<\/sub>) + …<\/p>\n

and so on, for every ordinal \u03b1 that we can define in the language of F.\u00a0 For every such ordinal \u03b1, we can easily construct a Turing machine M\u03b1<\/sub> that runs forever, but that can’t be proved<\/em> to run forever in F\u03b1<\/sub> (only in the later theories).\u00a0 The interesting question is, what happens if we reverse the quantifiers?<\/em> In other words:<\/p>\n

Given a Turing machine M that runs forever, is there always an ordinal \u03b1 such that F\u03b1<\/sub> proves that M runs forever?<\/strong><\/p>\n

This is the question Turing studied, but I should warn you that his answer is disappointing.\u00a0 It turns out that the theories F\u03b1<\/sub> are not as well-defined as they look.\u00a0 The trouble is that, even to define<\/em> a theory with infinitely many axioms (like F\u03c9<\/sub> or F2\u03c9<\/sub>), you need to encode the axioms in some systematic way: for example, by giving a Turing machine that spits out the axioms one by one.\u00a0 But Turing observes that the power of F\u03b1<\/sub> can depend strongly on which<\/em> Turing machine you use to spit out its axioms!\u00a0 Indeed, he proves the following theorem:<\/p>\n

Given any Turing machine M that runs forever, there is some “version” of F\u03c9+1<\/sub> (i.e., some way of encoding its axioms) such that F\u03c9+1<\/sub> proves that M runs forever.<\/strong><\/p>\n

The proof is simple.\u00a0 Assume for simplicity that F itself has only finitely many axioms (removing that assumption is straightforward).\u00a0 Then consider the following Turing machine P for outputting the axioms of F\u03c9<\/sub>, which gives rise to a “version” of F\u03c9<\/sub> that we’ll call FP<\/sub>:<\/p>\n

Output the axioms of F<\/p>\n

For t=0,1,2,…<\/p>\n

If M halts in t steps or fewer, then output “Con(FP<\/sub>)”; otherwise output “Con(Ft<\/sub>)”<\/p>\n

Next t<\/p>\n

You might notice that our description of P involves the very theory FP<\/sub> that we’re defining!\u00a0 What lets us get away with this circularity is the Recursion Theorem<\/a>, which says (informally) that when writing a program, we can always assume that the program has access to its own code.<\/p>\n

Notice that, if P ever output the axiom “Con(FP<\/sub>)”, then FP<\/sub> would assert its own consistency, and would therefore be in<\/em>consistent, by the Second Incompleteness Theorem.\u00a0 But by construction, P outputs “Con(FP<\/sub>)” if and only if M halts.\u00a0 Therefore, if we assume FP<\/sub>‘s consistency as an axiom, then we can easily deduce that M doesn’t<\/em> halt.\u00a0 It follows that the theory F\u03c9+1<\/sub> := FP<\/sub> + Con(FP<\/sub>) proves that M runs forever.<\/p>\n

One question that the above argument leaves open is whether there’s a Turing machine M that runs forever, as well as a system S of ordinal notations “extending as far as possible”, such that if<\/em> we use S to define the theories F\u03b1<\/sub>, then<\/em> none of the F\u03b1<\/sub>‘s prove that M runs forever.\u00a0 If so, then there would be a clear sense in which iterated consistency axioms, by themselves, do not<\/em> suffice to solve the halting problem.\u00a0 Alas, I fear the answer might depend on exactly how we interpret the phrase “extending as far as possible” … elucidation welcome!<\/p>\n

Update (June 29, 2011):<\/span><\/strong> In a comment, Fran\u00e7ois Dorais comes to the rescue once again:<\/p>\n

In connection with your last paragraph, Feferman has shown that there are paths through O such that the resulting theory proves all true \u220f0<\/sup>1<\/sub> statements. [JSL 27 (1962), 259-316] Immediately after Feferman and Spector showed that not all paths through O do this. [JSL 27 (1962), 383-390] In particular, they show that any good path must be more complicated than O itself: the path cannot be \u220f1<\/sup>1<\/sub>. In other words, there is no simple way to form a wellordered iterated consistency extension that captures all true \u220f0<\/sup>1<\/sub> statements.<\/p>\n","protected":false},"excerpt":{"rendered":"

We’ve all been there before: by the time you start graduate school in Princeton, you’ve already invented the Turing machine, pioneered the concept of computational universality, and proved the unsolvability of Hilbert’s Entscheidungsproblem.\u00a0 A few years from now, you’re going to return to England to make decisive contributions to the breaking of the Enigma and […]<\/p>\n","protected":false},"author":1,"featured_media":0,"comment_status":"closed","ping_status":"closed","sticky":false,"template":"","format":"standard","meta":{"advanced_seo_description":"","jetpack_seo_html_title":"","jetpack_seo_noindex":false,"jetpack_seo_schema_type":"","_jetpack_newsletter_access":"","_jetpack_dont_email_post_to_subs":false,"_jetpack_newsletter_tier_id":0,"_jetpack_memberships_contains_paywalled_content":false,"_jetpack_feature_clip_id":0,"_jetpack_memberships_contains_paid_content":false,"footnotes":"","jetpack_publicize_message":"{title}\n\n{excerpt}\n\n{url}","jetpack_publicize_feature_enabled":true,"jetpack_social_post_already_shared":false,"jetpack_social_options":{"image_generator_settings":{"template":"highway","default_image_id":0,"font":"","enabled":false},"version":2},"_wpas_customize_per_network":false,"jetpack_post_was_ever_published":false},"categories":[11,32],"tags":[],"class_list":["post-697","post","type-post","status-publish","format-standard","hentry","category-nerd-interest","category-planetmo"],"jetpack_publicize_connections":[],"jetpack_featured_media_url":"","jetpack_sharing_enabled":true,"_links":{"self":[{"href":"https:\/\/scottaaronson.blog\/index.php?rest_route=\/wp\/v2\/posts\/697","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/scottaaronson.blog\/index.php?rest_route=\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/scottaaronson.blog\/index.php?rest_route=\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/scottaaronson.blog\/index.php?rest_route=\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/scottaaronson.blog\/index.php?rest_route=%2Fwp%2Fv2%2Fcomments&post=697"}],"version-history":[{"count":5,"href":"https:\/\/scottaaronson.blog\/index.php?rest_route=\/wp\/v2\/posts\/697\/revisions"}],"predecessor-version":[{"id":703,"href":"https:\/\/scottaaronson.blog\/index.php?rest_route=\/wp\/v2\/posts\/697\/revisions\/703"}],"wp:attachment":[{"href":"https:\/\/scottaaronson.blog\/index.php?rest_route=%2Fwp%2Fv2%2Fmedia&parent=697"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/scottaaronson.blog\/index.php?rest_route=%2Fwp%2Fv2%2Fcategories&post=697"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/scottaaronson.blog\/index.php?rest_route=%2Fwp%2Fv2%2Ftags&post=697"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}