Linear Logic Properly Displayed

Research output: Contribution to JournalArticleAcademicpeer-review

Abstract

We introduce proper display calculi for intuitionistic, bi-intuitionistic and classical linear logics with exponentials, which are sound, complete, conservative, and enjoy cut elimination and subformula property. Based on the same design, we introduce a variant of Lambek calculus with exponentials, aimed at capturing the controlled application of exchange and associativity. Properness (i.e., closure under uniform substitution of all parametric parts in rules) is the main technical novelty of the present proposal, allowing both for the smoothest proof of cut elimination and for the development of an overarching and modular treatment for a vast class of axiomatic extensions and expansions of intuitionistic, bi-intuitionistic, and classical linear logics with exponentials. Our proposal builds on an algebraic and order-theoretic analysis of linear logic and applies the guidelines of the multi-type methodology in the design of display calculi.

Original languageEnglish
Article number3570919
Pages (from-to)1-56
Number of pages56
JournalACM Transactions on Computational Logic
Volume24
Issue number2
DOIs
Publication statusPublished - Apr 2023

Bibliographical note

Funding Information:
The research of Giuseppe Greco and Alessandra Palmigiano has been funded in part by the NWO grant KIVI.2019.001.

Publisher Copyright:
© 2023 Association for Computing Machinery.

Keywords

  • analytic inductive inequalities
  • lattice expansions
  • Proper display calculi
  • properly displayable logics
  • unified correspondence

Fingerprint

Dive into the research topics of 'Linear Logic Properly Displayed'. Together they form a unique fingerprint.

Cite this