Phase Semantics for Linear Logic with Least and Greatest Fixed Points

Jan 16 14:00 ₂₀₂₄

Abstract: The truth semantics of linear logic (i.e. phase semantics) is often overlooked despite having a wide range of applications and deep connections with several denotational semantics. In phase semantics, one is concerned about the provability of formulas rather than the contents of their proofs (or refutations). Linear logic equipped with the least and greatest fixpoint operators (\muMALL) has been an active field of research for the past one and a half decades. Various proof systems are known viz. finitary and non-wellfounded, based on explicit and implicit (co)induction respectively. In this talk, I present an extension of the phase semantics of multiplicative additive linear logic (a.k.a. \MALL) to \muMALL with explicit (co)induction (i.e. \muMALLind). Then I introduce a Tait-style system for \muMALL where proofs are wellfounded but potentially infinitely branching. We will see its phase semantics and the fact that it does not have the finite model property. This presentation is based on joint work with Abhishek De and Alexis Saurin.