An extension of the omega-rule

Ryota Akiyoshi, Grigori Mints

Research output: Contribution to journalArticle

3 Citations (Scopus)

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 ID1) 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 languageEnglish
Pages (from-to)593-603
Number of pages11
JournalArchive for Mathematical Logic
Volume55
Issue number3-4
DOIs
Publication statusPublished - 2016 May 1

    Fingerprint

Keywords

  • Cut-elimination
  • Infinitary proof theory
  • Ordinal analysis

ASJC Scopus subject areas

  • Logic
  • Philosophy

Cite this