权益分类	功能权益	普通用户	{{item.name}}会员
{{category.name}}	{{benefitItem.name}}

A Study of Substractural Logics

减法逻辑研究

基本信息

批准号：
10640103
负责人：
KOMORI Yuichi
金额：
$ 2.43万
依托单位：
Chiba University
依托单位国家：
日本
项目类别：
Grant-in-Aid for Scientific Research (C)
财政年份：
1998
资助国家：
日本
起止时间：
1998 至 1999
项目状态：
已结题

来源：
https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-10640103/
关键词：
Substructural Logic Classical Logic Intuitionistic Logic BCK Logic Lambda Calculus Type Theory

项目摘要

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.

1.最近lambda演算联合了子结构逻辑、直觉逻辑和经典逻辑的研究。在此背景下，鹿岛为经典蕴涵逻辑提出了一个自然演绎系统。他的体系有三个规则，即隐含排除规则、隐含引入规则和格规则。小森注意到，隐含的引入是从判例规则和弱化中派生出来的。因此，我们从鹿岛的系统出发，用弱化代替蕴涵的引入，得到了系统TAμ。类型分配系统TAλ给出了蕴涵直觉主义逻辑的自然演绎，而类型分配系统TAμ给出了经典蕴涵逻辑的自然演绎。此外，对于任何经典蕴涵定理α，都存在TAμ中的α具有子公式性质的证明.更多的λ-演算可以在μ-演算中模拟.一个新的微积分系统从上述结果中产生。我们正在研究新微积分的意义。藤田在多结论自然演绎系统和λμ-演算方面进行了积极的研究，撰写了多篇论文. BB'IW逻辑的可判定性问题是数学中最困难的问题之一。我们正在努力解决这个问题。金泽对范畴语法进行了研究，取得了很好的结果.樱井研究了范畴模型的微积分，并写了两篇很好的论文。