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)

We present sound and complete semantics and a sequent calculus for the Lambek calculus extended with intuitionistic propositional logic.

We show that the relational semantics of the Lambek calculus, both nonassociative and associative, is also sound and complete for its extension with classical propositional logic. Then, using filtrations, we obtain the finite model property for the nonassociative Lambek calculus extended with classical propositional logic.

The aim of the present book is to give a comprehensive account of the ‘state of the art’ of substructural logics, focusing both on their proof theory and on their semantics (both algebraic and relational. It is for graduate students in either philosophy, mathematics, theoretical computer science or theoretical linguistics as well as specialists and researchers.

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)

In this paper, we introduce connectification operators for intuitionistic and classical linear algebras corresponding to linear logic and to some of its extensions withn-contraction. In particular,n-contraction (n2) is a version of the contraction rule, wheren+1 occurrences of a formula may be contracted ton occurrences. Since cut cannot be eliminated from the systems withn-contraction considered most of the standard proof-theoretic techniques to investigate meta-properties of those systems are useless. However, by means of connectification we establish the disjunction property for both intuitionistic (...) and classical affine linear logics withn-contraction. (shrink)

We give a proof-theoretic and algorithmic complexity analysis for systems introduced by Morrill to serve as the core of the CatLog categorial grammar parser. We consider two recent versions of Morrill’s calculi, and focus on their fragments including multiplicative (Lambek) connectives, additive conjunction and disjunction, brackets and bracket modalities, and the! subexponential modality. For both systems, we resolve issues connected with the cut rule and provide necessary modifications, after which we prove admissibility of cut (cut elimination theorem). We also prove (...) algorithmic undecidability for both calculi, and show that categorial grammars based on them can generate arbitrary recursively enumerable languages. (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.

Lambek categorial grammars is a class of formal grammars based on the Lambek calculus. Pentus proved in 1993 that they generate exactly the class of context-free languages without the empty word. In this paper, we study categorial grammars based on the Lambek calculus with the permutation rule LP. Of particular interest is the product-free fragment of LP called the Lambek-van Benthem calculus LBC. Buszkowski in his 1984 paper conjectured that grammars based on the Lambek-van Benthem calculus (LBC-grammars for short) generate (...) exactly permutation closures of context-free languages. In this paper, we disprove this conjecture by presenting a language generated by an LBC-grammar that is not a permutation closure of any context-free language. Firstly, we introduce an ad-hoc modification of vector addition systems called linearly-restricted branching vector addition systems with states and additional memory (LRBVASSAMs for short) and prove that the latter are equivalent to LBC-grammars. Then we construct an LRBVASSAM that generates a non-semilinear set and thus disprove Buszkowski’s conjecture. Since Buszkowski’s conjecture is false, not so much is known about the languages generated by LBC-grammars or by LP-grammars. The equivalence of LRBVASSAMs and LBC-grammars allows us to establish a number of their properties. We show that LP-grammars generate the same class of languages as LBC-grammars; that is, removing product from LP does not decrease expressive power of corresponding categorial grammars. We also prove that this class of languages is closed under union, intersection, concatenation, and Kleene plus. (shrink)

As an undergraduate I was taught to multiply two numbers with the help of log tables, using the formulaHaving graduated to teach calculus to Engineers, I learned that log tables were to be replaced by slide rules. It was then that Imade the fateful decision that there was no need for me to learn how to use this tedious device, as I could always rely on the students to perform the necessary computations. In the course of time, slide rules were (...) replaced by pocket calculators and personal computers, but I stuck to my original decision.My computer phobia did not prevent me from taking an interest in the theoretical question: what is a computation? This question goes back to Hilbert's 10th problem, which asks for an algorithm, or computational procedure, to decide whether any given polynomial equation is solvable in integers. It quickly leads to the related question: which numerical functionsf: ℕn→ ℕ are computable?While Hilbert's 10th problem was only resolved in 1970, this related question had some earlier answers, of which I shall single out the following three:f is recursive,f is computable on an abstract machine,f is definable in the untyped λ-calculus.These tentative answers were shown to be equivalent by Church [1936] and Turing [1936–7].I shall discuss here some of the more recent developments of these notions of computability and their relevance to linguistics and logic. I hope to be forgiven for dwelling on some of the work I have been involved with personally, with greater emphasis than is justified by its historical significance. (shrink)

We study an expansion of the Distributive Non-associative Lambek Calculus with conjugates of the Lambek product operator and residuals of those conjugates. The resulting logic is well-motivated, under-investigated and difficult to tackle. We prove completeness for some of its fragments and establish that it is decidable. Completeness of the logic is an open problem; some difficulties with applying the usual proof method are discussed.

This contributed volume includes both theoretical research on philosophical logic and its applications in artificial intelligence, mostly employing the concepts and techniques of modal logic. It collects selected papers presented at the Second Asia Workshop on Philosophical Logic, held in Guangzhou, China in 2014, as well as a number of invited papers by specialists in related fields. The contributions represent pioneering philosophical logic research in Asia.

We provide a complete binary implicational axiomatization of the positive fragment of propositional dynamic logic. The intended application of this result are completeness proofs for non-classical extensions of positive PDL. Two examples are discussed in this article, namely, a paraconsistent extension with modal De Morgan negation and a substructural extension with the residuated operators of the non-associative Lambek calculus. Informal interpretations of these two extensions are outlined.

\ is a 7000 line Prolog parser/theorem-prover for logical categorial grammar. In such logical categorial grammar syntax is universal and grammar is reduced to logic: an expression is grammatical if and only if an associated logical statement is a theorem of a fixed calculus. Since the syntactic component is invariant, being the logic of the calculus, logical categorial grammar is purely lexicalist and a particular language model is defined by just a lexical dictionary. The foundational logic of continuity was established (...) by Lambek while a corresponding extension including also logic of discontinuity was established by Morrill and Valentín :167–192, 2010). \ implements a logic including as primitive connectives the continuous and discontinuous connectives of the displacement calculus, additives, 1st order quantifiers, normal modalities, bracket modalities, and universal and existential subexponentials. In this paper we review the rules of inference for these primitive connectives and their linguistic applications, and we survey the principles of Andreoli’s focusing, and of a generalisation of van Benthem’s count-invariance, on the basis of which \ is implemented. (shrink)

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)