η-conversions of IPC implemented in atomic F.

Authors :: FERREIRA, GILDA
Source :: Logic Journal of the IGPL; Apr2017, Vol. 25 Issue 2, p115-130, 16p
Publication Year :: 2017
Abstract: It is known that the β-conversions of the full intuitionistic propositional calculus (IPC) translate into βη-conversions of the atomic polymorphic calculus F<subscript>at</subscript> . Since F<subscript>at</subscript> 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 (the atomic polymorphic calculus F∧<subscript>at</subscript> ). In fact, from the strong normalization of F∧<subscript>at</subscript> we can derive the strong normalization of the full intuitionistic propositional calculus considering all the standard (β and η) conversions. [ABSTRACT FROM AUTHOR]