科研之友
微信
新浪微博
Facebook
分享链接
摘要
It has been known for six years that the restriction of Girard%26apos;s polymorphic system F to atomic universal instantiations interprets the full fragment of the intuitionistic propositional calculus. We firstly observe that Tait%26apos;s method of %26quot;convertibility%26quot; applies quite naturally to the proof of strong normalization of the restricted Girard system. We then show that each beta-reduction step of the full intuitionistic propositional calculus translates into one or more beta eta-reduction steps in the restricted Girard system. As a consequence, we obtain a novel and perspicuous proof of the strong normalization property for the full intuitionistic propositional calculus. It is noticed that this novel proof bestows a crucial role to eta-conversions.
- 出版日期2013-3
