Predicativity and parametric polymorphism of Brouwerian implication
History and Overview
2018-05-08 v2 Logic
Abstract
A common objection to the definition of intuitionistic implication in the Proof Interpretation is that it is impredicative. I discuss the history of that objection, argue that in Brouwer's writings predicativity of implication is ensured through parametric polymorphism of functions on species, and compare this construal with the alternative approaches to predicative implication of Goodman, Dummett, Prawitz, and Martin-L\"of.
Cite
@article{arxiv.1710.07704,
title = {Predicativity and parametric polymorphism of Brouwerian implication},
author = {Mark van Atten},
journal= {arXiv preprint arXiv:1710.07704},
year = {2018}
}
Comments
Added further references (Pistone, Poincar\'e, Tabatabai, Van Atten)