An Ordinal-Free Proof of the Cut-elimination Theorem for a Subsystem of $\Pi^1_1$-Analysis with $\omega$-rule (Proof theoretical study of the structure of logic and computation)
Ryota Akiyoshi · Institutional Repositories DataBase (IRDB) · 2009
The aim of this paper is to sketch our ideas of a simple ordinal-free proof of the cut-elimination theorem for a subsystem of $\Pi_{1}^{1}$ -analysis with $\omega$ -rule.The aim of this paper is to sketch our ideas of a simple ordinal-free proof of the cut-elimination theorem for a subsystem of $\Pi_{1}^{1}$ -analysis with $\omega$ -rule.The motivation is that use of heavy ordinal notation systems sometimes obscures our intuitive understanding of cut-elimination theorems.In the case of predicative systems, it is easy to understand why the cut-elimination procedure terminates.For example, the proof of the cut-elimination theorem for $PA$ with $\omega$ -rule proceeds by induction on cut-degree.But the matter is not very $tr\partial$ nsparent in the case of impredicative systems.Our proof of the cut-elimination theorem for a subsystem of $\Pi_{1}^{1}$ -analysis with w-rule proceeds just by transfinite induction on the height of a derivation.Moreover our proof involves only reasoning about well-founded trees.The present paper consists of 5 sections.After recalling basic definitions in section 1. we introduce $ii_{\grave{1}}fiiitary$ systems $BI_{0}^{\Omega},$ $BI_{1}^{\Omega}$ (section 2).$BI_{0}^{\Omega}$ is just cut-free arithmetic with $\omega$ -rule and Mints's "Repetition Rule".$BI_{1}^{\Omega}$ is obtained by adding cut-rule, a rule for second-order universal quantifier, and Buchholz's $\Omega,\tilde{\Omega}$ -rules to BI $0\Omega$ .In section 3 we define operators $\mathcal{R},$ $\mathcal{E}$ , and $\mathcal{E}_{\omega}$ on derivations in BI $\Omega 1$ .Moreover we define the collapsing operator $\mathcal{D}_{0}$ which eliminates $\tilde{\Omega}_{ eg\forall XA}$ .Finally we define the substitution operator $S_{T}^{\lambda^{r}}$ .In section 4 we introduce BIl-, which is a subsystem of $\Pi_{1}^{1}$ -analysis.BIl is obtained by adding $R_{A},$ $E,$ $E_{\omega},$ $D_{0},$ $Sub_{T}^{X}$ .These rules correspond to op- erations $\mathcal{R}$ .$\mathcal{E},$ $\mathcal{E}_{\omega},$ $D_{0}$ , and $S_{T}^{\lambda'}$ respectively.The idea of introducing these