Department of Computer Science and Technology

Technical reports

Multiple modalities

G.M. Bierman

December 1998, 26 pages

DOI: 10.48456/tr-455


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

  author =	 {Bierman, G.M.},
  title = 	 {{Multiple modalities}},
  year = 	 1998,
  month = 	 dec,
  url = 	 {},
  institution =  {University of Cambridge, Computer Laboratory},
  doi = 	 {10.48456/tr-455},
  number = 	 {UCAM-CL-TR-455}