We consider the task of theorem proving in Lambek calculi and their generalisation to ‘multimodal residuation calculi’. These form an integral part of categorial logic, a logic of signs stemming from categorial grammar, of the basis of which language processing is essentially theorem proving. The demand of this application is not just for efficient processing of some or other specific calculus, but for methods that will be generally applicable to categorial logics.It is proposed that multimodal cases be treated by dealing (...) with the highest common factor of all the connectives as linear validity. The prosodic aspects are encoded in labels, in effect the term-structure of quantified linear logic. The correctness condition on proof nets can be implemented by SLD resolution in linear logic with unification on labels/terms limited to one way matching. A suitable unification strategy is obtained for calculi of discontinuity by normalisation of the ground goal term followed by recursive descent and redex pattern matching on the head term. (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)

We present a new frame semantics for positive relevant and substructural propositional logics. This frame semantics is both a generalisation of Routley–Meyer ternary frames and a simplification of them. The key innovation of this semantics is the use of a single accessibility relation to relate collections of points to points. Different logics are modeled by varying the kinds of collections used: they can be sets, multisets, lists or trees. We show that collection frames on trees are sound and complete for (...) the basic positive distributive substructural logic $\mathsf {B}^+$, that collection frames on multisets are sound and complete for $\mathsf {RW}^+$ (the relevant logic $\mathsf {R}^+$, without contraction, or equivalently, positive multiplicative and additive linear logic with distribution for the additive connectives), and that collection frames on sets are sound for the positive relevant logic $\mathsf {R}^+$. The completeness of set frames for $\mathsf {R}^+$ is, currently, an open question. (shrink)

It is shown that the intuitionistic propositional calculus is sound and complete with respect to Kripke-style models that are not quasi-ordered. These models, called rudimentary Kripke models, differ from the ordinary intuitionistic Kripke models by making fewer assumptions about the underlying frames, but have the same conditions for valuations. However, since accessibility between points in the frames need not be reflexive, we have to assume, besides the usual intuitionistic heredity, the converse of heredity, which says that if a formula holds (...) in all points accessible to a point x, then it holds in x. Among frames of rudimentary Kripke models, particular attention is paid to those that guarantee that the assumption of heredity and converse heredity for propositional variables implies heredity and converse heredity for all propositional formulae. These frames need to be neither reflexive nor transitive. (shrink)

We present an axiomatization of the non-associative Lambek calculus extended with classical negation for which the frame semantics with the classical interpretation of negation is sound and complete.

We prove that algebras of binary relations whose similarity type includes intersection, union, and one of the residuals of relation composition form a nonfinitely axiomatizable quasivariety and that the equational theory is not finitely based. We apply this result to the problem of the completeness of the positive fragment of relevance logic with respect to binary relations.

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.

In this paper we give relational semantics and an accompanying relational proof theory for full Lambek calculus (a sequent calculus which we denote by FL). We start with the Kripke semantics for FL as discussed in [11] and develop a second Kripke-style semantics, RelKripke semantics, as a bridge to relational semantics. The RelKripke semantics consists of a set with two distinguished elements, two ternary relations and a list of conditions on the relations. It is accompanied by a Kripke-style valuation system (...) analogous to that in [11]. Soundness and completeness theorems with respect to FL hold for RelKripke models. Then, in the spirit of the work of Orlowska [14], [15], and Buszkowski and Orlowska [3], we develop relational logic RFL. The adjective relational is used to emphasize the fact that RFL has a semantics wherein formulas are interpreted as relations. We prove that a sequent Γ → α in FL is provable if and only if a translation, t( $\gamma_1 \bullet \cdots \bullet \gamma_n \supset \alpha)\varepsilon \upsilon u$ , has a cut-complete fundamental proof tree. This result is constructive: that is, if a cut-complete proof tree for $t(\gamma_1 \bullet \cdots \bullet \gamma_n \supset \alpha)\varepsilon \upsilon u$ is not fundamental, we can use the failed proof search to build a relational countermodel for $t(\gamma_1 \bullet \cdots \bullet \gamma_n \supset \alpha)\varepsilon \upsilon u$ and from this, build a RelKripke countermodel for $\gamma_1 \bullet \cdots \bullet \gamma_n \supset \alpha$ . These results allow us to add FL, the basic substructural logic, to the list of those logies of importance in computer science with a relational proof theory. (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 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)

It is shown that both classical and intuitionistic propositional logics of an associative binary modality are undecidable. The proof is based on the deduction theorem for these logics.

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.

Grishin algebras are a generalisation of Boolean algebras that provide algebraic models for classical bilinear logic with two mutually cancelling negation connectives. We show how to build complete Grishin algebras as algebras of certain subsets (“propositions”) of cover systems that use an orthogonality relation to interpret the negations. The variety of Grishin algebras is shown to be closed under MacNeille completion, and this is applied to embed an arbitrary Grishin algebra into the algebra of all propositions of some cover system, (...) by a map that preserves all existing joins and meets. This representation is then used to give a cover system semantics for a version of classical bilinear logic that has first-order quantifiers and infinitary conjunctions and disjunctions. (shrink)

The problem of whether Lambek Calculus is complete with respect to (w.r.t.) relational semantics, has been raised several times, cf. van Benthem (1989a) and van Benthem (1991). In this paper, we show that the answer is in the affirmative. More precisely, we will prove that that version of the Lambek Calculus which does not use the empty sequence is strongly complete w.r.t. those relational Kripke-models where the set of possible worlds,W, is a transitive binary relation, while that version of the (...) Lambek Calculus where we admit the empty sequence as the antecedent of a sequent is strongly complete w.r.t. those relational models whereW=U×U for some setU. We will also look into extendability of this completeness result to various fragments of Girard's Linear Logic as suggested in van Benthem (1991), p. 235, and investigate the connection between the Lambek Calculus and language models. (shrink)

In this paper we compare grammatical inference in the context of simple and of mixed Lambek systems. Simple Lambek systems are obtained by taking the logic of residuation for a family of multiplicative connectives /,,\, together with a package of structural postulates characterizing the resource management properties of the connective.Different choices for Associativity and Commutativity yield the familiar logics NL, L, NLP, LP. Semantically, a simple Lambek system is a unimodal logic: the connectives get a Kripke style interpretation in terms (...) of a single ternary accessibility relation modeling the notion of linguistic composition for each individual system.The simple systems earch have their virtues in linguistic analysis. But none of them in isolation provides a basis for a full theory of grammar. In the second part of the paper, we consider two types of mixed Lambek systems. (shrink)

Recently M. Szabolcs [12] has shown that many substructural logics including Lambek CalculusL are complete with respect to relativized Relational Semantics. The current paper proves that it is sufficient forL to consider a relativization to the relation x dividesy in some fixed semigroupG.

This paper studies the relation between some extensions of the non-associative Lambek Calculus NL and their interpretation in tree models (free groupoids). We give various examples of sequents that are valid in tree models, but not derivable in NL. We argue why tree models may not be axiomatizable if we add finitely many derivation rules to NL, and proceed to consider labeled calculi instead.We define two labeled categorial calculi, and prove soundness and completeness for interpretations that are almost the intended (...) one, namely for tree models where some branches of some trees may be resp. all branches of all trees must be infinitely extending. Extrapolating from the experiences in our quite simple systems, we briefly discuss some problems involved with the introduction of labels in categorial grammar, and argue that many of the basic questions are not yet understood. (shrink)