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

Source abstract

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 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öf’s type theory and Homotopy type theory, the incompatibility with classical predicativity à 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 λ-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 λ-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öf 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.