## Abstract

The Ω -rule was introduced by W. Buchholz to give an ordinal-free proof of cut-elimination for a subsystem of analysis with ^{Π 1 1}-comprehension. W. Buchholz’s proof provides cut-free derivations by familiar rules only for arithmetical sequents. When second-order quantifiers are present, they are introduced by the Ω -rule and some residual cuts are not eliminated. In the present paper, we introduce an extension of the Ω -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 ω-rule). In fact we treat the subsystem of ^{Π 1 1}-CA (of the same strength as I_{D1}) that W. Buchholz used for his explanation of G. Takeuti’s finite reductions. Extension to full ^{Π 1 1}-CA is planned for another paper.

Original language | English |
---|---|

Pages (from-to) | 593-603 |

Number of pages | 11 |

Journal | Archive for Mathematical Logic |

Volume | 55 |

Issue number | 3-4 |

DOIs | |

Publication status | Published - 2016 May 1 |

## Keywords

- Cut-elimination
- Infinitary proof theory
- Ordinal analysis

## ASJC Scopus subject areas

- Logic
- Philosophy