Article
On noncommutative extensions of linear logic
Pomset logic introduced by Retoré is an extension of linear logic with a self-dual noncommutative connective. The logic is defined by means of proof-nets, rather than a sequent calculus. Later a deep inference system BV was developed with an eye to capturing Pomset logic, but equivalence of system has not been proven up to now. As for a sequent calculus formulation, it has not been known for either of these logics, and there are convincing arguments that such a sequent calculus in the usual sense simply does not exist for them. In an on-going work on semantics we discovered a system similar to Pomset logic, where a noncommutative connective is no longer self-dual. Pomset logic appears as a degeneration, when the class of models is restricted. Motivated by these semantic considerations, we define in the current work a semicommutative multiplicative linear logic}, which is multiplicative linear logic extended with two nonisomorphic noncommutative connectives (not to be confused with very different Abrusci-Ruet noncommutative logic). We develop a syntax of proof-nets and show how this logic degenerates to Pomset logic. However, a more interesting problem than just finding yet another noncommutative logic is to find a sequent calculus for this logic. We introduce decorated sequents, which are sequents equipped with an extra structure of a binary relation of reachability on formulas. We define a decorated sequent calculus for semicommutative logic and prove that it is cut-free, sound and complete. This is adapted to "degenerate" variations, including Pomset logic. Thus, in particular, we give a variant of sequent calculus formulation for Pomset logic, which is one of the key results of the paper.
In their seminal paper:
Lincoln, P., Mitchell, J., Scedrov, A. and Shankar, N. (1992). Decision problems for propositional linear logic. Annals of Pure and Applied Logic 56 (1–3) 239–311,
LMSS have established an extremely surprising result that propositional linear logic is undecidable. Their proof is very complex and involves numerous nested inductions of different kinds. Later an alternative proof for the LL undecidability has been developed based on simulation Minsky machines in linear logic: Kanovich, M. (1995). The direct simulation of Minsky machines in linear logic. In: Girard, J.-Y., Lafont, Y. and Regnier, L. (eds.) Advances in Linear Logic, London Mathematical Society Lecture Notes, volume 222, Cambridge University Press 123–145. Notice that this direct simulation approach has been successfully applied for a large number of formal systems with resolving a number of open problems in computer science and even computational linguistics, e.g.,
James Brotherston, Max I. Kanovich: Undecidability of Propositional Separation Logic and Its Neighbours. J. ACM 61(2): 14:1-14:43 (2014), Max Kanovich, Stepan Kuznetsov, Andre Scedrov: Undecidability of the Lambek Calculus with a Relevant Modality. FG 2016: 240-256. Nevertheless, recently the undecidability of linear logic is questioned by some people. They claim that they have found lacunae in the LMSS 1992 paper, and, moreover, they have a proof that propositional linear logic is decidable!!! I have been asked to submit a paper, as clear as possible, to the Journal, in order to sort out such a confusing problem, once and for all.
Here, we give a fully self-contained, easy-to-follow, but fully detailed, direct and constructive proof of the undecidability of a very simple Horn-like fragment of linear logic, the proof is accessible to a wide range of people. Namely, we show that there is a direct correspondence between terminated computations of a Minsky machine M and cut-free linear logic derivations for a Horn-like sequent of the form \Phi_M, l1 |- l0 where \Phi_M consists only of Horn-like implications of the very simple forms. Neither negation, nor &, nor constants, nor embedded implications/bangs are used here. Furthermore, our particular correspondence constructed above provides decidability for some smaller Horn-like fragments along with the complexity bounds that come from the proof.
Just as intuitionistic proofs can be modeled by functions, linear logic proofs, being symmetric in the inputs and outputs, can be modeled by relations (for example, cliques in coherence spaces). However generic relations do not establish any functional dependence between the arguments, and therefore it is questionable whether they can be thought as reasonable generalizations of functions. On the other hand, in some situations (typically in differential calculus) one can speak in some precise sense about an implicit functional dependence defined by a relation. It turns out that it is possible to model linear logic with implicit functions rather than general relations, an adequate language for such a semantics being (elementary) differential calculus. This results in a non-degenerate model enjoying quite strong completeness properties.
This paper proposes a definition of categorical model of the deep inference system BV, defined by Guglielmi. Deep inference introduces the idea of performing a deduction in the interior of a formula, at any depth. Traditional sequent calculus rules only see the roots of formulae. However in these new systems, one can rewrite at any position in the formula tree. Deep inference in particular allows the syntactic description of logics for which there is no sequent calculus. One such system is BV, which extends linear logic to include a noncommutative self-dual connective. This is the logic our paper proposes to model. Our definition is based on the notion of a linear functor, due to Cockett and Seely. A BV-category is a linearly distributive category, possibly with negation, with an additional tensor product which, when viewed as a bivariant functor, is linear with a degeneracy condition. We show that this simple definition implies all of the key isomorphisms of the theory. We consider Girard’s category of probabilistic coherence spaces and show that it contains a self-dual monoidal structure in addition to the *-autonomous structure exhibited by Girard. This structure makes the category a BV-category. We believe this structure is also of independent interest, as well-behaved noncommutative operators generally are.
The Lambek calculus can be considered as a version of non-commutative intuitionistic linear logic. One of the interesting features of the Lambek calculus is the so-called “Lambek’s restriction,” that is, the antecedent of any provable sequent should be non-empty. In this paper we discuss ways of extending the Lambek calculus with the linear logic exponential modality while keeping Lambek’s restriction. We present several versions of the Lambek calculus extended with exponential modalities and prove that those extensions are undecidable, even if we take only one of the two divisions provided by the Lambek calculus.
Linear logic and its refinements have been used as a specification language for a number of deductive systems. This has been accomplished by carefully studying the structural restrictions of linear logic modalities. Examples of such refinements are subexponentials, light linear logic, and soft linear logic. We bring together these refinements of linear logic in a non-commutative setting. We introduce a non-commutative substructural system with subexponential modalities controlled by a minimalistic set of rules. Namely, we disallow the contraction and weakening rules for the exponential modality and introduce two primitive subexponentials. One of the subexponentials allows the multiplexing rule in the style of soft linear logic and light linear logic. The second subexponential provides the exchange rule. For this system, we construct a sequent calculus, establish cut elimination, and also provide a complete focused proof system. We illustrate the expressive power of this system by simulating Turing computations and categorial grammar parsing for compound sentences. Using the former, we prove undecidability results. The new system employs Lambek’s non-emptiness restriction, which is incompatible with the standard (sub)exponential setting. Lambek’s restriction is crucial for applications in linguistics: without this restriction, categorial grammars incorrectly mark some ungrammatical phrases as being correct.
This proceedings publication is a compilation of selected contributions from the “Third International Conference on the Dynamics of Information Systems” which took place at the University of Florida, Gainesville, February 16–18, 2011. The purpose of this conference was to bring together scientists and engineers from industry, government, and academia in order to exchange new discoveries and results in a broad range of topics relevant to the theory and practice of dynamics of information systems. Dynamics of Information Systems: Mathematical Foundation presents state-of-the art research and is intended for graduate students and researchers interested in some of the most recent discoveries in information theory and dynamical systems. Scientists in other disciplines may also benefit from the applications of new developments to their own area of study.