Department of Computer Science and Technology

Technical reports

A mixed linear and non-linear logic: proofs, terms and models

P.N. Benton

October 1994, 65 pages

DOIhttps://doi.org/10.48456/tr-352

Abstract

Intuitionistic linear logic regains the expressive power of intuitionistic logic through the ! (‘of course’) modality. Benton, Bierman, Hyland and de Paiva have given a term assignment system for ILL and an associated notion of catagorical model in which the ! modality is modelled by a comonad satisfying certain extra conditions. Ordinary intuitionistic logic is then modelled in a cartesian closed category which arises as a full subcategory of the category of coalgebras for the comonad.

This paper attempts to explain the connection between ILL and IL more directly and symmetrically by giving a logic, term calculus and categorical model for a system in which the linear and non-linear worlds exist on an equal footing, with operations allowing one to pass in both directions. We start from the categorical model of ILL given by Benton, Bierman, Hyland and de Paiva and show that that this is equivalent to having a symmetric monoidal adjunction between a symmetric monoidal closed category and a cartesian closed category. We then derive both a sequent calculus and a natural deduction presentation of the logic corresponding to the new notion of model.

Full text

PDF (4.7 MB)

BibTeX record

@TechReport{UCAM-CL-TR-352,
  author =	 {Benton, P.N.},
  title = 	 {{A mixed linear and non-linear logic: proofs, terms and
         	   models}},
  year = 	 1994,
  month = 	 oct,
  url = 	 {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-352.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  doi = 	 {10.48456/tr-352},
  number = 	 {UCAM-CL-TR-352}
}