No label defined (Q4386982)

This paper is a revised English version of an article which originally appeared in Russian [cf. Set theory and topology, No. 1, Interuniv. Work. Collect., Izhevsk 1977, 27-36 (1977; Zbl 0483.03038)]. The author introduces a sequent calculus for second order arithmetic with \(\omega\)-rule, where second order variables range over definable sets of natural numbers. Formally, this means that the sequent calculus has an infinitary rule which allows to infer \(\forall X A(X)\) whenever \(A(T)\) is derivable for each closed second order term \(T\). The main result is a non-constructive cut-elimination theorem for the calculus (whence consistency); the proof adapts Takahashi's method of completing semivaluations and uses the constructibility axiom, \(V=L\), in order to get a sound interpretation of the infinitary inference rule for universal set quantification. The paper is neatly written. It would be interesting to know if there are applications of the main theorem to other branches to mathematical logic.