Recursive \(\omega\)-rule for proof systems (Q1119627)

By using the result of \textit{E. G. K. Lopez-Escobar} [Stud. Logic Found. Math. 89, 75--97 (1977; Zbl 0386.03026)] that if there is an effective disjunctor on a formal Carnap theory \({\mathcal F}\), then \({\mathcal F}^{\infty}\) is a conservative extension of \({\mathcal F}^{\infty}_{rec}\), this author shows that infinitary rules in most proof systems in computer science can be restricted to recursive ones.