Project/Area Number  10640103 
Research Category 
GrantinAid for Scientific Research (C).

Section  一般 
Research Field 
General mathematics (including Probability theory/Statistical mathematics)

Research Institution  Chiba University 
Principal Investigator 
KOMORI Yuichi Chiba University, Faculty of Science, Professor, 理学部, 教授 (10022302)

CoInvestigator(Kenkyūbuntansha) 
FUJITA Kenetsu Kyusyu University, Faculty of Informatic Technology, Lecturer, 情報工学部, 講師 (30228994)
HIROKAWA Sachiko Kyusyu University, Computer Center, Professor, 大型計算センター, 教授 (40126785)
KANAZAWA Makoto Chiba University, Faculty of Science, Assistant Professor, 文学部, 助教授 (20261886)
YAMAMOTO Mitsuharu Chiba University, Faculty of Science, Research Associate, 理学部, 助手 (00291295)
SAKURAI Takafumi Chiba University, Faculty of Science, Assistant Professor, 理学部, 助教授 (60183373)

Project Fiscal Year 
1998 – 1999

Project Status 
Completed(Fiscal Year 1999)

Budget Amount *help 
¥3,800,000 (Direct Cost : ¥3,800,000)
Fiscal Year 1999 : ¥1,600,000 (Direct Cost : ¥1,600,000)
Fiscal Year 1998 : ¥2,200,000 (Direct Cost : ¥2,200,000)

Keywords  Substructural Logic / Classical Logic / Intuitionistic Logic / BCK Logic / Lambda Calculus / Type Theory / 部分構造論理 / 古典論理 / 直観主義論理 / BCK論理 / ラムダ計算 / 型理論 
Research Abstract 
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 multipleconclusion 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 lambdacalculus and has written two good papers.
