Analysis and Extension of Omega-Rule

MaRDI QIDQ6213733zbMATH OpenFDO

Authors Ryota Akiyoshi, G. E. Mints

Publication date 30 April 2009

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05)

Abstract: $Omega$-rule was introduced by W. Buchholz to give an ordinal-free cut-elimination proof for a subsystem of analysis with $P{i}_1^1$-comprehension. His proof provides cut-free derivations by familiar rules only for arithmetical sequents. When second-order quantifiers are present, they are introduced by $Omega$-rule and some residual cuts are not eliminated. Using an extension of $Omega$-rule we obtain (by the same method as W. Buchholz) complete cut-elimination: any derivation of arbitrary sequent is transformed into its cut-free derivation by the standard rules (with induction replaced by $omega$-rule). W. Buchholz used $Omega$-rule to explain how reductions of finite derivations (used by G. Takeuti for subsystems of analysis) are generated by cut-elimination steps applied to derivations with $Omega$-rule. We show that the same steps generate standard cut-reduction steps for infinitary derivations with familiar standard rules for second-order quantifiers. This provides an analysis of $Omega$-rule in terms of standard rules and ordinal-free cut-elimination proof for the system with the standard rules for second-order quantifiers. In fact we treat the subsystem of $P{i}_1^1$-CA (of the same strength as $I{D}_1$) that W. Buchholz used for his explanation of finite reductions. Extension to full $P{i}_1^1$-CA is forthcoming in another paper.

This page was built for publication: Analysis and Extension of Omega-Rule

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6213733)