[FOM] Consistency of formal systems

[Torkel Franzen]

Bill Tait said, in a message posted earlier this summer:

  >Turing, Feferman and Fenstad have 
  >written on such hierarchies of theories; but I don't remember the 
  >details. I think that Feferman gave a bound on how high such a 
  >hierarchy could go and then Fenstad improved on it (?)

  I commented earlier that Fenstad's proof was known to be incorrect.
However, it seems that this fact is known only in folklore, and that
no retraction or correction has been published in the logical
literature - more precisely, I haven't found any such, but stand ready
to be corrected. Since the completeness results (by Turing and
Feferman) for progressions of theories often crop up in foundational
discussions, it may be of interest to have on record an indication of
an error in the argument.

  Fenstad's paper is "On the completeness of some transfinite
recursive progressions of axiomatic theories", JSL 31, number 1, March
1968.  Feferman's completeness proof used Shoenfield's result
concerning the completeness of the recursive omega-rule. Fenstad's
idea was to eliminate the use of Shoenfield's result by giving a
direct proof by induction on n that every true Pi-0-n statement is
provable in some theory T_a in a progression, also obtaining in this
way a new and simpler proof of Shoenfield's result and a sharper bound
on the ordinal denoted by a. The main step of the proposed proof is
presented in §4 of his paper.

Consider a true statement (x)(Ey)(z)P(x,y,z) with P primitive recursive
(the case of at most two quantifiers having been covered by reference
to results in Feferman's paper). For every m there is a k such that
(z)P(m,k,z) is provable in T_G(m,k), where G is primitive recursive,
and G(m,k) is in O if (z)P(m,k,z) is true. Fenstad now invokes a
lemma from Feferman's paper, that given a recursive F such that
F(m) is in O for every m, a notation a can be constructed for which
everything provable in some T_F(m) is provable in T_a. Applying this
to an index (with m as parameter) for the function mapping k to G(m,k)
yields a notation a (with m as parameter) for which everything
provable in some T_G(m,k) is provable in T_a. But Feferman's lemma is
not applicable, since it is not the case, unless (y)(z)P(m,y,z) is true,
that G(m,k) is in O for every k.

---
Torkel Franzen