Title: Polymorphism and the obstinate circularity of second order logic: a victims' tale,
Abstract: The investigations on higher-order type theories and on the related notion of
parametric polymorphism constitute the technical counterpart of the old
foundational problem of the circularity (or impredicativity) of second and
higher order logic. However, the epistemological significance of such
investigations, and of their often non trivial results, has not received much
attention in the contemporary foundational debate. The results recalled in this
paper suggest that the question of the circularity of second order logic cannot
be reduced to the simple assessment of a vicious circle. Through a comparison
between the faulty consistency arguments given by Frege and Martin-Löf,
respectively for the logical system of the Grundgesetze (shown inconsistent by
Russell's paradox) and for the intuitionistic type theory with a type of all
types (shown inconsistent by Girard's paradox), and the normalization argument
for second order type theory (or System F), we indicate a bunch of subtle
mathematical problems and logical concepts hidden behind the hazardous idea of
impredicative quantification, constituting a vast (and largely unexplored)
domain for foundational research.