Regeneration of Church's Lambda calculus on BCK logic

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

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