Abstract

It is known that the β-conversions of the full intuitionistic propositional calculus translate into βη-conversions of the atomic polymorphic calculus Fat. Since Fat enjoys the property of strong normalization for βη-conversions, an alternative proof of strong normalization for IPC considering β-conversions can be derived. In the present article, we improve the previous result by analysing the translation of the η-conversions of the latter calculus into a technical variant of the former system. In fact, from the strong normalization of F∧at we can derive the strong normalization of the full intuitionistic propositional calculus considering all the standard conversions.