8 March 2022, The Utrecht Logic in Progress Series (TULIPS), Revantha Ramanayake

Abstract: Cut-elimination is a fundamental result of proof theory. It is the algorithm for eliminating cuts from a sequent calculus proof, leading to cut-free calculi and applications. Although the algorithm is remarkably robust in the sense that it applies with few amendments to many logics (irrespective of their semantics), it simply does not hold for most logics. Its importance is such that the invariable response is a move from the sequent calculus to richer proof formalisms in a bid to regain the cut-elimination. In this talk I will discuss the first steps in a radically different approach called cut-restriction: identifying how to adapt Gentzen’s age-old cut-elimination arguments to restrict the shape of the cut-formulas when elimination is not possible. I will present the “first level above cut-free”: restricting the standard sequent calculi for bi-intuitionistic logic and S5 to analytic cuts. These are two logics where (analytic) cuts are known to be essential.

This is joint work with Agata Ciabattoni (TU Wien) and Timo Lang (UCL).

TRANSLATE with <img /> x English ArabicHebrewPolish BulgarianHindiPortuguese CatalanHmong DawRomanian Chinese SimplifiedHungarianRussian Chinese TraditionalIndonesianSlovak CzechItalianSlovenian DanishJapaneseSpanish DutchKlingonSwedish EnglishKoreanThai EstonianLatvianTurkish FinnishLithuanianUkrainian FrenchMalayUrdu GermanMalteseVietnamese GreekNorwegianWelsh Haitian CreolePersian <img /> <img /> <img /> <img /> TRANSLATE with <img /> COPY THE URL BELOW

<!--a id="TwitterLink" title="Share on Twitter"> <img id="TwitterImg" /></a> <a-- id="FacebookLink" title="Share on Facebook"> <img id="FacebookImg" /></a-->
<a title="Email this translation"> <img /></a> <a> <img /></a> Back EMBED THE SNIPPET BELOW IN YOUR SITE <a title="Copy this code and place it into your HTML."> <img /></a> Enable collaborative features and customize widget: Bing Webmaster Portal Back