Skip navigation
Skip navigation

Valentini's cut-elimination for provability logic resolved

Gore, Rajeev; Ramanayake, Revantha


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...[Show more]

CollectionsANU Research Publications
Date published: 2008
Type: Conference paper
Source: Advances in Modal Logic, Volume 7


File Description SizeFormat Image
01_Gore_Valentini's_cut-elimination_2008.pdf505.78 kBAdobe PDF    Request a copy

Items in Open Research are protected by copyright, with all rights reserved, unless otherwise indicated.

Updated:  19 May 2020/ Responsible Officer:  University Librarian/ Page Contact:  Library Systems & Web Coordinator