David Bourget (Western Ontario)
David Chalmers (ANU, NYU)
Rafael De Clercq
Jack Alan Reynolds
Learn more about PhilPapers
Review of Symbolic Logic 5 (2):212-238 (2012)
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||categorize this paper)|
Setup an account with your affiliations in order to access resources via your University's proxy server
Configure custom proxy (use this if your affiliation does not provide a proxy)
|Through your library|
References found in this work BETA
A. S. Troelstra (2000). Basic Proof Theory. Cambridge University Press.
Gaisi Takeuti (1987). Proof Theory. Sole Distributors for the U.S.A. And Canada, Elsevier Science Pub. Co..
Nuel D. Belnap (1982). Display Logic. Journal of Philosophical Logic 11 (4):375-417.
Francesca Poggiolesi (2008). A Cut-Free Simple Sequent Calculus for Modal Logic S. Review of Symbolic Logic 1 (1):3-15.
Giovanni Sambin & Silvio Valentini (1982). The Modal Logic of Provability. The Sequential Approach. Journal of Philosophical Logic 11 (3):311 - 342.
Citations of this work BETA
Jude Brighton (forthcoming). Cut Elimination for GLS Using the Terminability of its Regress Process. Journal of Philosophical Logic:1-7.
Nick Bezhanishvili & Silvio Ghilardi (2014). The Bounded Proof Property Via Step Algebras and Step Frames. Annals of Pure and Applied Logic 165 (12):1832-1863.
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 downloads18 ( #150,906 of 1,725,584 )
Recent downloads (6 months)8 ( #81,222 of 1,725,584 )
How can I increase my downloads?