关于构造预测数学与魏尔经典预测性的兼容性
On the Compatibility of Constructive Predicative Mathematics with Weyl's Classical Predicativity
AI总结：
本文探讨了构造预测数学与魏尔经典预测性的兼容性问题，指出通过限制指数运算和放弃数论选择原理，极简基础可能成为两者之间的桥梁。
摘要：
众所周知，大多数旨在发展比什的构造分析的构造和预测基础是与魏尔在《连续体》中提出的经典预测分析发展不兼容的。在这里，我们展示这种不兼容性是如何由于能够通过量化（函数关系的指数）来定义集合的可能性而产生的。这种可能性存在于大多数构造基础中，但在现代重新表述的魏尔逻辑系统中是不允许的。特别是，我们展示了在阿克塞尔的构造集合论、马丁-洛夫的类型论和同调类型论中，与经典预测性à la Weyl的不兼容性归结于能够将霍伊廷算术解释为所有有限类型（加上内部的数论唯一选择规则）的事实。然后，我们论证一种可能的出路是通过构造基础，如极简基础，其中指数被限制为由（依赖）类型论中的λ项定义的函数。代价是放弃数论选择原理，包括典型的大多数形式化比什构造数学的基础的唯一选择规则。这种限制要求进行无点的构造拓扑学发展，如P.马丁-洛夫和G.萨宾提出的正式拓扑学。我们然后得出结论，极简基础有望成为比什构造主义和魏尔经典预测性之间的自然交汇点，前提是可行的无点构造分析的重新表述。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
