We introduce a new correctness criterion for multiplicative non commutative proof nets which can be considered as the non- commutative counterpart to the Danos-Regnier criterion for proof nets of linear logic. The main intuition relies on the fact that any switching for a proof net can be naturally viewed as a series-parallel order variety on the conclusions of the proof net.

We give a proof of the finite model property of some fragments of commutative and noncommutative linear logic: the Lambek calculus, BCI, BCK and their enrichments, MALL and Cyclic MALL. We essentially simplify the method used in [4] for proving fmp of BCI and the Lambek ca culus and in [5] for proving fmp of MALL. Our construction of finite models also differs from that used in Lafont [8] in his proof of fmp of MALL.

RésuméUn paradigme en vogue en informatique théorique exploite l'analogie entre les formules et les types et traite une deduction Al… An→ B comme une opération plurisortale. On propose ici d'étendre cette analogie aux déductions de la forme Al… An→, où la place à droite de la flèche est vide. D'un point de vue logique, une telle déduction constitue une réfutation de la conjonction desformules qui se trouvent à gauche de la flèche. On défend l'idée qu'ilfaut, selon ce paradigme étendu, interpréter (...) la flèche comme assignant à n'importe quelle séquence al… an, où aiest de type Ai, le type des valeurs de vérite correspondantes. Pour que cela fonctionne, cependant, il faut abandonner la règle structurale de l'affaiblissement à droite de la flèche. La négation de A est alors interprétée comme l'ensemble puissance de A et la complétude fonctionnelle habituelle s'identifie au schème de compréhension avec extensionnalitè. (shrink)

In this paper, I discuss the analysis of logic in the pragmatic approach recently proposed by Brandom. I consider different consequence relations, formalized by classical, intuitionistic and linear logic, and I will argue that the formal theory developed by Brandom, even if provides powerful foundational insights on the relationship between logic and discursive practices, cannot account for important reasoning patterns represented by non-monotonic or resource-sensitive inferences. Then, I will present an incompatibility semantics in the framework of linear logic which allow (...) to refine Brandom’s concept of defeasible inference and to account for those non-monotonic and relevant inferences that are expressible in linear logic. Moreover, I will suggest an interpretation of discursive practices based on an abstract notion of agreement on what counts as a reason which is deeply connected with linear logic semantics. (shrink)

This paper contributes to the theory of hybrid substructural logics, i.e. weak logics given by a Gentzen-style proof theory in which there is only alimited possibility to use structural rules. Following the literture, we use an operator to mark formulas to which the extra structural rules may be applied. New in our approach is that we do not see this as a modality, but rather as themeet of the marked formula with a special typeQ. In this way we can make (...) the specific structural behaviour of marked formulas more explicit.The main motivation for our approach is that we can provide a nice, intuitive semantics for hybrid substructural logics. Soundness and completeness for this semantics are proved; besides this we consider some proof-theoretical aspects like cut-elimination and embeddings of the strong system in the hybrid one. (shrink)

Two constructions for adding an involution operator to residuated ordered monoids are investigated. One preserves integrality and the mingle axiom x 2x but fails to preserve the contraction property xx 2. The other has the opposite preservation properties. Both constructions preserve commutativity as well as existent nonempty meets and joins and self-dual order properties. Used in conjunction with either construction, a result of R.T. Brady can be seen to show that the equational theory of commutative distributive residuated lattices (without involution) (...) is decidable, settling a question implicitly posed by P. Jipsen and C. Tsinakis. The corresponding logical result is the (theorem-) decidability of the negation-free axioms and rules of the logic RW, formulated with fusion and the Ackermann constant t. This completes a result of S. Giambrone whose proof relied on the absence of t. (shrink)

The book is a philosophical refection on the possibility of mathematical history. Are poosible models of historical phenomena so exact as those of physical ones? Mathematical models borrowed from quantum mechanics by the meditation of its interpretations are accomodated to history. The conjecture of many-variant history, alternative history, or counterfactual history is necessary for mathematical history. Conclusions about philosophy of history are inferred.

