Atomic polymorphism

It has been known for six years that the restriction of Girard’s polymorphic system F to atomic universal instantiations interprets the full fragment of the intuitionistic propositional calculus. We firstly observe that Tait’s method of “convertibility” applies quite naturally to the proof of strong normalization of the restricted Girard system. We then show that each β-reduction step of the full intuitionistic propositional calculus translates into one or more βη-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 η-conversions.Both authors acknowledge support of FCT-Fundação para a Ciência e a Tecnologia [project PTDC/MAT/104716/2008] and Centro de Matematica e Aplicações Fundamentais (Universidade de Lisboa). The second author is also grateful to FCT [grant SFRH/BPD/34527/2006] and Nucleo de Investigação em Matemática (Universidade Lusófona).