Technical reports

Multiple modalities

G.M. Bierman

December 1998, 26 pages

DOI: 10.48456/tr-455

Abstract

Linear logic removes the structural rules of weakening and contraction and adds an S4-like modality (written !). Only formulae of the form !φ can be weakened or contracted. An interesting question is whether these two capabilities can be separated using two different modalities. This question was studied semantically in a comprehensive paper by Jacobs. This paper considers the question proof-theoretically, giving sequent calculus, natural deduction and axiomatic formulations.

Full text

PDF (1.3 MB)

BibTeX record

@TechReport{UCAM-CL-TR-455,
  author =	 {Bierman, G.M.},
  title = 	 {{Multiple modalities}},
  year = 	 1998,
  month = 	 dec,
  url = 	 {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-455.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  doi = 	 {10.48456/tr-455},
  number = 	 {UCAM-CL-TR-455}
}