In [5] we study Nonassociative Lambek Calculus augmented with De Morgan negation, satisfying the double negation and contraposition laws. This logic, introduced by de Grooté and Lamarche [10], is called Classical Non-Associative Lambek Calculus. Here we study a weaker logic InNL, i.e. NL with two involutive negations. We present a one-sided sequent system for InNL, admitting cut elimination. We also prove that InNL is PTIME.

We provide an algorithm for determining a categorial grammar from linguistic data that essentially uses unification of type-schemes assigned to atoms. The algorithm presented here extends an earlier one restricted to rigid categorial grammars, introduced in [4] and [5], by admitting non-rigid outputs. The key innovation is the notion of an optimal unifier, a natural generalization of that of a most general unifier.

We prove the finite model property (fmp) for BCI and BCI with additive conjunction, which answers some open questions in Meyer and Ono [11]. We also obtain similar results for some restricted versions of these systems in the style of the Lambek calculus [10, 3]. The key tool is the method of barriers which was earlier introduced by the author to prove fmp for the product-free Lambek calculus [2] and the commutative product-free Lambek calculus [4].

Compact Bilinear Logic , introduced by Lambek [14], arises from the multiplicative fragment of Noncommutative Linear Logic of Abrusci [1] by identifying times with par and 0 with 1. In this paper, we present two sequent systems for CBL and prove the cut-elimination theorem for them. We also discuss a connection between cut-elimination for CBL and the Switching Lemma from [14].

Action logic of Pratt [21] can be presented as Full Lambek Calculus FL [14, 17] enriched with Kleene star *; it is equivalent to the equational theory of residuated Kleene algebras (lattices). Some results on axiom systems, complexity and models of this logic were obtained in [4, 3, 18]. Here we prove a stronger form of *-elimination for the logic of *-continuous action lattices and the –completeness of the equational theories of action lattices of subsets of a finite monoid and (...) action lattices of binary relations on a finite universe. We also discuss possible applications in linguistics. (shrink)

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.

Some notions of the logic of questions (presupposition of a question, validation, entailment) are used for defining certain kinds of completeness of elementary theories. Presuppositional completeness, closely related to -completeness ([3], [6]), is shown to be fulfilled by strong elementary theories like Peano arithmetic.

Pentus (1992) proves the equivalence of LCG's and CFG's, and CFG's are equivalent to BCG's by the Gaifman theorem (Bar-Hillel et al., 1960). This paper provides a procedure to extend any LCG to an equivalent BCG by affixing new types to the lexicon; a procedure of that kind was proposed as early, as Cohen (1967), but it was deficient (Buszkowski, 1985). We use a modification of Pentus' proof and a new proof of the Gaifman theorem on the basis of (...) the Lambek calculus. (shrink)

The three essays presented here concern natural connections between grammatical derivations and structures provided by certain standard grammar formalisms, on the one hand, and deductions in logical systems, on the other hand. In the first essay we analyse the adequacy of Polish notation for higher-order languages. The Ajdukiewicz algorithm (Ajdukiewicz 1935) is discussed in terms of generalized MP-deductions. We exhibit a failure in Ajdukiewicz’s original version of the algorithm and give a correct one; we prove that generalized MP-deductions have the (...) frontier property, which is essential for the plausibility of Polish notation. The second essay deals with logical systems corresponding to different grammar formalisms, as e.g. Finite State Acceptors, Context-Free Grammars, Categorial Grammars, and others. We show how can logical methods be used to establish certain linguistically significant properties of formal grammars. The third essay discusses the interplay between Natural Deduction proofs in grammar oriented logics and semantic structures expressible by typed lambda terms and combinators. (shrink)

van Benthem [1] introduces a variant of Lambek Syntactic Calculus , proposed by Lambek [6], we call the variant Lambek-van Benthem Calculus . As proved by van Benthem, LBC is complete with respect to a semantics of λ-terms. In this note we indicate other relevant properties of LBC , just supporting some expectations of van Benthem. Given a countable set P r, of primitive types, the set T p, of types, is the smallest one such that: T p contains P (...) r, if x, y are in T p then is in T p. The variables x, y, z will range over types. Expressions X → x are to be called reduction formulas. (shrink)

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)

