Licata, Daniel R. ;
Shulman, Michael ;
Riley, Mitchell
A Fibrational Framework for Substructural and Modal Logics
Abstract
We define a general framework that abstracts the common features of many intuitionistic substructural and modal logics / type theories. The framework is a sequent calculus / normalform type theory parametrized by a mode theory, which is used to describe the structure of contexts and the structural properties they obey. In this sequent calculus, the context itself obeys standard structural properties, while a term, drawn from the mode theory, constrains how the context can be used. Product types, implications, and modalities are defined as instances of two general connectives, one positive and one negative, that manipulate these terms. Specific mode theories can express a range of substructural and modal connectives, including nonassociative, ordered, linear, affine, relevant, and cartesian products and implications; monoidal and nonmonoidal functors, (co)monads and adjunctions; nlinear variables; and bunched implications. We prove cut (and identity) admissibility independently of the mode theory, obtaining it for many different logics at once. Further, we give a general equational theory on derivations / terms that, in addition to the usual beta/etarules, characterizes when two derivations differ only by the placement of structural rules. Additionally, we give an equivalent semantic presentation of these ideas, in which a mode theory corresponds to a 2dimensional cartesian multicategory, the framework corresponds to another such multicategory with a functor to the mode theory, and the logical connectives make this into a bifibration. Finally, we show how the framework can be used both to encode existing existing logics / type theories and to design new ones.
BibTeX  Entry
@InProceedings{licata_et_al:LIPIcs:2017:7740,
author = {Daniel R. Licata and Michael Shulman and Mitchell Riley},
title = {{A Fibrational Framework for Substructural and Modal Logics}},
booktitle = {2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)},
pages = {25:125:22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {9783959770477},
ISSN = {18688969},
year = {2017},
volume = {84},
editor = {Dale Miller},
publisher = {Schloss DagstuhlLeibnizZentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2017/7740},
URN = {urn:nbn:de:0030drops77400},
doi = {10.4230/LIPIcs.FSCD.2017.25},
annote = {Keywords: type theory, modal logic, substructural logic, homotopy type theory}
}
2017
Keywords: 

type theory, modal logic, substructural logic, homotopy type theory 
Seminar: 

2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)

Issue date: 

2017 
Date of publication: 

2017 