1999 Fiscal Year Final Research Report Summary
A Study of Substractural Logics
| Project/Area Number |
10640103
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Single-year Grants |
|---|
| 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)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
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)
FUJITA Ken-etsu Kyusyu University, Faculty of Informatic Technology, Lecturer, 情報工学部, 講師 (30228994)
HIROKAWA Sachiko Kyusyu University, Computer Center, Professor, 大型計算センター, 教授 (40126785)
|
|---|
| Project Period (FY) |
1998 – 1999
|
| Keywords | Substructural Logic / Classical Logic / Intuitionistic Logic / BCK Logic / Lambda Calculus / Type Theory |
|---|
| 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 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.
|