We study the sequent system mentioned in the author's work as CyInFL with ‘intuitionistic’ sequents. We explore the connection between this system and symmetric constructive logic of Zaslavsky and develop an algebraic semantics for both of them. In contrast to the previous work, we prove the strong completeness theorem for CyInFL with ‘intuitionistic’ sequents and all of its basic variants, including variants with contraction. We also show how the defined classes of structures are related to cyclic involutive FL‐algebras and Nelson (...) FLew‐algebras. In particular, we prove the definitional equivalence of symmetric constructive FLewc‐algebras (algebraic models of symmetric constructive logic) and Nelson FLew‐algebras (algebras introduced by Spinks and Veroff, as the termwise equivalent definition of Nelson algebras). Because of the strong completeness theorem that covers all basic variants of CyInFL with ‘intuitionistic’ sequents, we rename this sequent system to symmetric constructive full Lambek calculus (). We verify the decidability of this system and its basic variants, as we did in the case of their distributive cousins. As a consequence we obtain that the corresponding theories of (distributive and nondistributive) symmetric constructive FL‐algebras are decidable. (shrink)

In this paper, we introduce the notion of d-elements on precoherent preidempotent quantale (PIQ), construct Zariski topology on $Max(Q_{d})$ and explore its various properties. Firstly, we give a sufficient condition of a topological space $Max(Q_{d})$ being Hausdorff. Secondly, we prove that if $ P=\mathfrak{B}(P) $ and $ Q=\mathfrak{B}(Q) $, then $P$ is isomorphic to $Q$ iff $ Max(P_{d}) $ is homeomorphic to $ Max(Q_{d}) $. Moreover, we prove that $ (P\otimes Q)_{d} $ is isomorphic to $ P_{d} \otimes Q_{d} $ (...) iff $ P_{d} \otimes Q_{d}=(P_{d} \otimes Q_{d})_{d} $. Finally, we prove that the category $ \textbf{dPFrm} $ is a reflective subcategory of $\textbf{PIQuant}.$. (shrink)

Linear Logic is a versatile framework with diverse applications in computer science and mathematics. One intriguing fragment of Linear Logic is Multiplicative-Additive Linear Logic (MALL), which forms the exponential-free component of the larger framework. Modifying MALL, researchers have explored weaker logics such as Noncommutative MALL (Bilinear Logic, BL) and Cyclic MALL (CyMALL) to investigate variations in commutativity. In this paper, we focus on Cyclic Nonassociative Bilinear Logic (CyNBL), a variant that combines noncommutativity and nonassociativity. We introduce a sequent system for (...) CyNBL, which includes an auxiliary system for incorporating nonlogical axioms. Notably, we establish the cut elimination property for CyNBL. Moreover, we establish the strong conservativeness of CyNBL over Full Nonassociative Lambek Calculus (FNL) without additive constants. The paper highlights that all proofs are constructed using syntactic methods, ensuring their constructive nature. We provide insights into constructing cut-free proofs and establishing a logical relationship between CyNBL and FNL. (shrink)

This paper presents a systematic investigation of fuzzy Galois connections in the sense of R. Bělohlávek [1], from the point of view of enriched category theory. The results obtained show that the theory of enriched categories makes it possible to present the theory of fuzzy Galois connections in a succinct way; and more importantly, it provides a useful method to express and to study the link and the difference between the commutative and the non-commutative worlds.

This book sets out the foundations, methodology, and practice of a formal framework for the description of language. The approach embraces the trends of lexicalism and compositional semantics in computational linguistics, and theoretical linguistics more broadly, by developing categorial grammar into a powerful and extendable logic of signs. Taking Montague Grammar as its point of departure, the book explains how integration of methods from philosophy (logical semantics), computer science (type theory), linguistics (categorial grammar) and meta-mathematics (mathematical logic ) provides a (...) categorial foundation with coverage including intensionality, quantification, featural polymorphism, domains and constraints. For the first time, the book systematises categorial thinking into a unified program which is at once both logically secured, and a practical tool for pure lexical grammar development with type-theoretic semantics. It should be of interest to all those active in computational linguistics and formal grammar and is suitable for use at advanced undergraduate, postgraduate, and research levels. (shrink)

