We formalize in Coq a focused system [2] for first-order linear logic (FLL) [1]. We prove cut-elimination directly in this system using five cut-rules dealing with the two different kind of sequents in this system (focused and unfocused sequents).
Following [3], we encode the inference rules of other logics as LL theories and formalize the necessary conditions for those logics to have the cut-elimination property. We then obtain cut-elimination for first-order classical, minimal and intuitionistic logics. We also use the LL meta-theory to formalize the relative completeness of natural deduction and sequent calculus in first-order minimal logic.
We have also formalized the result in [5]: Hybrid Linear Logic can be adequately encoded as an LL theory. Moreover, we propose an alternative encoding which is cut-coherent and we obtain cut-elimination for HyLL.
More details in this paper.
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.12.0 No extra library is needed for compilation.
Typing "make" should suffice to compile the project (time ~7min):
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 [4] 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:
- Focused first-order linear logic as specification logic (SL); and
- Different OLs encoded as LL 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.
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 (i.e., focused first-order linear logic) and the cut-elimination theorem.
This file defines the syntax of linear logic and its notation. We also define several notions needed for the focused system (e.g., negative and positive formulas, polarity of atoms, etc)
This file formalizes Andreoli's triadic (focused) system for linear logic. Sequents are of the shape
|-- B ; M ; X
where
- B is the classical context
- M contains only positive formulas
- X is an "arrow" that can be:
- UP L, where L is a list of formulas (negative phase )
- DW F, where F is a formula (positive phase)
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).
Here we define several tactics useful for dealing with FLL sequents.
This file proves some invertibility lemmas for the negative (unfocus) phase. In
the end, EquivUpArrow shows that exchange is admissible in the list
L of the negative 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 general initial rule is admissible.
This directory contains a simple example showing how to use the library to prove sequents in FLL. It also contains two applications of the framework:
- Formalizing the necessary conditions for an object logic to have the cut-elimination property following the approach in [3].
- Encoding a transition system and proving some properties of it.
The README.md file in each directory contains further details on the formalized theorems.
[1] Linear Logic by Jean-Yves Girard. Theoretical Computer Science (50), pp. 1-102 (1987)
[2] Logic Programming with Focusing Proofs in Linear Logic by Jean-Marc Andreoli. J. Log. Comput. 2(3): 297-347 (1992).
[3] A formal framework for specifying sequent calculus proof systems by Dale Miller and Elaine Pimentel. Theor. Comput. Sci. 474: 98-116 (2013)
[4] 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)
[5] Hybrid linear logic, revisited by Kaustuv Chaudhuri, Joëlle Despeyroux, Carlos Olarte, Elaine Pimentel. Math. Struct. Comput. Sci. 29(8): 1151-1176 (2019)