Multiple conclusion linear logic: cut elimination and more

Harley Eades, Valeria De Paiva

Research output: Contribution to journalArticle

Abstract

Full intuitionistic linear logic (FILL) was first introduced by Hyland and de Paiva, and went against current beliefs that it was not possible to incorporate all of the linear connectives, e.g. tensor, par and implication, into an intuitionistic linear logic. Bierman showed that their formalization of FILL did not enjoy cut elimination as such, but Bellin proposed a small change to the definition of FILL regaining cut elimination and using proof nets. In this note we adopt Bellin's proposed change and give a direct proof of cut elimination for the sequent calculus. Then we show that a categorical model of FILL in the basic dialectica category is also a linear/non-linear model of Benton and a full tensor model of Melliès' and Tabareau's tensorial logic. We give a double-negation translation of linear logic into FILL that explicitly uses par in addition to tensor. Lastly, we introduce a new library to be used in the proof assistant Agda for proving properties of dialectica categories.

Original languageEnglish (US)
Pages (from-to)157-174
Number of pages18
JournalJournal of Logic and Computation
Volume30
Issue number1
DOIs
StatePublished - Jan 23 2020

Keywords

  • classical linear logic
  • cut elimination
  • dialectica category
  • formal proof
  • full intuitionistic linear logic
  • par
  • proof assistants
  • tensorial logic

ASJC Scopus subject areas

  • Software
  • Theoretical Computer Science
  • Arts and Humanities (miscellaneous)
  • Hardware and Architecture
  • Logic

Fingerprint Dive into the research topics of 'Multiple conclusion linear logic: cut elimination and more'. Together they form a unique fingerprint.

  • Cite this