[FOM] The recursive omega rule

[Torkel Franzen]

  I have a couple of questions that may have some foundational interest,
concerning the literature on the recursive omega rule.

  The recursive omega rule is an infinitary rule of inference, whereby
(x)A(x) follows from A(0),A(1),... whenever there is a recursive
function F such that F(n) is (encodes) a proof of A(n) for every
n. Shoenfield proved, in "On a restricted w-rule", 1959, that
arithmetic with this rule of inference is complete. The new ingredient
in his paper was a proof that, essentially, the recursive omega rule
can prove any arithmetical well-ordering to be a well-ordering. He
obtains his completeness result by combining this with theorem 5 in §6
of "Number theoretic concepts and recursive well-orderings" by
Kreisel, Shoenfield, and Wang.  This theorem is a proof-theoretic
version of the earlier result by Kleene that an arithmetical sentence
A is true iff a certain provably total primitive recursive ordering
constructed from A is a well-ordering: for any sentence A of
arithmetic, we can define a provably total arithmetical ordering
relation R such that R is a well-ordering if A is true, and for a
particular term t(x) (in an extension by definitions of arithmetic),

            (Ex)~R(t(x+1),t(x)) -> A

is arithmetically provable. (Thus if A is false, we get a definable
infinitely R-descending sequence.)

  The number of applications of the recursive omega rule used to 
prove A is the ordinal of the ordering R. Shoenfield says in
his paper that "the above proof with the considerations of [the
Kreisel-Shoenfield-Wang paper]" shows that at most w^w applications
are needed." The reference is to a theorem in the Kreisel-Shoenfield-Wang
paper that a certain relation R is a well-ordering iff A is true,
where the ordinal of R is smaller than w^w.

  Now, it is common to refer to Shoenfield's completeness theorem for
the recursive w-rule together with this bound w^w. In particular, this
is done in Feferman's paper on progressions. However, in the
Kreisel-Shoenfield-Wang paper the proof-theoretic result is not in
fact established for the w^w-bounded relation R. Instead it is stated
in a footnote to theorem 5 of §6 that using the w^w-bounded relation
"would complicate the proofs considerably, and have little value" -
this because no ordinal bounds enter into the formulation of theorem
5.  Shoenfields comment, however, presupposes that a proof of theorem 5
can be carried through using this R.

  Thus my first question is: is there anywhere in the literature a proof
of (a result corresponding to) theorem 5 using an w^w-bounded relation,
or has it just been accepted that such a proof can be carried out?

  The actual proof of theorem 5 in the Kreisel-Shoenfield-Wang paper
uses the Brouwer-Kleene ordering restricted to the set of sequence
numbers unsecured with respect to a certain relation. This proof, if
correct, suffices for Shoenfield's proof of the completeness of the
recursive w-rule to go through. Here my problem is that I can't see
that the proof is correct.

  To check the proof, consider a statement A of the form (Ex)(y)(Ez)F(x,y,z)
with F primitive recursive. By Skolemization, A is true iff
(g)(Ex)(Ez)F(x,g(x),z) is true. Lemma 9 of §6 of the paper observes
that we can define a relation D1 such that

          (Ex)(Ez)F(x,g(x),z) <-> (Ex)D1(x,t(x))

is arithmetically provable for a certain term t(x). Specifically, t(x)
is g((x)_0), using a coding of pairs of numbers for which x encodes
the pair <(x)_0,(x)_1>, and D1(x,y) is F((x)_0,y,(x)_1).

  In the proof of theorem 5, R is defined as the Brouwer-Kleene
ordering restricted to the unsecured sequence numbers s, where s
is unsecured if ~D(x,(s)_x) holds for every x smaller than the
length of s, and (s)_x is the x-th number in the sequence encoded by s.

  Now here is my objection to the argument. If this relation R is
well-founded, there is no g for which (x)~D1(x,g(x)). But this means
that (g)(Ex)F((x)_0,g(x),(x)_1), which implies (Ex)(Ez)(y)F(x,y,z).
So it doesn't hold in general that R is well-founded if A is true.
And indeed looking at the proof of theorem 5, the line "From this we
obtain ~C by Lemmas 9 and 7" (p.61) has no apparent justification.

  Thus my second question is whether the gap in the proof is in fact
there (or am I confused?), and if is there, whether there is some
obvious fix of the proof of theorem 5, or some other argument in or
based on the literature which establishes the result used in
Shoenfield's completeness proof (quite apart from the bound w^w).

---
Torkel Franzen