A Study of Substractural Logics

点击翻译按钮获取中文摘要

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.