权益分类	功能权益	普通用户	{{item.name}}会员
{{category.name}}	{{benefitItem.name}}

Regeneration of Church's Lambda calculus on BCK logic

Church 的 Lambda 演算在 BCK 逻辑上的再生

基本信息

批准号：
15540107
负责人：
KOMORI Yuichi
金额：
$ 2.24万
依托单位：
Chiba University
依托单位国家：
日本
项目类别：
Grant-in-Aid for Scientific Research (C)
财政年份：
2003
资助国家：
日本
起止时间：
2003 至 2006
项目状态：
已结题

来源：
https://kaken.nii.ac.jp/en/grant/KAKENHI-PROJECT-15540107/
关键词：
Lambda Calculus BCK Logic Church Classical Logic Curry-Howard isomorphism Intuitionistic Logic Russel's Paradox Illative Combinatory Logic 数理論理学 P=NP問題極小論理式部分構造論理

项目摘要

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

1.为了用BCK β η系统重新评价Church的Lambda演算，我们必须证明BCK β η系统在逻辑上可以模拟经典逻辑。由于直觉逻辑可以模拟经典逻辑，我们证明系统BCK β η可以在逻辑上模拟直觉逻辑就足够了。Komori提出了两种模拟直觉逻辑的方法，并在这两种方法上证明了：存在一个变换^*，使得A^* 是系统BCK β η的公式，且对于直觉逻辑的任何公式A，A^* 在系统BCK β η中是可证明的，如果我们能证明“如果A^* 在系统BCK β η中是可证明的，则A在直觉逻辑中是可证明的”，则系统BCK β η能在逻辑上模拟直觉逻辑。但现在，反向仍然开放。两种方法中的一种翻译很简单。另一种方法的翻译是相当复杂的，但我认为反过来会被证明是容易的 ...更多信息而不是前者。关于后者，反过来是一个重要的开放问题。小森提出了一个系统，名为“Rhoda-rho-calculus”。类型赋值系统TA_lambda为蕴涵直觉主义逻辑提供了一个自然的演绎，而类型赋值系统TA_Aida-rho为经典蕴涵逻辑提供了一个自然的演绎。此外，对于任何经典蕴涵定理A，都存在A在TA_A_rhoda-rho中具有子公式性质的证明。我们证明了TA_α-rho的强正规化定理。在证明中采用了一种新的思想。这一思想可用于证明其它系统的强正规化定理。鹿岛亮为经典蕴涵逻辑提出了一个自然演绎系统。他的体系有三个规则，即隐含排除规则、隐含引入规则和格规则。笔者注意到，默示规则的引入是由判例规则的引入和对默示规则的弱化而产生的。因此我们从鹿岛的系统中用弱化代替蕴涵的引入得到了TA_mu系统。然后我们发现了Renda-rho-calculus。少