Η-conversions of IPC implemented in atomic F. (30th June 2016)

• Record Type: Journal Article
• Authors: Ferreira, Gilda
• Is Part Of: Logic journal of the IGPL. Volume 25:Number 2(2017:Apr.)
• Page Start: 115
• Page End: 130
• Publication Date: 2016-06-30
• Subjects: η-conversions -- predicative polymorphism -- intuitionistic propositional calculus -- strong normalization -- natural deduction; Logic, Symbolic and mathematical -- Periodicals; 511.3
• DOI: 10.1093/jigpal/jzw035
• Languages: English
• ISSNs: 1367-0751

Abstract

Abstract: 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.