Graduate studies at Western
The Review of Symbolic Logic 5 (2):212-238 (2012)
|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)|
No categories specified
(categorize this paper)
|Through your library||Configure|
Similar books and articles
J. 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.
Rajeev Gore, Linda Postniece & Alwen Tiu, Cut-Elimination and Proof-Search for Bi-Intuitionistic Logic Using Nested Sequents.
Silvio Valentini (1983). The Modal Logic of Provability: Cut-Elimination. [REVIEW] Journal of Philosophical Logic 12 (4):471 - 476.
Added to index2009-01-28
Total downloads6 ( #155,400 of 757,557 )
Recent downloads (6 months)1 ( #63,427 of 757,557 )
How can I increase my downloads?