Relational Models for the Lambek Calculus with Intersection and Constants

2025-04-29 0 0 488.12KB 27 页 10玖币

侵权投诉

Logical Methods in Computer Science

Volume 19, Issue 4, 2023, pp. 32:1–32:27

https://lmcs.episciences.org/

Submitted Oct. 04, 2022

Published Dec. 18, 2023

RELATIONAL MODELS FOR THE LAMBEK CALCULUS

WITH INTERSECTION AND CONSTANTS ∗

STEPAN L. KUZNETSOV

Steklov Mathematical Institute of RAS, 8 Gubkina St., Moscow, Russia

e-mail address: sk@mi-ras.ru

Abstract.

We consider relational semantics (R-models) for the Lambek calculus extended

with intersection and explicit constants for zero and unit. For its variant without constants

and a restriction which disallows empty antecedents, Andr´eka and Mikul´as (1994) prove

strong completeness. We show that it fails without this restriction, but, on the other hand,

prove weak completeness for non-standard interpretation of constants. For the standard

interpretation, even weak completeness fails. The weak completeness result extends to an

inﬁnitary setting, for so-called iterative divisions (Kleene star under division). We also

prove strong completeness results for product-free fragments.

Introduction

The Lambek calculus Lwas originally introduced back in 1958 for modelling natural lan-

guage syntax [

Lam58

]. From a modern point of view, the Lambek calculus is considered

as the most basic associative substructural logic, being the algebraic logic of residuated

semigroups [

GJKO07

]. On the other hand, as noticed by Abrusci [

Abr90

], the Lambek

calculus can be viewed as a non-commutative, multiplicative-only variant of Girard’s [

Gir87

]

linear logic.

A residuated semigroup is a semigroup with a partial order

⪯

and division operations

and /obeying the following equivalences:

b⪯a\c⇐⇒ a·b⪯c⇐⇒ a⪯c / b.

Notice that here divisions and multiplication are connected via partial order, not equality.

The idea of such divisions, also called residuals, goes back to the works of Krull [

Kru24

] and

Ward and Dilworth [WD39].

Formulae of the Lambek calculus are built from a variables using the operations of

residuated semigroups:

. From the point of view of ﬁrst-order logic, such formulae

are terms in the signature of residuated semigroups. Furthermore, Loperates expressions

of the form

A→B

, where

and

are formulae. Here

→

corresponds to

⪯

, thus, from

Key words and phrases: Lambek calculus, relational semantics, completeness.

∗This article is an extended version of the conference paper presented at RAMiCS 2021.

The author is grateful to Daniel Rogozin for fruitful discussions. The work was supported by the Theoretical

Physics and Mathematics Advancement Foundation “BASIS”.

LOGICAL METHODS

IN COMPUTER SCIENCE DOI:10.46298/LMCS-19(4:32)2023

⃝Creative Commons

32:2 S. L. Kuznetsov Vol. 19:4

the ﬁrst-order point of view, these are atomic formulae. We call such expressions atomic

sequents.

The set of theorems of Lcan be semantically described as the set of all sequents which

are true on any residuated semigroup under any interpretation of variables. Syntactically,

Lis axiomatised as a Gentzen-style sequent calculus [

Lam58

]. This calculus is presented

in Section 1 below. Derivable objects of this sequent calculus are sequents of the form

A1, . . . , An→B, which generalise atomic sequents deﬁned above.

Natural language applications, connections to linear logic, and algebraic interpretations

on residuated structures suggest extending the Lambek calculus with extra operations.

Adding new operations and constants to the algebraic construction of residated semigroups

results in extending the Lambek calculus. In this article, we focus on extending Lwith the

following:

•the unit constant 1, which is the unit for multiplication;

•

the zero constant 0, which is the smallest element for

⪯

(using division operations one

can also prove that 0is the zero element for multiplication);

•

the intersection, or meet operation

∧

a∧b

inf⪯{a, b}

; meet turns the preorder into a

lower semilattice.

Note that extending Lwith 1and ∧is also due to Lambek [Lam61, Lam69].

An intricate issue arises when extending Lwith the unit constant 1: unlike most others,

this extension is not a conservative one. Consider the atomic sequent (

p\p

)

\q→q

, which

belongs to the original language of L. This atomic sequent is true on all residuated monoids

(i.e., residuated semigroups with the unit). However, it fails to be true on all residuated

semigroups (which form a larger class of algebraic structures).

Thus, even in the language without 1, the algebraic logic of all residuated monoids

