M. Kanovich, S. Kuznetsov, V. Nigam, A. Scedrov. A logical framework with commutative and
Logical frameworks allow the specification of deductive systems using the same logical machinery. Linear logical frameworks have been successfully used for the specification of a number of computational, logics and proof
systems. Its success relies on the fact that formulas can be distinguished as linear,
which behave intuitively as resources, and unbounded, which behave intuitionistically. Commutative subexponentials enhance the expressiveness of linear logic
frameworks by allowing the distinction of multiple contexts. These contexts may
behave as multisets of formulas or sets of formulas. Motivated by applications
in distributed systems and in type-logical grammar, we propose a linear logical
framework containing both commutative and non-commutative subexponentials.
Non-commutative subexponentials can be used to specify contexts which behave
as lists, not multisets, of formulas. In addition, motivated by our applications in
type-logical grammar, where the weakenening rule is disallowed, we investigate
the proof theory of formulas that can only contract, but not weaken. In fact, our
contraction is non-local. We demonstrate that under some conditions such formulas may be treated as unbounded formulas, which behave intuitionistically.