The equivalence of (classical) categorial grammars and context-free grammars, proved by Gaifman [4], is a very basic result of the theory of formal grammars (an essentially equivalent result is known as the Greibach normal form theorem [1], [14]). We analyse the contents of Gaifman's theorem within the framework of structure and type transformations. We give a new proof of this theorem which relies on the algebra of phrase structures and exhibit a possibility to justify the key construction used in Gaifman's (...) proof by means of the Lambek calculus of syntactic types [15]. (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.

Classical categorial grammars are the grammars introduced by Ajdukiewicz [1] and formalized by Bar-Hillel [2], Bar-Hillel et al. [3]. In [3] there is proved the weak equivalence of CCG’s and context-free grammars [6]. In this note we characterize the strong generative capacity of finite and rigid CCG’s, i.e. their capacity of structure generation. These results are more completely discussed in [4], [5].

In Zielonka (1981a, 1989), I found an axiomatics for the product-free calculus L of Lambek whose only rule is the cut rule. Following Buszkowski (1987), we shall call such an axiomatics linear. It was proved that there is no finite axiomatics of that kind. In Lambek's original version of the calculus (cf. Lambek, 1958), sequent antecedents are non empty. By dropping this restriction, we obtain the variant L0 of L. This modification, introduced in the early 1980s (see, e.g., (...) class='Hi'>Buszkowski, 1985; Zielonka, 1981b), did not gain much popularity initially; a more common use of L0 has only occurred within the last few years (cf. Roorda, 1991: 29). In Zielonka (1988), I established analogous results for the restriction of L0 to sequents without left (or, equivalently, right) division. Here, I present a similar (cut-rule) axiomatics for the whole of L0.This paper is an extended, corrected, and completed version of Zielonka (1997). Unlike in Zielonka (1997), the notion of rank of an axiom is introduced which, although inessential for the results given below, may be useful for the expected non-finite-axiomatizability proof.The paper follows the same way of subject exposition as Zielonka (2000) but it is technically much less complicated. I restrict myself to giving bare results; all the ideological background is exactly the same as in case of the non-associative calculusNL0 and those who are interested in it are requested to consult the introductory section of Zielonka (2000). (shrink)

In Zielonka (1981a, 1989), I found an axiomatics for the product-free calculus L of Lambek whose only rule is the cut rule. Following Buszkowski (1987), we shall call such an axiomatics linear. It was proved that there is no finite axiomatics of that kind. In Lambek's original version of the calculus (cf. Lambek, 1958), sequent antecedents are non empty. By dropping this restriction, we obtain the variant L 0 of L. This modification, introduced in the early 1980s (see, e.g., (...) Buszkowski, 1985; Zielonka, 1981b), did not gain much popularity initially; a more common use of L 0 has only occurred within the last few years (cf. Roorda, 1991: 29). In Zielonka (1988), I established analogous results for the restriction of L 0 to sequents without left (or, equivalently, right) division. Here, I present a similar (cut-rule) axiomatics for the whole of L 0. This paper is an extended, corrected, and completed version of Zielonka (1997). Unlike in Zielonka (1997), the notion of rank of an axiom is introduced which, although inessential for the results given below, may be useful for the expected non-finite-axiomatizability proof. (shrink)

Traditional martial arts continue to be interesting and inspiring to many people around the globe. Some of their contemporary adaptations attract enthusiasts for whom they are especially important. In this article, the author bases his observations on his own long-term participation. The analysis takes into account the influence of the perspectives of Jigoro Kano and several other creators of modern varieties of Japanese budo. It can be concluded that regular, even daily, practice—cultivating martial arts and internalizing its values—co-creates the lifestyle (...) of instructors and advanced students. (shrink)

Kazimierz Twardowski attributed high cognitive value to introspection because he believed it plays a fundamental role in psychology, the primary philosophical discipline. He believed that basing philosophy on inner experience would allow it to obtain universal and justified results. Internal experience consists of perceiving one’s own mental facts; it is non-sensual and selfevident. Twardowski referred to introspection in his investigations in various ways, which is presented in the article.

The Limits of Cognition and the Shape of Being Based on the Thought of Karl Jaspers The article points out the elements of Karl Jaspers’ epistemological conception that cross out the possibility of a comprehensive account of being. The key issue here is the limits of cognition, which take the form of object cognition. The theme of limits points to the inadequacies of human thinking in the context of quantifiable and absolutist representations of reality. The impossibility of adequately grasping the (...) totality of reality will be illustrated here by means of the criticism Jaspers levelled at absolutising metaphysics. In connection with the description of the structure of cognition proposed by Jaspers, the article points out the conceptual proximity of the issue of worldview and metaphysics in the light of the thought of the cited author. (shrink)

Expression of physical motion (e.g., man runs by) shows systematic variability not only between language types (i.e., inter-typological) but also within a language type (i.e., intra-typological). In this study, we asked whether the patterns of variability extend to metaphorical motion events (e.g., time runs by). Our analysis of randomly selected 450 physical motion (150/language) and 450 metaphorical motion (150/language) event descriptions from written texts originally produced by German, Polish, and Spanish authors showed strong inter-typological differences in the expression of both (...) event types. German and Polish speakers differed from Spanish speakers in how they packaged manner and path components of a motion event; they also differed in how extensively they expressed each component in their lexicalization of motion. The strong inter-typological differences were accompanied by more modest intra-typological variability: Polish and German writers differed in their packaging and lexicalization of manner and path components of metaphorical—but not physical—motion events. Our results provide evidence for robust inter-typological differences evident in the expression of both physical and metaphorical motion, along with less robust intra-typological differences, largely evident in the expression of metaphorical motion. Our study thus highlights event type as an important factor in determining crosslinguistic variation in motion expression. (shrink)