Valentini's cut-elimination for provability logic resolved
| Abstract | 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 underly ing 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 arguments in a formal setting and proving cut elimination for sequents built from multisets. The formal setting is particularly important for sequents built from multisets, in order 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 diffi cult to verify the correctness of his induction argument based on “width”. In our formulation however, verification of the induction argument is straight forward. Finally, the multiset setting also introduces a new complication in the 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 show that the algorithm purporting to show the non termi nation of Valentini’s arguments is not a faithful representation of the original arguments, but is instead a transformation already known to be insufficient. | |||||||||
| Keywords | No keywords specified (fix it) | |||||||||
| Categories | No categories specified (fix it) | |||||||||
| Options |
|
|||||||||
Download options| PhilPapers Archive |
Upload a copy of this paper Check publisher's policy on self-archival Papers currently archived: 5,653 |
| External links |
  Try with proxy. |
| Through your library | Only published papers are available at libraries |
Similar books and articlesJ. W. Degen (1999). Complete Infinitary Type Logics. Studia Logica 63 (1):85-119.
G. Mints (1999). Cut-Elimination for Simple Type Theory with an Axiom of Choice. Journal of Symbolic Logic 64 (2):479-485.
David J. Pym (1995). A Note on the Proof Theory the λII-Calculus. Studia Logica 54 (2):199 - 230.
Roy Dyckhoff & Luis Pinto (1998). Cut-Elimination and a Permutation-Free Sequent Calculus for Intuitionistic Logic. Studia Logica 60 (1):107-118.
Gilles Dowek & Benjamin Werner (2003). Proof Normalization Modulo. Journal of Symbolic Logic 68 (4):1289-1316.
Grigori Mints (1997). Indexed Systems of Sequents and Cut-Elimination. Journal of Philosophical Logic 26 (6):671-696.
Grigori Mints (2012). Effective Cut-Elimination for a Fragment of Modal Mu-Calculus. Studia Logica 100 (1-2):279-287.
Silvio Valentini (1983). The Modal Logic of Provability: Cut-Elimination. Journal of Philosophical Logic 12 (4):471 - 476.
Analytics
Monthly downloads |
Added to index2009-01-28Total downloads6 ( #145,407 of 548,977 )Recent downloads (6 months)2 ( #37,438 of 548,977 )How can I increase my downloads? |
My notes
Discussion
