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

TL;DR

This paper explores the incompatibility between constructive predicative foundations and Weyl's classical predicative analysis, proposing the Minimalist Foundation as a potential compatible framework through point-free topology.

Contribution

It identifies the source of incompatibility in the ability to define sets via quantification over functional relations and suggests restrictions in exponentiation to reconcile the frameworks.

Findings

Incompatibility arises from defining sets by quantifying over functional relations.

Restricting exponentiation to lambda-term functions can bridge the gap.

Minimalist Foundation offers a promising approach for point-free constructive analysis.

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.