Substructural Logics on Display
Substructural Logics on Display
复制标题
展示的底层逻辑
作者：
R. Goré
传统上，子结构逻辑是通过从根岑的微积分LK或LJ中删除部分或全部结构规则来获得的。众所周知，通常的逻辑连接词然后分裂成一个以上的连接词。或者，我们可以从（直觉主义）Lambek演算开始，它包含这些多个连接词，并以增量的方式获得许多逻辑，如：指数自由线性逻辑，相关逻辑，BCK逻辑和直觉主义逻辑。这些逻辑中的每一个也有一个经典的对应，有些也有一个“循环”的对应。这些逻辑已经被广泛研究，并得到很好的理解。进一步推广，我们可以从直觉主义的Bi-Lambek逻辑开始，它包含来自Lambek演算的每个连接词的对偶。结构规则的添加然后以增量方式再次给出双线性、双相关、双BCK和双直觉逻辑。这些逻辑中的每一个也有一个经典的对应，有些甚至有一个“循环”的对应。Bi-Lambek逻辑的这些（双直觉主义和双经典）扩展并没有得到很好的理解。例如，经典Bi-Lambek逻辑的割消并不完全清楚，因为一些割规则有要求某些成分为空或非空的副条件。Nuel Belnap的显示逻辑是一个通用的Gentzen风格的证明理论框架，旨在在一个统一的设置中捕获许多不同的逻辑。显示逻辑的美是一个普遍的切消定理，由于贝尔纳普，适用于任何时候的规则显示演算遵守某些，容易检查，条件。原始的显示逻辑及其各种各样的体现，不适合以统一的方式捕获双直觉和双经典逻辑。我们补救这种情况，给一个单一的（切自由）显示演算的双兰贝克演算，从所有著名的（双直觉和双经典）扩展获得的增量增加的结构规则的逻辑引入规则的恒定核心。我们强调内在的二重性和对称性，在这个框架内获得“四个证明的价格之一”。我们给出了代数语义的Bi-Lambek逻辑，并证明了我们的演算是健全的和完整的这些语义。我们将展示如何定义一个替代显示演算双经典的子结构逻辑使用否定，而不是影响，作为原语。借用其他显示演算，我们展示了如何扩展我们的显示演算来处理双直觉主义或双经典的子结构逻辑，其中包含时态逻辑中熟悉的向前和向后模态，线性逻辑的指数，关系代数中熟悉的匡威运算符，四个否定，以及对应于Sheffer的“匕首”和“中风”的非经典类似物的两个不寻常的模态，都是模块化的。使用Gaggle理论的邓恩，我们概述了二元和一元内涵连接词的关系语义，但没有尝试这样做的外延连接词，或指数。最后，我们充实了一个建议，Lambek嵌入直觉逻辑使用两个不寻常的“指数”，并表明，这些“指数”本质上是紧张的逻辑模态，很不符合通常的指数。使用display属性的细化，您可以从这些可能性中进行选择，以构造满足您需要的显示演算。
Substructural logics are traditionally obtained by dropping some or all of the structural rules from Gentzen’s sequent calculi LK or LJ. It is well known that the usual logical connectives then split into more than one connective. Alternatively, one can start with the (intuitionistic) Lambek calculus, which contains these multiple connectives, and obtain numerous logics like: exponential-free linear logic, relevant logic, BCK logic, and intuitionistic logic, in an incremental way. Each of these logics also has a classical counterpart, and some also have a “cyclic” counterpart. These logics have been studied extensively and are quite well understood. Generalising further, one can start with intuitionistic Bi-Lambek logic, which contains the dual of every connective from the Lambek calculus. The addition of the structural rules then gives Bi-linear, Bi-relevant, Bi-BCK and Bi-intuitionistic logic, again in an incremental way. Each of these logics also has a classical counterpart, and some even have a “cyclic” counterpart. These (bi-intuitionistic and bi-classical) extensions of Bi-Lambek logic are not so well understood. Cut-elimination for Classical Bi-Lambek logic, for example, is not completely clear since some cut rules have side conditions requiring that certain constituents be empty or non-empty. The Display Logic of Nuel Belnap is a general Gentzen-style proof theoretical framework designed to capture many different logics in one uniform setting. The beauty of display logic is a general cut-elimination theorem, due to Belnap, which applies whenever the rules of the display calculus obey certain, easily checked, conditions. The original display logic, and its various incarnations, are not suitable for capturing bi-intuitionistic and bi-classical logics in a uniform way. We remedy this situation by giving a single (cut-free) Display calculus for the Bi-Lambek Calculus, from which all the well-known (bi-intuitionistic and bi-classical) extensions are obtained by the incremental addition of structural rules to a constant core of logical introduction rules. We highlight the inherent duality and symmetry within this framework obtaining “four proofs for the price of one”. We give algebraic semantics for the Bi-Lambek logics and prove that our calculi are sound and complete with respect to these semantics. We show how to define an alternative display calculus for bi-classical substructural logics using negations, instead of implications, as primitives. Borrowing from other display calculi, we show how to extend our display calculus to handle bi-intuitionistic or bi-classical substructural logics containing the forward and backward modalities familiar from tense logic, the exponentials of linear logic, the converse operator familiar from relation algebra, four negations, and two unusual modalities corresponding to the non-classical analogues of Sheffer’s “dagger” and “stroke”, all in a modular way. Using the Gaggle Theory of Dunn we outline relational semantics for the binary and unary intensional connectives, but make no attempt to do so for the extensional connectives, or the exponentials. Finally, we flesh out a suggestion of Lambek to embed intuitionistic logic using two unusual “exponentials”, and show that these “exponentials” are essentially tense logical modalities, quite at odds with the usual exponentials. Using a refinement of the display property, you can pick and choose from these possibilities to construct a display calculus for your needs.