- November 24, Björn Lellmann (SBA Research, Vienna)
Proof Theory for Modal Tense Logic and Symmetric Modal Logic via Linear Nested Sequents
Modal logics offering the possibility of travelling backwards along the accessibility relation, such as modal tense logic Kt or symmetric modal logic KB, have often proved difficult to capture satisfactorily from a proof-theoretic point of view. In particular, while ordinary sequent systems, e.g., for KB exist, they rely on an analytic cut rule for completeness. Both tense logic Kt and symmetric modal logic KB have been given cut-free calculi in much more expressive frameworks, arguably the simplest being that of nested sequent calculi. However, the machinery necessary for nested sequents as well as the immediate connection to the semantics raise the question whether these logics can also be captured in a simpler framework.
As a possible contender, recently there has been a resurgence of work in the linear nested sequent framework, an intermediate framework between ordinary and full nested sequents. What was lacking so far, however, were convincing examples for the added expressivity of this frameworks over ordinary sequents, which did not depend on the linear structure of the models for the logics in question.
In this talk I will present joint work with Rajeev Gore showing that modal tense logic Kt and symmetric modal logic KB can indeed be captured in the linear nested sequent framework, thus providing positive answers to both of the above questions.
Time: 16.00 – 17.15
Location: The talk will take place in our dedicated MS Teams team “TULIPS – The Utrecht Logic in Progress Series.” Contact the organizers for information about how to join the online meeting.