On the Compatibility of Constructive Predicative Mathematics with Weyl's Classical Predicativity
Michele Contente, Maria Emilia Maietti
TL;DR
Problem: Reconciling Bishop-style constructive mathematics with Weyl's classical predicativity is nontrivial due to predicative constraints on sets and quantification over functional relations. Approach: The paper analyzes how HA^ω with internal unique choice plus classical logic yields impredicative second-order comprehension, and argues for a constrained alternative in the Minimalist Foundation (MF) with a point-free, lambda-term-based notion of function. Contributions: It details incompatibility for CZF, MLTT, and HoTT, shows how MF restricts exponentiation to λ-functions while avoiding iRC!, and discusses point-free topology within MF as a route to predicative analysis; MF's real numbers are not sets, aligning with Weyl. Significance: MF could provide a natural bridge between Bishop's constructivism and Weyl's predicativity, enabling predicative analysis via point-free methods if such reformulations prove viable.
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ö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.