Analysis and Extension of Omega-Rule

R. Akiyoshi, G. Mints

$\Omega$-rule was introduced by W. Buchholz to give an ordinal-free cut-elimination proof for a subsystem of analysis with ${\Pi }_1^1$-comprehension. His proof provides cut-free derivat…