Name
Abstract | ||
|---|---|---|
The $$Omega $$Ω-rule was introduced by W. Buchholz to give an ordinal-free proof of cut-elimination for a subsystem of analysis with $$Pi ^{1}_{1}$$?11-comprehension. W. Buchholzu0027s proof provides cut-free derivations by familiar rules only for arithmetical sequents. When second-order quantifiers are present, they are introduced by the $$Omega $$Ω-rule and some residual cuts are not eliminated. In the present paper, we introduce an extension of the $$Omega $$Ω-rule and prove the complete cut-elimination by the same method as W. Buchholz: any derivation of arbitrary sequent is transformed into its cut-free derivation by the standard rules (with induction replaced by the $$omega $$?-rule). In fact we treat the subsystem of $$Pi ^{1}_{1}$$?11-CA (of the same strength as $$ID_{1}$$ID1) that W. Buchholz used for his explanation of G. Takeutiu0027s finite reductions. Extension to full $$Pi ^{1}_{1}$$?11-CA is planned for another paper. |
Year | DOI | Venue |
|---|---|---|
2016 | 10.1007/s00153-016-0482-y | Arch. Math. Log. |
Keywords | Field | DocType |
Cut-elimination, Infinitary proof theory, Ordinal analysis, 03F05, 03F35 | Discrete mathematics,Combinatorics,Arithmetic function,Ordinal analysis,Omega,Sequent,Mathematics | Journal |
Volume | Issue | ISSN |
55 | 3-4 | 1432-0665 |
Citations | PageRank | References |
2 | 0.44 | 4 |
Authors | ||
2 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Ryota Akiyoshi | 1 | 4 | 1.90 |
| Grigori Mints | 2 | 235 | 72.76 |