We take a fresh look at the logics of informational dependence and independence of Hintikka and Sandu and Väänänen, and their compositional semantics due to Hodges. We show how Hodges’ semantics can be seen as a special case of a general construction, which provides a context for a useful completeness theorem with respect to a wider class of models. We shed some new light on each aspect of the logic. We show that the natural propositional logic carried by the semantics (...) is the logic of Bunched Implications due to Pym and O’Hearn, which combines intuitionistic and multiplicative connectives. This introduces several new connectives not previously considered in logics of informational dependence, but which we show play a very natural rôle, most notably intuitionistic implication. As regards the quantifiers, we show that their interpretation in the Hodges semantics is forced, in that they are the image under the general construction of the usual Tarski semantics; this implies that they are adjoints to substitution, and hence uniquely determined. As for the dependence predicate, we show that this is definable from a simpler predicate, of constancy or dependence on nothing. This makes essential use of the intuitionistic implication. The Armstrong axioms for functional dependence are then recovered as a standard set of axioms for intuitionistic implication. We also prove a full abstraction result in the style of Hodges, in which the intuitionistic implication plays a very natural rôle. (shrink)

We study filters in residuated structures that are associated with congruence relations (which we call -filters), and develop a semantical theory for general substructural logics based on the notion of primeness for those filters. We first generalize Stone’s sheaf representation theorem to general substructural logics and then define the primeness of -filters as being “points” (or stalkers) of the space, the spectrum, on which the representing sheaf is defined. Prime FL-filters will turn out to coincide with truth sets under various (...) well known semantics for certain substructural logics. We also investigate which structural rules are needed to interpret each connective in terms of prime -filters in the same way as in Kripke or Routley-Meyer semantics. We may consider that the set of the structural rules that each connective needs in this sense reflects the difficulty of giving the meaning of the connective. A surprising discovery is that connectives , ⅋ of linear logic are linearly ordered in terms of the difficulty in this sense. (shrink)

We discuss the logic of pregroups, introduced by Lambek [34], and its connections with other type logics and formal grammars. The paper contains some new ideas and results: the cut-elimination theorem and a normalization theorem for an extended system of this logic, its P-TIME decidability, its interpretation in L1, and a general construction of (preordered) bilinear algebras and pregroups whose universe is an arbitrary monoid.

Permutative logic is a non-commutative conservative extension of linear logic suggested by some investigations on the topology of linear proofs. In order to syntactically reflect the fundamental topological structure of orientable surfaces with boundary, permutative sequents turn out to be shaped like q-permutations. Relaxation is the relation induced on q-permutations by the two structural rules divide and merge; a decision procedure for relaxation has been already provided by stressing some standard achievements in theory of permutations. In these pages, we provide (...) a parallel procedure in which the problem at issue is approached from the point of view afforded by geometry of 2-manifolds and solved by making specific surfaces interact. (shrink)

This paper presents a systematic investigation of fuzzy Galois connections in the sense of R. Bělohlávek [1], from the point of view of enriched category theory. The results obtained show that the theory of enriched categories makes it possible to present the theory of fuzzy Galois connections in a succinct way; and more importantly, it provides a useful method to express and to study the link and the difference between the commutative and the non-commutative worlds.

The starting point of the present study is the interpretation of intuitionistic linear logic in Petri nets proposed by U. Engberg and G. Winskel. We show that several categories of order algebras provide equivalent interpretations of this logic, and identify the category of the so called strongly coherent quantales arising in these interpretations. The equivalence of the interpretations is intimately related to the categorical facts that the aforementioned categories are connected with each other via adjunctions, and the compositions of the (...) connecting functors with co-domain the category of strongly coherent quantales are dense. In particular, each quantale canonically induces a Petri net, and this association gives rise to an adjunction between the category of quantales and a category whose objects are all Petri nets. (shrink)

This paper gives a simple method for providing categorial brands of feature-based unification grammars with a model-theoretic semantics. The key idea is to apply the paradigm of fibred semantics (or layered logics, see Gabbay (1990)) in order to combine the two components of a feature-based grammar logic. We demonstrate the method for the augmentation of Lambek categorial grammar with Kasper/Rounds-style feature logic. These are combined by replacing (or annotating) atomic formulas of the first logic, i.e. the basic syntactic types, by (...) formulas of the second. Modelling such a combined logic is less trivial than one might expect. The direct application of the fibred semantics method where a combined atomic formula like np (num: sg & pers: 3rd) denotes those strings which have the indicated property and the categorial operators denote the usual left- and right-residuals of these string sets, does not match the intuitive, unification-based proof theory. Unification implements a global bookkeeping with respect to a proof whereas the direct fibring method restricts its view to the atoms of the grammar logic. The solution is to interpret the (embedded) feature terms as global feature constraints while maintaining the same kind of fibred structures. For this adjusted semantics, the anticipated proof system is sound and complete. (shrink)

