An extension of the omega-rule (Q283132)

In this paper, the extension of the \(\Omega\)-rule introduced by \textit{W. Buchholz} [``The \(\Omega_{\mu +1}\)-rule'', Lect. Notes Math. 897, 188--233 (1981; \url{doi:10.1007/BFb0091898})] is presented which allows for the proof of cut elimination for a subsystem of analysis with \(\Pi^1_1\)-comprehension. The first constructive proof of cut elimination for \(\Pi^1_1\)-analysis was provided by \textit{G. Takeuti} [Ann. Math. 86, No. 2, 299--348 (1967; Zbl 0159.00905)]. This proof, and other similar provided by Arai, Buchholz, Howard and Pohlers, are based on complicated ordinal notations (like ordinal diagrams). The \(\Omega\)-rule of Buchholz allowed him to prove ordinal-free partial cut elimination for a subsystem of analysis with parameter-free \(\Pi^1_1\)-comprehension. However, in the presence of second-order quantifiers, some residual cuts are not eliminable in Buchholz' approach. The authors provide a modification which allows for complete cut elimination from proofs of arbitrary sequents, not only arithmetical ones. It uses a technique of Takeuti of labelling formulas as explicit (traceable to end-sequent) or implicit (traceable to cut-formulas). In Section 2, the target system BI is presented which is a parameter-free subsystem of \(\Pi^1_1\)-analysis with \(\Omega\)-rule. In Section 3, the system BI\(^{\Omega+}\) with extended \(\Omega\)-rule and formulas labelled as explicit/implicit is introduced. For this system, cut elimination is constructively proved. Finally, by means of embedding a function from BI to BI\(^{\Omega+}\) it is demonstrated that any proof in BI is translatable into a cut-free proof. The method was also sucessfully applied by the second author [Stud. Log. 100, No. 1--2, 279--287 (2012; Zbl 1254.03110)] to subsystems of modal \(\mu\)-calculus, and by the first author [``Complete cut-elimination theorem for \(\Omega_{\mu +1}\)-rule'', Preprint; ``An ordinal-free proof of the complete cut-elimination theorem for \(\Pi^1_1\)-CA + BI with the \(\omega\)-rule'', Preprint] to \(\Pi^1_1\)-analysis with bar induction and \(\Omega\)-rule.