Polymorphism and the obstinate circularity of second order logic: a victims' tale

TL;DR

This paper explores the complex foundational issues of second order logic's circularity, comparing historical and modern arguments to reveal subtle mathematical and logical problems that challenge simple assessments of impredicativity.

Contribution

It offers a nuanced analysis of the circularity problem in second order logic, highlighting overlooked mathematical and logical complexities and comparing key foundational arguments.

Findings

Circularity in second order logic is more complex than a simple vicious circle.

Historical and modern consistency arguments reveal subtle foundational issues.

Impredicative quantification involves deep, largely unexplored logical problems.

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\"of, 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.