Skip navigation
Skip navigation

Valentini's cut-elimination for provability logic resolved

Gore, Rajeev; Ramanayake, Revantha

Description

Valentini (1983) has presented a proof of cut-elimination for provability logic GL for a sequent calculus using sequents built from sets as opposed to multisets, thus avoiding an explicit contraction rule. From a formal point of view, it is more syntactic and satisfying to explicitly identify the applications of the contraction rule that are 'hidden' in proofs of cut-elimination for such sequent calculi. There is often an underlying assumption that the move to a proof of cut-elimination for...[Show more]

CollectionsANU Research Publications
Date published: 2012
Type: Journal article
URI: http://hdl.handle.net/1885/71939
Source: Review of Symbolic Logic
DOI: 10.1017/S1755020311000323

Download

File Description SizeFormat Image
01_Gore_Valentini's_cut-elimination_2012.pdf188.38 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