Supplement to Proof Theory

B. Turing’s and Feferman’s Results on Recursive Progressions

We will give a proof of Turing’s completeness Theorem 5.2 to be able to discuss its scope. Moreover, we shall also look at Feferman’s much stronger result about progressions based on the uniform reflection principle. As to the hierarchies that have been studied most frequently, please refer to section 5.2. The existence of primitive recursive functions nψn in the definition of the different progressions is an easy consequence of the primitive recursion theorem.[49] If all axioms of T a true (in the standard model) it can be shown for all aO by transfinite induction on |a| that Ta is a true theory (in a sufficiently strong metatheory). For numbers a outside O the theories Ta bear no interest. They may actually be inconsistent. For example, the recursion theorem ensures that there exists an e such that {e}(0)=suc(lim(e)). As T{e}(0)Tlim(e) and T{e}(0) proves the consistency of Tlim(e), both theories are inconsistent.

Recall that Turing’s completeness result, Theorem 5.2, asserts that for any true Π10 sentence ϕ a number aϕO with |aϕ|=ω+1 can be constructed such that Taϕϕ. Moreover, the function ϕaϕ is primitive recursive. The proof proceeds as follows: Let θ be xψ(x) with ψ primitive recursive. Define e by the recursion theorem such that, provably in PA,

{e}(n)={nOif ψ(k¯) is true for every knsuc(lim(e))otherwise.

Note that {e} is total (by induction on n). As θ is true, we have {e}(n)=nO for all n. Thus lim(e) belongs to O and |lim(e)|=ω. We claim that the consistency of Tlim(e) entails that θ is true. For if θ were false we would have ¬ψ(m¯) for some m and thus T{e}(n)=Tsuc(lim(e)) for all nm. But, by design, Tsuc(lim(e)) proves the consistency of Tlim(e) and T{e}(n) is a subtheory of Tlim(e) for all n. Thus Tlim(e) would prove its own consistency, rendering it inconsistent (by Gödel’s second incompleteness theorem). The foregoing reasoning can be formalized in PA and a fortiori in Tsuc(lim(e)). As a result, Tsuc(lim(e))θ.

This proof is based on the trick of coding the truth of θ as a member of O. It shows that the infinitely many iterated consistency axioms Con(T0),Con(T1), of Tsuc(lim(e)) play no role in proving θ. The reason why one has to go to stage ω+1 is simply that only at stage ω a non-standard definition of the axioms of n<ωTn can be introduced. And actually a non-standard definition of the axioms of T0 would serve the same purpose. Setting ϑ(v0):⇔ψ(v0)(x¬ψ(x)v0=0=1), the theory T0 defined by the Σ10-formula ϑ has the same axioms as T0, but the consistency of T0 implies θ (provably so in PA). Also note that epistemologically recognizing that suc(lim(e)) is in O hinges on us knowing that θ is true, and hence nothing is gained by further knowing that Tsuc(lim(e))θ.

The proof of the Theorem 5.2 works with any consistency progression. Turing actually considered slightly stronger progressions in that he used a special version of local reflection progressions, where (R2) is restricted to Π20-sentences, i.e., sentences of form with primitive recursive matrix. He took as one of his main aims to show that these progressions are complete for Π20-sentences. However, this is not the case as we have shown.

Theorem B.1 Let (Ta)aO be a progression based on the local reflection principle. Then the following hold:

  1. aOTaT0+ all true Π10-sentences.
  2. There is a true Π20-sentence that is not provable in aOTa.

Proof: Let T:=T0+all true Π10-sentences.

  1. We show by induction on aO that TaT. Only the successor step needs to be looked at. So suppose a=suc(b) and TbT. It suffices to show that TPrTb(ϕ)ϕ holds for every sentence ϕ. There are two cases to consider. If PrTb(ϕ) is false then ¬PrTb(ϕ) is a true Π10-sentence and hence T¬PrTb(ϕ) which entails TPrTb(ϕ)ϕ. If PrTb(ϕ) is true then Tbϕ and, by the induction hypothesis, Tϕ which also yields TPrTb(ϕ)ϕ.
  2. The provability predicate for T is of complexity Σ20. If aOTa proved all true Π20-sentences then T would be Π20-complete. But that is absurd on account of the arithmetical hierarchy theorem.

The problem left open after Turing’s thesis, namely whether any stronger progressions can be complete for Π20-statements, was addressed by Feferman (1962) with the surprising result that progressions based on the uniform reflection principle were not only complete with respect to Π20-sentences but for all arithmetical sentences.

Theorem B.2 (Feferman’s completeness theorem 1962) Let (Ta)aO be a progression based on the uniform reflection principle with T0=PA.

For any true arithmetical sentence θ there exists aO such that Taθ. Moreover, aO can be chosen such that |a|<ωωω+1.

In contrast to Turing’s result, Theorem 5.2, the proof of B.2 is rather difficult; it also utilizes a theorem from Shoenfield 1959 stating that Peano arithmetic with the recursive ω-rule is complete for arithmetical statements.[50] However, as far as mathematical knowledge is concerned, the same circularity as in Turing’s completeness theorem obtains in Theorem B.2 in that recognizing an aO with Taψ is at least as hard as recognizing that ψ is true. The starting point for constructing such an aO therefore is the truth of ψ and as in Turing’s theorem one proceeds to cook up a via an application of the primitive recursion theorem, albeit this time a very intricate one.

Copyright © 2024 by
Michael Rathjen <rathjen@maths.leeds.ac.uk>
Wilfried Sieg <sieg@cmu.edu>

Open access to the SEP is made possible by a world-wide funding initiative.
The Encyclopedia Now Needs Your Support
Please Read How You Can Help Keep the Encyclopedia Free