Ferreira, Gilda2018-02-092018-05-312017Gilda Ferreira - η-conversions of IPC implemented in atomic F. "Logic Journal of the IGPL" [Em linha]. ISSN 1367-0751 (Print) 1368-9894 (Online). Vol. 25, nº 2 (2017), p. 115–1301367-0751 (Print)http://hdl.handle.net/10400.2/7091It is known that the β-conversions of the full intuitionistic propositional calculus (IPC) 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 (the atomic polymorphic calculus Fat^∧_at). In fact, from the strong normalization of Fat^∧_at we can derive the strong normalization of the full intuitionistic propositional calculus considering all the standard (β and η) conversions.engMathematical logicEta-conversionsPredicative polymorphismIntuitionistic propositional calculusStrong normalizationNatural deductionjournal article10.1093/jigpal/jzw035