Valentini's cut-elimination for provability logic resolved

In 1983, Valentini presented a syntactic proof of cut-elimination for a sequent calculus GLSV for the provability logic GL where we have added the subscript V for "Valentini". The sequents in GLSV were built from sets, as opposed to multisets, thus avoiding an explicit contraction rule. From a syntactic point of view, it is more satisfying and formal to explicitly identify the applications of the contraction rule that are `hidden' in these set-based proofs of cut-elimination. There is often an underlying assumption that the move to a proof of cut-elimination for sequents built from multisets is easy. Recently, however, it has been claimed that Valentini's arguments to eliminate cut do not terminate when applied to a multiset formulation of GLSV 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 argum...

• Type: Conference
• Year: 2008
• Where: AIML
• Authors: Rajeev Goré, Revantha Ramanayake
• Keywords: AIML 2008, Contraction Rules, Logical Reasoning, Sequents, Valentini's Arguments