On Cut-elimination for Provability Logic GL

Revantha Ramanayake (ANU, College of Engineering and Computer Science)

CSL PHD MONITORING

DATE: 2007-03-29
TIME: 13:30:00 - 14:00:00
LOCATION: RSISE Seminar Room, ground floor, building 115, cnr. North and Daley Roads, ANU
CONTACT: JavaScript must be enabled to display this email address.

ABSTRACT:
In 1983, Valentini presented a syntactic proof of cut-elimination for a sequent calculus $GLS$ for the provability logic $GL$. The sequents in $GLS$ were built from sets, as opposed to multisets, thus permitting implicit contractions. Recently it has been claimed that Valentini's transformations to eliminate cut do not terminate when applied to a multiset formulation of $GLS$ with a rule of contraction. However it appears that the algorithm used to show non-termination is extit{not} a faithful representation of Valentini's arguments. Here we show how Valentini's transformations can in fact be applied in a multiset setting. As usual, it is the case of contractions above cut that requires special care, especially when the cut-formula is boxed. We deal with this instance using a transformation based on Valentini's original arguments.
BIO: