η-conversions of IPC implemented in atomic F

Ferreira, Gilda

http://hdl.handle.net/10400.2/7091

Use this identifier to reference this record.

Name:	Description:	Size:	Format:
etaconversions.pdf		122.51 KB	Adobe PDF	Download

Send Feedback

Authors

Ferreira, Gilda

Abstract(s)

It 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.

Keywords

Mathematical logic Eta-conversions Predicative polymorphism Intuitionistic propositional calculus Strong normalization Natural deduction

URI

http://hdl.handle.net/10400.2/7091

Citation

Gilda 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–130