A Study of Substractural Logics

1. 近年来，λ演算将子结构逻辑、直觉逻辑和经典逻辑的研究结合起来。在此背景下，鹿岛提出了经典蕴涵逻辑的自然演绎体系。他的制度有三条规则，即排除蕴涵、引入蕴涵和判例规则。小森注意到，暗示的引入可以从案例规则和弱化中推导出来。因此，我们用弱化取代隐含的引入，从鹿岛系统中得到了系统TAμ。类型赋值系统ta λ给出了蕴涵直觉逻辑的自然演绎，而类型赋值系统ta μ给出了经典蕴涵逻辑的自然演绎。此外，对于任何经典蕴涵定理α，在TAμ中存在具有子公式性质的α的证明。μ-calculus 2中还可以模拟更多的λ-calculus。由上述结果导出了一种新的微积分体系。我们正在研究新微积分的意义。藤田积极研究多结论自然演绎系统和λμ微积分，并发表了多篇论文。关于BB'IW逻辑的可决性问题是最困难的数学问题之一。我们正在努力解决这个问题。金泽研究了范畴语法，并取得了优异的成绩。Sakurai研究了λ微积分的范畴模型，并写了两篇很好的论文。

1. Recently lambda calculus unites studies of substructural logics, the intutionistic logic and the classical logic. In this context, Kashima has posed a Natural deduction system for the classical implicational logic. His system has three rules, the elimination of the implication, the introduction of the implication and the case rule. Komori has noticed that the introduction of the implication is derivable from the case rule and the weakening. So we have gotten the system TAμ from Kashima's system by replacing the introduction of implication by the weakening. While the type assignment system TAλgives a natural deduction for implicational intuitionistic logic, the type assignment system TAμgives a natural deduction for classical implicational logic. Moreover for any classical implicational theorem α there exists a proof of α in TAμ enjoying the subformula property. Still more λ-calculus can be simulated in μ-calculus.2. A new system of calculus comes out of the above result. We are investigating the meaning of the new calculus.3. Fujita has actively studied on multiple-conclusion natural deduction system and λμ-calculus, and then has written many papers.4. The problem on the decidablity of BB'IW logic in one of the most difficult mathematical problem. We are wrestling with the problem.5. Kanazawa has investigated Categorial Grammars and has gotten excellent results.6. Sakurai has investigated Categorical model of lambda-calculus and has written two good papers.