林哲

中山大学哲学系 中山大学逻辑与认知研究所linzhe8@mail.sysu.edu.cn

梁飞†

山东大学哲学与社会发展学院philoliangfei@gmail.com

1 引言

J.Lambek于1958年为自然语言计算引入了一个句法演算系统。（[7]）现在这个系统被统称为兰贝克演算。在过去几十年间，兰贝克演算在语言逻辑领域受到了广泛的重视，并且发展出许多重要的衍生和扩张。W.Buszkowski于1995年在论文[1]中引入带否定算子的兰贝克演算作为学习范畴语法的核心类型逻辑。Buszkowski在其文章中提出，作为学习范畴语法的核心类型逻辑，其否定规则只需要满足：

·置换性：假如类型A推出类型B，那么有¬B推出¬A，和

·双重否定率：对任何类型A:¬¬A=A。

有别于这种观点，在兰贝克演算的扩张研究中，构造性否定被广泛关注即类型的否定被定义为¬A:=A⊥。由于兰贝克演算一般不具有交换律，因此会产生两个否定。对这样的扩张的研究可以在文献[3,6]中找到详细的阐述。然而构造性否定会带来另外一个问题，即兰贝克矛盾律α·¬α=⊥在逻辑中会变成有效。这条性质缺乏语言逻辑研究的动机，并且还会破坏一些范畴语法系统所需要的性质，因此Buszkowski提出的兰贝克否定扩张更适合作为范畴语法的类型逻辑来研究。但是这种兰贝克演算其判定性是未知的，并且缺乏优秀的根岑演算系统。这会对基于这种类型逻辑范畴语法的进一步研究带来巨大的不便。

在本文我们选择了一种极为接近Buszkowski提出的否定，称为极小否定。极小否定满足置换性和一半的双重否定律：任何类型A推出类型¬¬A，并且在极小否定中对任何¬¬A类型都满足上述否定的两个性质。……