Valentini's cut-elimination for provability logic resolved
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]
|Collections||ANU Research Publications|
|Source:||Review of Symbolic Logic|
|01_Gore_Valentini's_cut-elimination_2012.pdf||188.38 kB||Adobe PDF||Request a copy|
Items in Open Research are protected by copyright, with all rights reserved, unless otherwise indicated.