陈钰

1 引言

直觉主义逻辑（Intuitionistic Logic,简称Int）相对于满足赋值单调性的自返和传递的克里普克模型类是可靠且完全的。所谓赋值单调性，指的是如果一个命题变元p 在一个点w 上为真，那么p 在w 的每一个可及点上都为真。（[4]）将直觉主义逻辑的克里普克模型类扩大为满足赋值单调性的传递模型类，则可以得到一个比直觉主义逻辑更弱的逻辑——维瑟（A.Visser）在[21]中提出的基本命题逻辑（Basic Propositional Logic，简称BPL）。克罗西（G.Crosi）在[6]中研究了一些现在所说的亚直觉主义逻辑（Subintuitionistic Logics），将其称之为弱逻辑。亚直觉主义逻辑与直觉主义逻辑和基本命题逻辑一样，其蕴涵也是严格蕴涵，而非实质蕴涵。使用严格蕴涵和严格否定但不使用实质蕴涵和实质否定的命题逻辑一般也称为严格蕴涵逻辑。（[9]）

克罗西在[6]中给出的最弱的逻辑是F。雷斯塔尔（G.Restall）在[17]中也研究了亚直觉主义逻辑，并且其提出的逻辑SJ 与F 是等价的（[22]）。就F 的证明系统而言，克罗西（[6]）和雷斯塔尔（[17]）给出的是希尔伯特式公理系统。万星（H.Wansing，[22]）给出了F 及其一些扩张的显示演算（Display Calculus）。塞拉特（C.Cerrato）给出了严格蕴涵逻辑的自然演绎系统。（[3]）石垣和鹿岛（R.Ishigaki&R.Kashima）给出了严格蕴涵逻辑的矢列演算，这些演算使用的是基于集合的矢列。（[9]）此外，他们运用语义的方法证明了切割规则的可容许性在这些演算中成立。马明辉和赵之光（M.Ma&Z.Zhao）使用[5]中提出的统一对应理论（unified correspondence theory）建立起严格蕴涵逻辑的模块化的无切割规则的矢列演算，而且这些演算中关于蕴涵的规则分为左引入规则和右引入规则。（[12]）山崎和佐野（S.Yamasaki&K.Sano）给出了F 和其他严格蕴涵逻辑的G3-型加标的矢列演算，并且证明切割规则在这些演算中是可容许的。……