Valentini's cut-elimination for provability logic resolved
-
Altmetric Citations
Gore, Rajeev; Ramanayake, Revantha
Description
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]
Collections | ANU Research Publications |
---|---|
Date published: | 2008 |
Type: | Conference paper |
URI: | http://hdl.handle.net/1885/52720 |
Source: | Advances in Modal Logic, Volume 7 |
DOI: | 10.1.1.218.2941&rank=1 |
Download
File | Description | Size | Format | Image |
---|---|---|---|---|
01_Gore_Valentini's_cut-elimination_2008.pdf | 505.78 kB | Adobe PDF | Request a copy |
Items in Open Research are protected by copyright, with all rights reserved, unless otherwise indicated.
Updated: 17 November 2022/ Responsible Officer: University Librarian/ Page Contact: Library Systems & Web Coordinator