This paper deals with substructural nuclear (image-based) logics and their algebraic and Kripke-style semantics. More precisely, we first introduce a class of substructural logics with connective _N_ satisfying nucleus property, called here substructural _nuclear_ logics, and its subclass, called here substructural _nuclear image-based_ logics, where _N_ further satisfies homomorphic image property. We then consider their algebraic semantics together with algebraic characterizations of those logics. Finally, we introduce _operational Kripke-style_ semantics for those logics and provide two sorts of completeness results for (...) them, one of which is based on algebraic completeness for all the logics and the other of which is based on set-theoretic one for the nuclear image-based logics. (shrink)

We prove that the full completeness theorem for MLL+Mix holds by the simple interpretation via formulas as objects and proofs as Z-invariant morphisms in the *-autonomous category of topologized vector spaces. We do this by generalizing the recent work of Blute and Scott 101–142) where they used the semantical framework of dinatural transformation introduced by Girard–Scedrov–Scott , Logic from Computer Science, vol. 21, Springer, Berlin, 1992, pp. 217–241). By omitting the use of dinatural transformation, our semantics evidently allows the interpretation (...) of the cut-rule, while the original Blute–Scott's does not. Moreover, our interpretation for proofs is preserved automatically under the cut elimination procedure. In our semantics proofs themselves are characterized by the concrete algebraic notion “Z-invariance”, and our denotational semantics provides the full completeness. Our semantics is naturally extended to the full completeness semantics for CyLL+Mix owing to an elegant method of Blute–Scott 1413–1436) 101–142))). (shrink)

This work presents a computational interpretation of the construction process for cyclic linear logic and non-commutative logic sequential proofs. We assume a proof construction paradigm, based on a normalisation procedure known as focussing, which efficiently manages the non-determinism of the construction. Similarly to the commutative case, a new formulation of focussing for NL is used to introduce a general constraint-based technique in order to dealwith partial information during proof construction. In particular, the procedure develops through construction steps propagating constraints in (...) intermediate objects called abstract proofs. (shrink)

We consider a class of graphs embedded in $R^2$ as noncommutative proof-nets with an explicit exchange rule. We give two characterization of such proof-nets, one representing proof-nets as CW-complexes in a two-dimensional disc, the other extending a characterization by Asperti. As a corollary, we obtain that the test of correctness in the case of planar graphs is linear in the size of the data. Braided proof-nets are proof-nets for multiplicative linear logic with Mix embedded in $R^3$ . In order to (...) prove the cut-elimination theorem, we consider proof-nets in $R^2$ as projections of braided proof-nets under regular isotopy. (shrink)

Linear logic, introduced by Girard, is a refinement of classical logic with a natural, intrinsic accounting of resources. This accounting is made possible by removing the ‘structural’ rules of contraction and weakening, adding a modal operator and adding finer versions of the propositional connectives. Linear logic has fundamental logical interest and applications to computer science, particularly to Petri nets, concurrency, storage allocation, garbage collection and the control structure of logic programs. In addition, there is a direct correspondence between polynomial-time computation (...) and proof normalization in a bounded form of linear logic. In this paper we show that unlike most other propositional logics, full propositional linear logic is undecidable. Further, we prove that without the modal storage operator, which indicates unboundedness of resources, the decision problem becomes PSPACE-complete. We also establish membership in NP for the multiplicative fragment, NP-completeness for the multiplicative fragment extended with unrestricted weakening, and undecidability for fragments of noncommutative propositional linear logic. (shrink)

Ordered sheaves on a small quantaloid have been defined in terms of -enriched categorical structures; they form a locally ordered category . The free-cocompletion KZ-doctrine on has , the quantaloid of -modules, as its category of Eilenberg–Moore algebras. In this paper we give an intrinsic description of the Kleisli algebras: we call them the locally principally generated -modules. We deduce that is biequivalent to the 2-category of locally principally generated -modules and left adjoint module morphisms. The example of locally principally (...) generated modules on a locale X is worked out in full detail: relating X-modules to objects of the slice category , we show that ordered sheaves on X correspond with skew local homeomorphisms into X. (shrink)

