Skip navigation
Skip navigation

Valentini's cut-elimination for provability logic resolved

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]

CollectionsANU 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 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:  12 November 2018/ Responsible Officer:  University Librarian/ Page Contact:  Library Systems & Web Coordinator