We formalize in Coq a linear nested system (LNS) [1] for focused [2] first-order linear logic [3] with subexponentials [4] where each subexpential may have different substructural and modal behaviors. In particular, each subexponential index may be unbounded (allowing weakening and contraction) or linear and, in addition, it may exhibit different modal behaviors including the axioms 4, D and T. The axiom K is assumed for all of them. We call this logic MMLL (multi-modal linear logic), that extends linear logic and also subexponential linear logic [5]. We prove a cut-elimination theorem for this system.
Following [6], we encode the inference rules of different logics as MMLL theories and formalize the necessary conditions for those logics to be analytic. We then obtain cut-elimination theorems for LNS presentations of classical and (multi-conclusion) intuitionistic logics as well as for multi-modal classical and substructural logics.
This package is free software; you can redistribute it and/or modify it under the terms of GNU Lesser General Public License (see the COPYING file).
The project was tested in Coq 8.15. No extra library is needed for compilation.
Typing "make" should suffice to compile the project:
coq_makefile -f _CoqProject -o Makefile
make
The project documentation can be generated by
make html
We briefly describe the content (theorems and definitions) of the .v files. The documentation of the library offers more detailed explanations.
We use the Hybrid library [7] to support reasoning about object logics (OLs) expressed using higher-order abstract syntax (HOAS). Hybrid is implemented as a two-level system and then, we have:
- MMLL as specification logic (SL); and
- Different OLs encoded as MMLL theories.
For this reason, the project is divided in two main subdirectories, namely, SL and OL plus an additional one (Misc) for some miscellaneous definitions and results. There is an additional TEX/PDF with the needed proof transformations to prove cut-admissibility of the focused system for MMLL.
In Hybrid.v there is an adaptation of the Hybrid library for our purposes. There are also additional results about lists and permutations needed in the development. The results in Permutation.v are based on the ones in MyPermutations.v.
This directory contains the formalization of the specification logic MMLL and the cut-elimination theorem.
This file defines the syntax of MMLL and its notation. We also define several
notions needed for the focused system (e.g., negative and positive formulas,
polarity of atoms, etc). The class Signature can be instantiated so to
specify the indices for the subexponentials and the axioms assumed for each of
them.
Definition of sequents and linear nested sequents.
We prove that, multiset-equivalent contexts (i.e., lists up to permutation) prove the same theorems (exchange rule). We also prove that the classical context admits the usual weakening and contraction rules (preserving the height of the derivation) for unbounded subexponentials.
Here we define several tactics useful for dealing with MMLL sequents.
This file proves some invertibility lemmas for the negative (unfocus) phase.
This file proves some invertibility lemmas showing that positive rules can be switched.
The proof of the cut-elimination theorem for the focused system.
The directory OL contains examples showing how to use object logics as MMLL theories. For the moment, there are specifications for the linear system for classical, (multi-conclusion) intuitionistic logic and the modal logic S4.
[1] Björn Lellmann: Linear Nested Sequents, 2-Sequents and Hypersequents. TABLEAUX 2015: 135-150
[2] Logic Programming with Focusing Proofs in Linear Logic by Jean-Marc Andreoli. J. Log. Comput. 2(3): 297-347 (1992).
[3] Linear Logic by Jean-Yves Girard. Theoretical Computer Science (50), pp. 1-102 (1987)
[4] Vincent Danos, Jean-Baptiste Joinet, Harold Schellinx: The Structure of Exponentials: Uncovering the Dynamics of Linear Logic Proofs. Kurt Gödel Colloquium 1993: 159-171
[5] Björn Lellmann, Carlos Olarte, Elaine Pimentel: A uniform framework for substructural logics with modalities. LPAR 2017: 435-455
[6] A formal framework for specifying sequent calculus proof systems by Dale Miller and Elaine Pimentel. Theor. Comput. Sci. 474: 98-116 (2013)
[7] Hybrid - A Definitional Two-Level Approach to Reasoning with Higher-Order Abstract Syntax by Amy P. Felty and Alberto Momigliano. J. Autom. Reasoning 48(1): 43-105 (2012)