Phase Semantics for Linear Logic with Least and Greatest Fixed Points
Résumé
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 (µMALL) 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 paper, we extend the phase semantics of multiplicative additive linear logic (a.k.a. MALL) to µMALL with explicit (co)induction (i.e. µMALL ind). We introduce a Tait-style system for µMALL called µMALLω where proofs are wellfounded but potentially infinitely branching. We study its phase semantics and prove that it does not have the finite model property.
Origine : Fichiers éditeurs autorisés sur une archive ouverte
Licence : CC BY - Paternité
Licence : CC BY - Paternité