Valentini's cut-elimination for provability logic resolved
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|
|Source:||Advances in Modal Logic, Volume 7|
|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.