diﬀers from L. This logic is called the Lambek calculus allowing empty antecedents [

Lam61

]

and is commonly denoted by L

∗

. We prefer, however, an alternative notation, L

, in order

to avoid notation conﬂicts with Kleene star which we shall use, in the form of iterative

divisions, in one of the sections of this article. The term “... allowing empty antecedents”

comes from the Gentzen-style formulation, see Section 1 below.

Residuated algebraic structures provide a very abstract and general framework for

semantics of the Lambek calculus, its variants and extensions. This is traditional provability

semantics, which interprets theoremhood and entailment, not proofs. More modern semantics

of proofs (see, e.g., [AH96, BS96, CGS13, dPE18]) are beyond the scope of this article.

As usual, proving completeness results for abstract algebraic semantics is a simple

application of the Lindenbaum – Tarski construction (cf. [

BP89

]). This construction gives

strong completeness, that is, completeness not only for theoremhood, but also for the

entailment relation (derivability vs. semantic entailment from sets of hypotheses). More

interesting issues arise when one starts concretising algebraic semantics, that is, considers

speciﬁc classes of algebras. Completeness theorems for such classes, if they hold, are non-

trivial results. We shall also see cases where completeness fails, or holds only in the weak

sense (for theoremhood, not for entailment).

This article concentrates on relational models, or R-models. In R-models, variables and

formulae are interpreted as binary relations over a non-empty set

. The set

(

W×W

) of

all binary relations over

has a natural structure of residuated monoid. Multiplication is

relation composition:

R·S=R◦S={(x, z)|(∃y∈W) ((x, y)∈Rand (y, z)∈S)}.

Vol. 19:4 R-MODELS FOR THE LAMBEK CALCULUS WITH INTERSECTION AND CONSTANTS 32:3

Divisions are deﬁned as follows:

