Lambek Calculus with Conjugates
- PDF / 430,622 Bytes
- 24 Pages / 453.543 x 680.315 pts Page_size
- 38 Downloads / 212 Views
Lambek Calculus with Conjugates
Abstract. 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. Keywords: Conjugates, Lambek Calculus, Modal logic, Routley–Meyer semantics.
1.
Introduction
The Lambek Calculus L is a well known formalism, initially introduced in [27] to reason about strings over a given alphabet but since then studied in a wide variety of different contexts. In the original linguistic interpretation, the basic language of L consists of a countable set of atomic elements P r (representing primitive types of strings) and three binary operators (giving rise to complex types). These are product ◦ (a string x is of type A◦B iff x is a concatenation yz of a string y of type A and z of type B), left division ← (x is of type B ← A iff, for all y of type A, yx is of type B), and right division → (x is of type A → B iff, for all y of type A, xy is of type B).1 According to the original interpretation, ◦ is associative, and L was generalised to the Non-associative Lambek Calculus, N L [28], which does not require product to be associative. In N L the only properties of ←, ◦, and → are the relations of residuation obtaining between them (and consequences of these such as the tonicity properties of the various connectives). It is natural to consider extensions of the basic Lambek language by lattice connectives ∧, ∨; both are added in [23], but [28] already considers 1 We use the notation associated with relevant logics, used in [35]. It is more common in the literature on the Lambek Calculus to use A\B for left division and B/A for right division; this notation is used also in some general algebraic expositions of substructural logics [16].
Presented by Heinrich Wansing; Received November 18, 2019
Studia Logica https://doi.org/10.1007/s11225-020-09913-2
c Springer Nature B.V. 2020
I. Sedl´ ar, A. Tedder
the addition of ∧, and related systems were studied in the context of relevant logic starting in the 60s and 70s.2 One can also add constants expressing neutral elements with respect to the lattice operations, namely, the trivial type [12], neutral with respect to ∧, and the empty type ⊥, neutral with respect to ∨ (not to be confused with the empty word, neutral with respect to product). These additions give rise to DL and DN L, when ∧, ∨ satisfy the usual distributive laws. These versions of the Lambek Calculus have algebraic semantics in terms of various classes of residuated partially ordered algebras [9,16], but they can also be seen as modal logics insofar as they can be given semantics in terms of frames endowed with a ternary accessibility relation. The ternary relation, a variation on that introduced in the semantics of r
Data Loading...
