Iterated local reflection versus iterated consistency (Q1899141)

If you add the sentence `\(T\) is consistent' to a theory \(T\) (large enough), you get a theory \(T'\) larger than \(T\). Repeating this transfinitely often you produce a transfinite progression \((T_\alpha)\), basing on iteration of consistency. If \(\alpha\) is chosen from a recursive notation system, this progression is called recursive. If the same procedure is performed using the so-called local reflection principle instead of consistency, another progression \((T^\alpha)\) is gained. In this case every step consists of adding the formulas \(\text{Pr}_T (\ulcorner A \urcorner) \to A\) as axioms to \(T\) for every sentence \(A\) of the language of \(T\), \(\text{Pr}_T\) being the provability predicate for \(T\). Starting from \textit{A. Turing}'s fundamental work [Proc. Lond. Math. Soc., II. Ser. 45, 161-228 (1939; Zbl 0021.09704)], \textit{S. Feferman} considered such progressions in J. Symb. Log. 27, 259-316 (1963; Zbl 0117.25402). Already Turing stated and Feferman pointed out precisely that the ordinals used cannot be taken from an arbitrary stock. The progressions depend on the chosen recursive description of the underlying well-ordering. Moreover the numeration of the axioms of the theories affects the progression. Connections between the different kinds of iterations can be found in papers of \textit{G. Kreisel} and \textit{A. Lévy} [Z. Math. Logik Grundlagen Math. 14, 97-142 (1968; Zbl 0167.01302)], \textit{S. N. Artemov} [Vopr. Kibern., Mosk. 75, 3-22 (1982; Zbl 0499.03046)], and \textit{S. V. Goryachev} [Mat. Zametki 40, No. 5, 561-571 (1986; Zbl 0632.03044)]. In the present paper the following precise relations are proven to hold under certain conditions: \[ (T^\alpha)_\beta \equiv_{\Pi^0_1} T_{\omega^\alpha (1 + \beta)}, \quad (T^\beta)_\alpha \equiv_{\Pi^0_1} T_{\beta + \omega^\alpha} \tag{*} \] where \(\equiv_{\Pi^0_1}\) means that in both theories the same \(\Pi^0_1\)-formulas are provable. To express the restrictions on (*), the author defines the concepts of a smooth numeration (of axioms) and of nice well-orderings. This is the real proof-theoretical importance of the paper. In smooth numerations the axioms added to \(T\) succeed the axioms of \(T\) provably in PRA. In nice well-orderings the usual functions for ordinals, \(+, \cdot\), and \(\omega^x\), are represented by primitive recursive terms and it can be proven in PRA that they possess the usual properties. The proof of (*) for such numerations and well-orderings is rather straightforward by nested transfinite induction. It is remarkable that for the proof of the induction basis for one part of (*), following Goryachev [loc. cit.], a valid formula of propositional modal logic is interpreted as a statement of provability in \(T\). This procedure can be formalized in PRA. A corollary of (*) is the following: If \((T^\alpha)\) and \((T_\alpha)\) are based on a nice well-ordering and on a smooth numeration, then, for \(\alpha > 0\), \(T^\alpha \equiv_{\Pi^0_1} T_{\omega^\alpha}\), and thus, just for \(\varepsilon\)-numbers \(\alpha\), \(T^\alpha \equiv_{\Pi^0_1} T_\alpha\). As appendix a theory of nice well-orderings is specified.