Online research in philosophy

The paper continues a series of results on cut-rule axiomatizability of the Lambek calculus. It provides a complete solution of a problem which was solved partially in one of the author''s earlier papers. It is proved that the product-free Lambek Calculus with the empty string (L 0) is not finitely axiomatizable if the only rule of inference admitted is Lambek''s cut rule. The proof makes use of the (infinitely) cut-rule axiomatized calculus C designed by the author exactly for this purpose.

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.

In this paper, we propose a game semantics for the (associative) Lambek calculus . Compared to the implicational fragment of intuitionistic propositional calculus, the semantics deals with two features of the logic: absence of structural rules, as well as directionality of implication. We investigate the impact of these variations of the logic on its game semantics.

In [4], I proved that the product-free fragment L of Lambek's syntactic calculus (cf. Lambek [2]) is not finitely axiomatizable if the only rule of inference admitted is Lambek's cut-rule. The proof (which is rather complicated and roundabout) was subsequently adapted by Kandulski [1] to the non-associative variant NL of L (cf. Lambek [3]). It turns out, however, that there exists an extremely simple method of non-finite-axiomatizability proofs which works uniformly for different subsystems of L (in particular, for NL). We present it below to the use of those who refer to the results of [1] and [4].

Nonassociative Lambek Calculus (NL) is a syntactic calculus of types introduced by Lambek [8]. The polynomial time decidability of NL was established by de Groote and Lamarche [4]. Buszkowski [3] showed that systems of NL with finitely many assumptions are decidable in polynomial time and generate context-free languages; actually the P-TIME complexity is established for the consequence relation of NL. Adapting the method of Buszkowski [3] we prove an analogous result for Nonassociative Lambek Calculus with unit (NL1). Moreover, we show that any Lambek grammar based on NL1 (with assumptions) can be transformed into an equivalent context-free grammar in polynomial time.

We present a novel way of using proof nets for the multimodal Lambek calculus, which provides a general treatment of both the unary and binary connectives. We also introduce a correctness criterion which is valid for a large class of structural rules and prove basic soundness, completeness and cut elimination results. Finally, we will present a correctness criterion for the original Lambek calculus Las an instance of our general correctness criterion.

An extension L + of the non-associative Lambek calculus Lis defined. In L + the restriction to formula-conclusion sequents is given up, and additional left introduction rules for the directional implications are introduced. The system L + is sound and complete with respect to a modification of the ternary frame semantics for L.

The Lambek calculus introduced in Lambek [6] is a strengthening of the type reduction calculus of Ajdukiewicz [1]. We study Associative Lambek Calculus L in Gentzen style axiomatization enriched with a finite set Γ of nonlogical axioms, denoted by L(Γ).It is known that finite axiomatic extensions of Associative Lambek Calculus generate all recursively enumerable languages (see Buszkowski [2]). Then we confine nonlogical axioms to sequents of the form p → q, where p and q are atomic types. For calculus L(Γ) we prove interpolation lemma (modifying the Roorda proof for L [10]) and the binary reduction lemma (using the Pentus method [9] with modification from [3]). In consequence we obtain the weak equivalence of the Context-Free Grammars and grammars based on L(Γ).

We introduce non-associative linear logic, which may be seen as the classical version of the non-associative Lambek calculus. We define its sequent calculus, its theory of proof-nets, for which we give a correctness criterion and a sequentialization theorem, and we show proof search in it is polynomial.

In the Lambek calculus of order 2 we allow only sequents in which the depth of nesting of implications is limited to 2. We prove that the decision problem of provability in the calculus can be solved in time polynomial in the length of the sequent. A normal form for proofs of second order sequents is defined. It is shown that for every proof there is a normal form proof with the same axioms. With this normal form we can give an algorithm that decides provability of sequents in polynomial time.