Regeneration of Church's Lambda calculus on BCK logic

1.要用BCKβη系统恢复丘奇的Lambda演算，必须证明系统BCKβη能够逻辑模拟经典逻辑。众所周知，直觉逻辑可以模拟经典逻辑，这足以证明系统BCKβη可以逻辑模拟直觉逻辑。Komori提出了两种模拟直觉逻辑的方法，并证明了这两种方法都有如下事实：存在一个转换^*使得A^*是系统BCKβη的公式，且A^*对于直觉逻辑的任何公式A在系统BCKβη中都是可证明的.如果我们能证明“如果A^*在系统BCKβη中可证明的话A在直觉逻辑中是可证明的”，则表明系统BCKβη能够逻辑地模拟直觉逻辑.但相反的情况现在仍然是开放的。用两种方法中的一种进行翻译很简单。另一种方法的翻译相当复杂，但我认为相反的方法会被证明更容易…比前者更多。关于后者，相反的问题是一个重要的未决问题。Komori提出了一个系统，名为Lambda-Rho-Calus。类型赋值系统TA_lambda给出了蕴涵直觉逻辑的自然演绎，而类型赋值系统TA_lambda-Rho给出了经典蕴涵逻辑的自然演绎。此外，对于任何经典蕴涵定理A，都存在A在TA_lambda-Rho中具有子公式性质的证明。证明了TA_lambda-Rho的强正规化定理。在证明中使用了一个新的想法。这一思想也可用于证明其他系统的强正规化定理。鹿岛亮为经典蕴涵逻辑提出了自然演绎体系。他的制度有三条规则，即排除蕴涵规则、引入蕴涵规则和案例规则。笔者注意到，该蕴涵的引入源于案例化规则和弱化。因此，我们从鹿岛系统中用弱化代替蕴涵的引入，得到了系统TA_u。然后我们就发现了拉姆达-罗-微积分。较少

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