η-conversions of IPC implemented in atomic F
Gilda Ferreira · Logic Journal of IGPL · 2016
It is known that the |$\beta$|-conversions of the full intuitionistic propositional calculus (|$\mathbf{IPC}$|) translate into |$\beta\eta$|-conversions of the atomic polymorphic calculus |${\mathbf{F}}_{\mathbf{at}}$|. Since |${\mathbf{F}}_{\mathbf{at}}$| enjoys the property of strong normalization for |$\beta\eta$|-conversions, an alternative proof of strong normalization for |$\mathbf{IPC}$| considering |$\beta$|-conversions can be derived. In the present article, we improve the previous result by analysing the translation of the |$\eta$|-conversions of the latter calculus into a technical variant of the former system (the atomic polymorphic calculus |${\mathbf{F}}_{\mathbf{at}}^{\wedge}$|). In fact, from the strong normalization of |${\mathbf{F}}_{\mathbf{at}}^{\wedge}$| we can derive the strong normalization of the full intuitionistic propositional calculus considering all the standard (|$\beta$| and |$\eta$|) conversions.