-autonomous lattices are the algebraic exponentials and without additive constants. In this paper, we investigate the structure theory of this variety and some of its subvarieties, as well as its relationships with other classes of algebras.

We introduce a linear analogue of Läuchli's semantics for intuitionistic logic. In fact, our result is a strengthening of Läuchli's work to the level of proofs, rather than provability. This is obtained by considering continuous actions of the additive group of integers on a category of topological vector spaces. The semantics, based on functorial polymorphism, consists of dinatural transformations which are equivariant with respect to all such actions. Such dinatural transformations are called uniform. To any sequent in Multiplicative Linear Logic (...) , we associate a vector space of“diadditive” uniform transformations. We then show that this space is generated by denotations of cut-free proofs of the sequent in the theory MLL + MIX. Thus we obtain a full completeness theorem in the sense of Abramsky and Jagadeesan, although our result differs from theirs in the use of dinatural transformations.As corollaries, we show that these dinatural transformations compose, and obtain a conservativity result: diadditive dinatural transformations which are uniform with respect to actions of the additive group of integers are also uniform with respect to the actions of arbitrary cocommutative Hopf algebras. Finally, we discuss several possible extensions of this work to noncommutative logic.It is well known that the intuitionistic version of Läuchli's semantics is a special case of the theory of logical relations, due to Plotkin and Statman. Thus, our work can also be viewed as a first step towards developing a theory of logical relations for linear logic and concurrency. (shrink)

Quantum B-algebras, the partially ordered implicational algebras arising as subreducts of quantales, are introduced axiomatically. It is shown that they provide a unified semantic for non-commutative algebraic logic. Specifically, they cover the vast majority of implicational algebras like BCK-algebras, residuated lattices, partially ordered groups, BL- and MV-algebras, effect algebras, and their non-commutative extensions. The opposite of the category of quantum B-algebras is shown to be equivalent to the category of logical quantales, in the way that every quantum B-algebra admits a (...) natural embedding into a logical quantale, the enveloping quantale. Partially defined products of algebras related to effect algebras are handled efficiently in this way. The unit group of the enveloping quantale of a quantum B-algebra X is shown to be always contained in X, which gives a functorial subgroup X× of X. Similar subfunctors are obtained for the non-commutative extensions of BCK-algebras and effect algebras. The results of Galatos, Jónsson, and Tsinakis on the splitting of generalized BL-algebras into a semidirect product of a partially ordered group operating on an integral residuated poset are extended to a characterization of twisted semidirect products of a po-group by a quantum B-algebra. (shrink)

We propose various methods for combining or amalgamating propositional languages and deductive systems. We make heavy use of quantales and quantale modules in the wake of previous works by the present and other authors. We also describe quite extensively the relationships among the algebraic and order-theoretic constructions and the corresponding ones based on a purely logical approach.

Involutive Nonassociative Lambek Calculus is a nonassociative version of Noncommutative Multiplicative Linear Logic, but the multiplicative constants are not admitted. InNL adds two linear negations to Nonassociative Lambek Calculus ; it is a strongly conservative extension of NL Logical aspects of computational linguistics. LNCS, vol 10054. Springer, Berlin, pp 68–84, 2016). Here we also add unary modalities satisfying the residuation law and De Morgan laws. For the resulting logic InNLm, we define and study phase spaces. We use them to prove (...) the cut elimination theorem for a one-sided sequent system for InNLm, introduced here. Phase spaces are also employed in studying auxiliary systems InNLm, assuming the k-cyclic law for negation. The latter behave similarly as Classical Nonassociative Lambek Calculus, studied in de Groote and Lamarche :355–388, 2002) and Buszkowski. We reduce the provability in InNLm to that in InNLm. This yields the equivalence of type grammars based on InNLm with -free) context-free grammars and the PTIME complexity of InNLm. (shrink)

, from Stanford Encyclopaedia of Philosophy.

