2006 Fiscal Year Final Research Report Summary
Regeneration of Church's Lambda calculus on BCK logic
| Project/Area Number |
15540107
|
|---|
| 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, IMIT, Professor, 総合メディア基盤センター, 教授 (10022302)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
SAKURAI Takafumi Chiba University, Faculty of Science, Associate Professor, 理学部, 助教授 (60183373)
YAMAMOTO Mitsuharu Chiba University, Faculty of Science, Associate Professor, 理学部, 助教授 (00291295)
HIROKAWA Sachio Kyushu University, Computing and Communication Center, Professor, 情報基盤センター, 教授 (40126785)
FUJITA Ken-etsu Gunma University, Faculty of Technology, Associate Professor, 工学部, 助教授 (30228994)
KASHIMA Ryo TIT, Associate Professor, 情報理工学研究科, 助教授 (10240756)
|
|---|
| Project Period (FY) |
2003 – 2006
|
| Keywords | Lambda Calculus / BCK Logic / Church / Classical Logic / Curry-Howard isomorphism / Intuitionistic Logic / Russel's Paradox / Illative Combinatory Logic |
|---|
| Research Abstract |
1. To regerate Church's Lambda calculus by the system BCK β η, we have to show that the system BCK β ηcan logically simulate the classical logic. As it is known that the intuitionistic logic can simulate the classical logic, it suffices that we show that the system BCK β η can logically simulate the intuitionistic logic. Komori has posed two methods for simulating the intuitionistic logic and showed the following fact on both the methods :
There exists a trabslation ^* such that A^* is a formula of the system BCK β η and A^* is provable in the system BCK β η for any formula A of the intuitionistic logic.
If we can show the reverse "A is provable in the intuitionistic logic if A^* is provable in the system BCK β η", then it is shown that the system BCK β η can logically simulate the intuitionistic logic. But the reverse is now still open. The translation in one of two methods is simple. The translation in another method is rather complex but I think that the reverse will be proved easier
… More
than the former. On the latter, the reverse is an important open problem.
2. Komori has posed a system, named lambda-rho-calculus. While the type assignment system TA_lambda gives a natural deduction for implicational intuitionistic logic, the type assignment system TA_lambda-rho gives a natural deduction for classical implicational logic. Moreover for any classical implicational theorem A there exists a proof of A in TA_lambda-rho enjoying the subformula property. We have proved the strong normalization theorem for TA_lambda-rho. A fresh idea is used in the proof. The idea can be used in proofs of the strong normalization theorem of other systems. Ryo 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. The author noticed that the introduction of the implication is derivable from the case rule and the weakening. So we have gotten the system TA_mu from Kashima's system by replacing the introduction of implication by the weakening. Then we have discovered the lambda-rho-calculus. Less
|
