Shtetl-Optimized

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.  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.  Your problem is, what do you do for the couple years in between?  (Keep in mind that you have a PhD thesis to submit, and the Turing machine is already old hat by now!)

The answer, apparently, is to tackle a neat problem in logic, one version of which was asked three weeks ago by a Shtetl-Optimized commenter named Schulz.  Not knowing the answer, I posted Schulz’s problem to MathOverflow.  There, François 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, which explains Turing’s basic observation and the background leading up to it in a crystal-clear way.

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ödel tells us that there are Turing machines that run forever, but that can’t be proved to run forever in F.  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.  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.

On the other hand, if we just add the reasonable axiom Con(F) (which asserts that F is consistent), then our new theory, F+Con(F), can prove that M runs forever.  Of course, we can then construct a new Turing machine M’, which runs forever if and only if F+Con(F) is consistent.  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)).  This leads inevitably to considering an infinite tower of theories F₀, F₁, F₂, …, where each theory asserts the consistency of the ones before it:

F₀ = F

F_i = F_i-1 + Con(F_i-1) for all i≥1

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

F_ω = F + Con(F₀) + Con(F₁) + Con(F₂) + …

F_ω+i = F_ω+i-1 + Con(F_ω+i-1) for all i≥1

F_2ω = F_ω + Con(F_ω) + Con(F_ω+1) + Con(F_ω+2) + …

and so on, for every ordinal α that we can define in the language of F.  For every such ordinal α, we can easily construct a Turing machine M_α that runs forever, but that can’t be proved to run forever in F_α (only in the later theories).  The interesting question is, what happens if we reverse the quantifiers? In other words:

Given a Turing machine M that runs forever, is there always an ordinal α such that F_α proves that M runs forever?

This is the question Turing studied, but I should warn you that his answer is disappointing.  It turns out that the theories F_α are not as well-defined as they look.  The trouble is that, even to define a theory with infinitely many axioms (like F_ω or F_2ω), 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.  But Turing observes that the power of F_α can depend strongly on which Turing machine you use to spit out its axioms!  Indeed, he proves the following theorem:

Given any Turing machine M that runs forever, there is some “version” of F_ω+1 (i.e., some way of encoding its axioms) such that F_ω+1 proves that M runs forever.

The proof is simple.  Assume for simplicity that F itself has only finitely many axioms (removing that assumption is straightforward).  Then consider the following Turing machine P for outputting the axioms of F_ω, which gives rise to a “version” of F_ω that we’ll call F_P:

Output the axioms of F

For t=0,1,2,…

If M halts in t steps or fewer, then output “Con(F_P)”; otherwise output “Con(F_t)”

Next t

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

Notice that, if P ever output the axiom “Con(F_P)”, then F_P would assert its own consistency, and would therefore be inconsistent, by the Second Incompleteness Theorem.  But by construction, P outputs “Con(F_P)” if and only if M halts.  Therefore, if we assume F_P‘s consistency as an axiom, then we can easily deduce that M doesn’t halt.  It follows that the theory F_ω+1 := F_P + Con(F_P) proves that M runs forever.

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 we use S to define the theories F_α, then none of the F_α‘s prove that M runs forever.  If so, then there would be a clear sense in which iterated consistency axioms, by themselves, do not suffice to solve the halting problem.  Alas, I fear the answer might depend on exactly how we interpret the phrase “extending as far as possible” … elucidation welcome!

Update (June 29, 2011): In a comment, François Dorais comes to the rescue once again:

In connection with your last paragraph, Feferman has shown that there are paths through O such that the resulting theory proves all true ∏⁰₁ 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 ∏¹₁. In other words, there is no simple way to form a wellordered iterated consistency extension that captures all true ∏⁰₁ statements.

Follow