Cut elimination for a logic with induction and co-induction (Q1948276): Difference between revisions

The aim of the paper is to present a sequent calculus Linc\(^-\) with induction and co-induction rules based on a proof-theoretic notion of definition due to Hallnas and Schroeder-Heister. It comprises the core fragment of the intuitionistic version of Church's simple theory of types and allows reasoning about properties of computational systems. However, this paper is not concerned with the applications of Linc\(^-\) but with a detailed proof of cut eliminability for this system based on the parametric reducibility technique due to Girard. In Section 2, the sequent calculus for \(\mathrm{Linc}^-\) is introduced. Except having induction and co-induction rules, it has the special feature that each sequent carries a typing context for eigenvariables, called the signature of the sequent. Although the use of signatures simplifies precise accounting for empty types, it is not well suited for proving cut elimination. To avoid the difficulties, in Section 3 the intermediate system \(\mathrm{Linc}_i^-\) is introduced, in which signatures are implicit. After the presentation of some transformations of derivations in \(\mathrm{Linc}_i^-\), it is shown in Section 5 that cut (or rather multicut) is eliminable. Cut elimination for \(\mathrm{Linc}^-\) is proved indirectly in Section 6 by showing that cut reduction steps preserve the operation of `decoration' derivations in \(\mathrm{Linc}_i^-\) with signatures. Finally, some comparisons with other approaches are suggested. The paper is strongly technical, but the proof of cut elimination is presented very carefully and readable with details added in two appendices. It may be of interest for researchers in Gentzen's proof theory.