Valentini's cut-elimination for provability logic resolved

Date

2012

Authors

Gore, Rajeev
Ramanayake, Revantha

Journal Title

Journal ISSN

Volume Title

Publisher

Cambridge University Press

Abstract

Valentini (1983) has presented a proof of cut-elimination for provability logic GL for a sequent calculus using sequents built from sets as opposed to multisets, thus avoiding an explicit contraction rule. From a formal point of view, it is more syntactic and satisfying to explicitly identify the applications of the contraction rule that are 'hidden' in proofs of cut-elimination for such sequent calculi. There is often an underlying assumption that the move to a proof of cut-elimination for sequents built from multisets is straightforward. Recently, however, it has been claimed that Valentini's arguments to eliminate cut do not terminate when applied to a multiset formulation of the calculus with an explicit rule of contraction. The claim has led to much confusion and various authors have sought new proofs of cut-elimination for GL in a multiset setting. Here we refute this claim by placing Valentini's arguments in a formal setting and proving cut-elimination for sequents built from multisets. The use of sequents built from multisets enables us to accurately account for the interplay between the weakening and contraction rules. Furthermore, Valentini's original proof relies on a novel induction parameter called width which is computed 'globally'. It is difficult to verify the correctness of his induction argument based on width. In our formulation however, verification of the induction argument is straightforward. Finally, the multiset setting also introduces a new complication in the case of contractions above cut when the cut-formula is boxed. We deal with this using a new transformation based on Valentini's original arguments. Finally, we discuss the possibility of adapting this cut-elimination procedure to other logics axiomatizable by formulae of a syntactically similar form to the GL axiom.

Description

Keywords

Citation

Source

Review of Symbolic Logic

Type

Journal article

Book Title

Entity type

Access Statement

License Rights

Restricted until

2037-12-31