In 1958 J. Lambek introduced a calculusL of syntactic types and defined an equivalence relation on types: x y means that there exists a sequence x=x1,...,xn=y (n 1), such thatx i x i+1 or xi+ x i (1 i n). He pointed out thatx y if and only if there is joinz such thatx z andy z. This paper gives an effective characterization of this equivalence for the Lambeck calculiL andLP, and for the multiplicative fragments of Girard's and Yetter's linear (...) logics. Moreover, for the non-directed Lambek calculusLP and the multiplicative fragment of Girard's linear logic, we present linear time algorithms deciding whether two types are equal, and finding a join for them if they are. (shrink)

The paper presents a way to transform pregroup grammars into contextfree grammars using functional composition. The same technique can also be used for the proof-nets of multiplicative cyclic linear logic and for Lambek calculus allowing empty premises.

Completeness is shown for several versions of Girard's linear logic with respect to Petri nets as the class of models. One logic considered is the -free fragment of intuitionistic linear logic without the exponential !. For this fragment Petri nets form a sound and complete model. The strongest logic considered is intuitionistic linear logic, with ,&, and the exponential ! , and forms of quantification. This logic is shown sound and complete with respect to atomic nets , though only once (...) we add extra axioms specific to the Petri-net model. The logic is remarkably expressive, enabling descriptions of the kinds of properties one might wish to show of nets; in particular, negative properties, asserting the impossibility of an assertion, can also be expressed. Unfortunately, with respect to this logic, whether an assertion is true of a finite net becomes undecidable. (shrink)

We define proof nets for cyclic multiplicative linear logic as edge bi-coloured graphs. Our characterization is purely graph theoretical and works without further complication for proof nets with cuts, which are usually harder to handle in the non-commutative case. This also provides a new characterization of the proof nets for the Lambek calculus (with the empty sequence) which simply are a restriction on the formulas to be considered (which are asked to be intuitionistic).

Context-dependent rules are an obstacle to cut elimination. Turning to a generalised sequent style formulation using deep inferences is helpful, and for the calculus presented here it is essential. Cut elimination is shown for a substructural, multiplicative, pure propositional calculus. Moreover we consider the extra problems induced by non-logical axioms and extend the results to additive connectives and quantifiers.

We prove completeness for some language-theoretic models of the full Lambek calculus and its various fragments. First we consider syntactic concepts and syntactic concepts over regular languages, which provide a complete semantics for the full Lambek calculus \. We present a new semantics we call automata-theoretic, which combines languages and relations via closure operators which are based on automaton transitions. We establish the completeness of this semantics for the full Lambek calculus via an isomorphism theorem for the syntactic concepts lattice (...) of a language and a construction for the universal automaton recognizing the same language. Finally, we use automata-theoretic semantics to prove completeness of relation models of binary relations and finite relation models for the Lambek calculus without and with empty antecedents and \), thus solving a problem left open by Pentus. (shrink)

Substructural logics are obtained from the sequent calculi for classical or intuitionistic logic by suitably restricting or deleting some or all of the structural rules (Restall, 2000; Ono, 1998). Recently, this field of research has come to encompass a number of logics - e.g. many fuzzy or paraconsistent logics - which had been originally introduced out of different, possibly semantical, motivations. A finer proof-theoretical analysis of such logics, in fact, revealed that it was possible to subsume them under the previous (...) definition (see e.g. Aguzzoli and Ciabattoni, 2000).Although proof systems for substructural logics are currently being investigated with remarkable success, their algebraic models do not seem equally satisfactory. In fact:(i) such structures are often very weak, i.e. they do not possess many interesting algebraic properties;(ii) as a consequence, their theories of ideals, congruences, and representation are as a rule scarcely developed, or even lacking.In this paper, we address these difficulties. (shrink)

This work mainly concerns the—here introduced—category of \(\mathscr {Q}\) -sets and functional morphisms, where \(\mathscr {Q}\) is a commutative semicartesian quantale. We prove it enjoys all limits and colimits, that it has a classifier for regular subobjects (a sort of truth-values object), which we characterize and give explicitly. Moreover: we prove it to be \(\kappa \) -locally presentable, (where \(\kappa =max\{|\mathscr {Q}|^+, \aleph _0\}\) ); we also describe a hierarchy of monoidal structures in this category.

The Riemann–Roch theorem for algebraic curves is derived from a theorem for Girard quantales. Serre duality is shown to be a quantalic phenomenon. An example provides a Girard quantale satisfying the Riemann–Roch theorem, where the associated curve is non-connected and irreducible.