David Bourget (Western Ontario)
David Chalmers (ANU, NYU)
Rafael De Clercq
Ezio Di Nucci
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.
Giovanni Sambin & Silvio Valentini (1982). The Modal Logic of Provability. The Sequential Approach. Journal of Philosophical Logic 11 (3):311 - 342.
Jan von Plato (2001). A Proof of Gentzen's Hauptsatz Without Multicut. Archive for Mathematical Logic 40 (1):9-18.
Citations of this work BETA
Jude Brighton (2016). Cut Elimination for GLS Using the Terminability of its Regress Process. Journal of Philosophical Logic 45 (2):147-153.
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.
Rajeev Gore, Linda Postniece & Alwen Tiu, Cut-Elimination and Proof-Search for Bi-Intuitionistic Logic Using Nested Sequents.
Grigori Mints (2012). Effective Cut-Elimination for a Fragment of Modal Mu-Calculus. Studia Logica 100 (1-2):279-287.
Grigori Mints (1997). Indexed Systems of Sequents and Cut-Elimination. Journal of Philosophical Logic 26 (6):671-696.
Gilles Dowek & Benjamin Werner (2003). Proof Normalization Modulo. Journal of Symbolic Logic 68 (4):1289-1316.
Roy Dyckhoff & Luis Pinto (1998). Cut-Elimination and a Permutation-Free Sequent Calculus for Intuitionistic Logic. Studia Logica 60 (1):107-118.
David J. Pym (1995). A Note on the Proof Theory the λII-Calculus. Studia Logica 54 (2):199 - 230.
G. Mints (1999). Cut-Elimination for Simple Type Theory with an Axiom of Choice. Journal of Symbolic Logic 64 (2):479-485.
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 downloads26 ( #148,029 of 1,796,189 )
Recent downloads (6 months)7 ( #116,661 of 1,796,189 )
How can I increase my downloads?