Explaining the Gentzen-Takeuti reduction steps: A second-order system (Q5944050)

This article continues the work of the author on deriving reduction steps as in Gentzen's second proof of the consistency of Peano Arithmetic [\textit{G. Gentzen}, ``Neue Fassung des Widerspruchsfreiheitsbeweises für die reine Zahlentheorie'', Forsch. Logik Grundlegung exakt. Wiss. N. F. 4, 19-44 (1938; Zbl 0019.24103)] on which the cut-elimination procedures of \textit{G. Takeuti} [Proof theory. 2nd ed. Amsterdam etc.: North-Holland (1987; Zbl 0609.03019)] and \textit{T. Arai} [``Consistency proof via pointwise induction'', Arch. Math. Logic 37, No. 3, 149-165 (1998; Zbl 0908.03052), and several unpublished manuscripts] is based. It continues previous work by the author [\textit{W. Buchholz}, ``Notation systems for infinitary derivations'', Arch. Math. Logic 30, No. 5/6, 277-296 (1991; Zbl 0726.03038), ``Explaining Gentzen's consistency proof within infinitary proof theory'', in: G. Gottlob (ed.) et al., Computational logic and proof theory. 5th Kurt Gödel Colloquium, KGC '97. Vienna, Austria. August 25-29, 1997. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 1289, 4-17 (1997; Zbl 0887.03043); ``Finitary treatment of operator controlled derivations'', Math. Log. Q. 47, No. 3, 363-396 (2001; Zbl 0986.03044)] and is related to independent work by \textit{G. E. Mints} [``Finite investigations of transfinite derivations'', J. Sov. Math. 10, 548-596 (1978; Zbl 0399.03044); the chapter ``Normalization of finite terms and derivations via infinite ones'' in his book: Selected papers in proof theory. Napoli: Bibliopolis. Amsterdam: North-Holland (1992; Zbl 0773.03038); ``A new reduction sequence for arithmetic'', J. Sov. Math. 20, 2322-2333 (1982; Zbl 0492.03021); ``A normal form for logical derivations implying one for arithmetic derivations'', Ann. Pure Appl. Logic 62, No. 1, 65-79 (1993; Zbl 0786.03040)]. The main motivation for the author is the desire to understand better the work of Arai, which is admired, but not yet well understood, by the proof-theoretic community. The principal method, Buchholz uses, is as follows: He first introduces an infinitary system and carries out cut elimination for it. Each lemma corresponds to a transformation of infinitary derivations, and an operator for this transformation is introduced. Next, he introduces a finitary system of derivation, by first formalizing the theory to be analysed and extending that system by formal symbols for all operators considered before. He determines for each derivation in these finitary systems the last rule of the corresponding infinitary derivation and for each of the possibly infinitely many premises of the infinitary derivation a finitary derivation. The last rule and the premises can be determined primitive recursively, provided one makes for certain steps use of the repetition rule (Rep), a rule which just repeats its premise. A derivation of a contradiction can only end in a repetition rule, and one can see now that the step from a conclusion of a Rep rule to the premise corresponds to steps similarly to those of Gentzen and Takeuti. A proof of the consistency is achieved, if one then assigns ordinals to all finitary derivations in such a way that the derivations of the premises of a rule (considered as finitary derivations) have smaller ordinals. In case of impredicative systems, one needs additionally (otherwise collapsing does not work) that the ordinals of the premises are essentially less than the conclusion relative to the index of the premise. If one then considers a proof of a contradiction, one sees that the premise of the repetition rule must be a proof of a contradiction with smaller ordinal, so the well-foundedness of the ordinal notation systems implies the consistency of the theory. In the article under review the author investigates what happens if one applies this approach to an impredicative system of second-order arithmetic \(\text{BI}^-_1\) of strength \(\text{ID}_1\). \(\text{BI}^-_1\) has second-order quantifiers, but the formation of \(\forall X.A\) and \(\exists X.A\) is only allowed if \(X\) is the only free predicate variable in \(A\) and \(A\) does not contain any second-order quantifiers. The logic of \(\text{BI}^-_1\) is second-order logic restricted to these formulas plus the induction schema. In the infinitary system, the author uses the \(\Omega\)-rule, introduced in his Habilitationsschrift (1977) and published and extended in Chapter IV of \textit{W. Buchholz, S. Feferman, W. Pohlers} and \textit{W. Sieg}'s book: Iterated inductive definitions and subsystems of analysis: recent proof-theoretical studies [Lecture Notes in Mathematics. 897. Berlin-Heidelberg-New York: Springer-Verlag (1981; Zbl 0489.03022)]. When applying the machinery, the reduction steps for a derivation ending with a collapsing rule with a premise having the \(\Omega\)-rule as last rule correspond to the reduction steps of Takeuti [loc. cit., pp. 327, 328, 339, 340]. The ordinal notation system used is that of \textit{M. Rathjen} and \textit{A. Weiermann} [``Proof-theoretic investigations on Kruskal's theorem'', Ann. Pure Appl. Logic 60, No. 1, 49-88 (1993; Zbl 0786.03042)]. This article is a typical Buchholz article: absolutely precise, without any gaps in the proofs, short and concise. As all his later articles, the current one is well motivated. The article under review is of highest standards -- unfortunately, one does not see such high quality papers often. With the connection of the early work of the author on the \(\Omega\)-rule with his recent research and the almost magic discovery of the reduction steps by Takeuti, this article is really a gem, crowning the work of the author's life. When reading the article one should however be aware that BI (Roman font) and \({\mathsf BI}\) (sans serif) have different meaning.