Back to Search
Start Over
Atomic polymorphism
- Source :
- Journal of Symbolic Logic; March 2013, Vol. 78 Issue: 1 p260-274, 15p
- Publication Year :
- 2013
-
Abstract
- AbstractIt has been known for six years that the restriction of Girard's polymorphic system F to atomicuniversal instantiations interprets the full fragment of the intuitionistic propositional calculus. We firstly observe that Tait's method of “convertibility” applies quite naturally to the proof of strong normalization of the restricted Girard system. We then show that each ß-reduction step of the full intuitionistic propositional calculus translates into one or more ß?-reduction steps in the restricted Girard system. As a consequence, we obtain a novel and perspicuous proof of the strong normalization property for the full intuitionistic propositional calculus. It is noticed that this novel proof bestows a crucial role to ?-conversions.
Details
- Language :
- English
- ISSN :
- 00224812
- Volume :
- 78
- Issue :
- 1
- Database :
- Supplemental Index
- Journal :
- Journal of Symbolic Logic
- Publication Type :
- Periodical
- Accession number :
- ejs40656250
- Full Text :
- https://doi.org/10.2178/jsl.7801180