On the Compatibility of Constructive Predicative Mathematics with Weyl's Classical Predicativity

Abstract

It is well known that most constructive and predicative foundations aiming to develop Bishop's constructive analysis are incompatible with a classical predicative development of analysis as put forward by Weyl in his $\textit{Das Kontinuum}$. Here, we show how this incompatibility arises from the possibility to define sets by quantifying over (the exponentiation of) functional relations. Such a possibility is present in most constructive foundations but it is not allowed in modern reformulations of Weyl's logical system. In particular, we show how in Aczel's Constructive Set Theory, Martin-L\"of's type theory and Homotopy Type Theory, the incompatibility with classical predicativity \`a la Weyl reduces to the fact of being able to interpret Heyting arithmetic in all finite types with the addition of the internal rule of number-theoretic unique choice, identifying functional relations over natural numbers with a primitive notion of function defined as $\lambda$-terms of type theory. Then, we argue that a possible way out is offered by constructive foundations, such as the Minimalist Foundation, where exponentiation is limited to functions defined as $\lambda$-terms of (dependent) type theory. The price to pay is to renounce number-theoretic choice principles, including the rule of unique choice, typical of most foundations formalizing Bishop's constructive mathematics. This restriction calls for a point-free constructive development of topology as advocated by P. Martin-L\"of and G. Sambin with the introduction of Formal Topology. We then conclude that the Minimalist Foundation promises to be a natural crossroads between Bishop's constructivism and Weyl's classical predicativity provided that a point-free constructive reformulation of analysis is viable.