R\S={(y, z)|(∀x∈W) ((x, y)∈R⇒(x, z)∈S},

S / R ={(x, y)|(∀z∈W) ((y, z)∈R⇒(x, z)∈S}.

The rˆole of the unit is played by the diagonal relation

{

(

x, x

)

|x∈W}

. The preorder is

the set inclusion relation

⊆

. Meet is set-theoretic intersection, and zero is the empty relation

∅.

Interpretations of the Lambek calculus on residuated monoids of all binary relations

on a non-empty set

are called unrelativised or square R-models. Unrelativised R-models

give natural semantics for L

; the completeness theorem was proved by Andr´eka and

Mikul´as [

AM94

]. Notice that the argument used for proving this completeness result does

not easily extend to 0,1, and

∧

. Issues with R-models for these extensions form the main

topic of this article.

More precisely, constants 0and 1ruin completeness w.r.t. square R-models, even in

the weak sense (see Section 2 below). In order to overcome this, we introduce variations of

R-models with non-standard interpretation of constants.

As for the extension of L

with intersection, Mikul´as [

Mik15a

Mik15b

] proves complete-

ness w.r.t. square R-models, but only in the weak sense. We show (Section 4) that this is

essential, and strong completeness fails. On the other hand, we strengthen Mikul´as’ result

by adding constants 0and 1, with non-standard interpretations. Our argument also gives an

alternative proof of Mikul´as’ result (without constants), which happens to be extendable to

an inﬁnitary extension of the calculus, with so-called iterative divisions (Section 5). Finally,

we show that strong completeness restores for the variant of L

with meet (intersection) but

without product (Section 7). Thus, the results presented in this article ﬁll some gaps in the

theory of R-models for extensions of L

Λ.

In order to provide adequate semantics for the original Lambek calculus L, one needs to

relax the deﬁnition of R-model. This is done by relativising it. Namely, instead of all binary

relations on

one may now consider only subsets of a ﬁxed transitive relation

, which is

called the “universal” one. By transitivity, composition (product) keeps this relativisation

in place; for divisions, again, one needs to impose it implicitly:

R\US={(y, z)∈U|(∀x∈W) ((x, y)∈R⇒(x, z)∈S)},

and similarly for

S /

. This deﬁnition of division operations signiﬁcantly depends on

the choice of

. In particular, replacing

by a superset might alter

and

. Square

R-models are a particular case of relativised ones, with U=W×W.

Since

is not required to be reﬂexive, in relativised R-models we deal with residuated

semigroups, not monoids, that is, a class of models for L, not L

. And indeed, as proved

also by Andr´eka and Mikul´as [

AM94

], Lis complete w.r.t. relativised R-models. Moreover,

unlike the L

Λcase, this result keeps valid for the extension of Lwith ∧.

Before going further, let us brieﬂy compare R-models with other classes of models for

the Lambek calculus and its extensions, which ﬁt into the general algebraic framework.

The original linguistic motivation of the Lambek calculus suggests interpretations on

the algebra of formal languages. Such models are called language models or L-models. In

L-models, multiplication is pairwise concatenation, and divisions are deﬁned in a natural

way. The diﬀerence between Land L

is reﬂected by absence or presence of the empty

word in the languages considered. Refraining from the empty word (which is, by the way,

motivated by linguistic applications [

MR12

,§2.5]) modiﬁes the deﬁnition of divisions, just

32:4 S. L. Kuznetsov Vol. 19:4

like relativisation in R-models. Completeness theorems for Land L

w.r.t. corresponding

versions of L-models were proved by Pentus [

Pen95

Pen98

]. Language models might look

quite similar to relational ones. However, there is the following signiﬁcant diﬀerence: while

any two words can be concatenated, for arrows in relations (i.e., pairs of elements of

)

this is possible only if the end of the ﬁrst one coincides with the beginning of the second

one. Thus, unlike algebras of formal languages, algebras of relations have divisors of zero: if

|W|>1, there exist non-empty relations Rand Sover Wsuch that R◦S=∅.

Language models may be viewed as models on powersets of free semigroups (for L) or

free monoids (for L

). This suggests considering models on powersets of arbitrary semigroups

or monoids (see [

Bus86

Bus96

]), since all of them have well-deﬁned division operations, and

also zero, unit, and intersection.

The well-known phase semantics for linear logic [

Gir95

Abr91

dG05

KOT06

], which

is also connected to denotational semantics [

BE01

], is another species of semantics based

on powersets of monoids. The crucial diﬀerence from L-models, however, is the usage of a

closure operator, which in case of phase semantics is the operator taking the biorthogonal

of a subset. Another variation of L-models which also uses a closure operation, but of a

diﬀerent nature, is the syntactic concept lattice semantics proposed by Wurm [

Wur17

]. In

the same article Wurm also proposed a similar variant of R-models, also augmented with

closure operations.

In the presence of closure operations, completeness proofs run more smoothly and cover

richer extensions of the original system. In particular, besides meet one can also consider

join (additive disjunction). For relational or language semantics without closure operations,

where meet and join are set-theoretic intersection and union, adding join immediately leads

to incompleteness, since the distributivity law (and its corollaries with only divisions and

join, but not meet) is generally true, but not derivable in the calculus [

OK85

KKS22

With closure operators, distributivity is no longer generally true, which opens the way to

completeness in the presence of join. In this article, we consider R-models without closure

operators, and therefore consider only meet, not join.

Finally, relational models considered in this article should not be confused with ternary

relational semantics for substructural logics (in particular, variants of the Lambek calculus),

which oﬀer a more Kripke-style approach (see [Doˇs92, CGvR14]).

The rest of the article is organised as follows.

•

In Section 1, we give accurate deﬁnitions of the calculus in question, denoted by L

Λ∧

01,

and R-models for it. Here we also formulate known completeness results, by Andr´eka and

Mikul´as [AM94, Mik15a, Mik15b].

•

In Section 2, we provide examples showing that each of the explicit constants 0and 1

ruins completeness, even in the weak sense (the example for 1is not a new one). As a

workaround, we relax the deﬁnition of R-models and deﬁne R-models with non-standard

interpretations of constants.

•

For these non-standard models, in Section 3 we prove weak completeness of L

Λ∧

01. As a

corollary, we obtain an alternative proof of Mikul´as’ completeness result [

Mik15a

Mik15b

]

for the fragment of L

Λ∧01 without constants.

•

Strong completeness fails, as proved in Section 4. The counterexample used in this section

was suggested by Mikul´as [Mik15b], but without proof. Here we ﬁll this gap.

•

In Section 5, we extend our weak completeness result to an inﬁnitary setting. Namely, we

consider so-called iterative divisions, which are Kleene stars in denominators of division

operations. Being axiomatised by

-rules, iterative divisions are in fact inﬁnite intersections.

Vol. 19:4 R-MODELS FOR THE LAMBEK CALCULUS WITH INTERSECTION AND CONSTANTS 32:5

The result of Section 5 solves a natural question suggested by the earlier work [

KR20

Namely, while [

KR20

] features R-completeness for the calculus with positive iterative

divisions under Lambek’s restriction, Theorem 5.1 of Section 5 provides the corresponding

completeness result without Lambek’s restriction.

•

The last two sections are devoted to the product-free fragment of L

Λ∧

01. We show

(Section 7) that, if one removes the product, then strong completeness can be restored, but

w.r.t. a modiﬁed class of models. However, inside the proof we essentially use the product,

which raises a conservativity issue. Conservativity is proved in Section 6 in the strong form,

i.e., for derivability from hypotheses, using an extension of L

Λ∧

01 with the exponential

modality (which allows a modalised variant of deduction theorem, cf. [

LMSS92

]). An

important corollary of the strong completeness result is that if we consider the product-free

fragment without constants (that is, in the language of

, and

∧

), then it will be strongly

complete w.r.t. square R-models in the standard sense.

This journal article is an extended version of the conference paper [

Kuz21

], presented

at RAMiCS 2021 and published in its proceedings. The extension here is twofold. First,

along with the unit constant 1, now we also consider the zero constant 0. We show that

this constant also raises issues with completeness, and resolve them using a non-standard

interpretation for 0also. Second, we add Section 7 (and Section 6 supporting it) with the

strong completeness result for the product-free fragment. This result was presented as a

short talk at AiML 2022, without formal publication.

1. The Lambek Calculus with Intersection and R-Models

Let us recall the formulation of L

Λ∧

01, the Lambek calculus with intersection and constants,

in the form of a Gentzen-style sequent calculus. Formulae are constructed from variables

(

p, q, r, . . .

) and constants 0(zero) and 1(unit) using four binary connectives:

(multipli-

cation),

(left division),

(right division), and

∧

(intersection). The set of all formulae

is denoted by

. Formulae are denoted by capital Latin letters. Capital Greek letters

denote sequences of formulae. Sequents are expressions of the form Π

→B

. (Due to the

non-commutative nature of the Lambek calculus, order in Π matters.) Here Π is called the

antecedent and Bthe succedent of the sequent.

Letter Λ, which appears in the name of the calculus, denotes the empty sequence of

formulae. However, in sequents with empty antecedents we omit it and write just

→B

instead of Λ →B.

The axioms and inference rules are as follows:

A→AId Π→AΓ, A, ∆→C

Γ,Π,∆→CCut

Π→AΓ, B, ∆→C

Γ,Π, A \B, ∆→C\LA, Π→B

Π→A\B\RΓ, A, B, ∆→C

Γ, A ·B, ∆→C·L

Π→AΓ, B, ∆→C

Γ, B / A, Π,∆→C/ L Π, A →B

Π→B / A / R Π→A∆→B

Π,∆→A·B·R

Γ, A, ∆→C

Γ, A ∧B, ∆→C∧L1

Γ, B, ∆→C

Γ, A ∧B, ∆→C∧L2Π→AΠ→B

Π→A∧B∧R

Γ,0,∆→C0LΓ,∆→C

Γ,1,∆→C1L→11R

文档加载中……请稍候！
如果长时间未打开，您也可以点击刷新试试。

下载文档到电脑，查找使用更方便

10 玖币 0人已下载

立即下载

摘要：

LogicalMethodsinComputerScienceVolume19,Issue4,2023,pp.32:1–32:27https://lmcs.episciences.org/SubmittedOct.04,2022PublishedDec.18,2023RELATIONALMODELSFORTHELAMBEKCALCULUSWITHINTERSECTIONANDCONSTANTS∗STEPANL.KUZNETSOVSteklovMathematicalInstituteofRAS,8GubkinaSt.,Moscow,Russiae-mailaddress:sk@mi-ras.r...

展开>> 收起<<

Relational Models for the Lambek Calculus with Intersection and Constants.pdf

共27页,预览5页

还剩页未读，继续阅读

声明：本站为文档C2C交易模式，即用户上传的文档直接被用户下载，本站只是中间服务平台，本站所有文档下载所得的收益归上传人(含作者)所有。玖贝云文库仅提供信息存储空间，仅对用户上传内容的表现方式做保护处理，对上载内容本身不做任何修改或编辑。若文档所含内容侵犯了您的版权或隐私，请立即通知玖贝云文库，我们立即给予删除！

Relational Models for the Lambek Calculus with Intersection and Constants

相关推荐

开通VIP享超值会员特权

作者详情

相关内容

热门标签

举报选择: