To be or not to be constructive, that is not the question

Sam Sanders

【摘要】在20世纪早期，L.E.J.布劳威尔（L.E.J.Brouwer）开创了一种新的数学哲学，称为直觉主义。直觉主义在许多方面都是革命性的，但在数学上却因挑战希尔伯特的形式主义数学哲学和反对主流数学中使用的“经典”逻辑而引人注目。直觉主义产生了直觉逻辑，并由此产生了布鲁沃-海廷克尔莫戈罗夫(brouyer - heyting - kolmogorov)对“存在x”的直观解释，即“给出了计算x的算法”。许多建构数学学派都是受布劳威尔的直觉是，从而基于直觉逻辑的启发而发展起来的，但对构成算法的东西有不同的解释。本文讨论了构造性数学与非构造性数学的二分法，或者说没有这样一个“被排斥的中间情况”。特别地，我们挑战“二元”观点，即数学要么是构造性的，要么不是。为此，我们确定了古典数学的一部分，即古典非标准分析，并指出它存在于构造与非构造之间的模糊地带。直观地说，非标准分析的典型谓词“x是标准的”可以解释为“x是可计算的”，从而产生了直接从经典非标准分析中获得的可计算(有时是构造性的)数学。我们的研究结果将奥斯瓦尔德（Osswald）“经典非标准分析是局部构造性的”这一长期以来的猜想正式化。最后，Brouwer的逻辑依赖于数学的论点为我们的结果提供了另一种解释。

【Abstract】In the early twentieth century, L.E.J. Brouwer pioneered a new philosophy of mathematics, called intuitionism. Intuitionism was revolutionary in many respects but stands out – mathematically speaking – for its challenge of Hilbert’s formalist philosophy of mathematics and rejection of the law of excluded middle from the ‘classical’ logic used in mainstream mathematics. Out of intuitionism grew intuitionistic logic and the associated Brouwer–Heyting–Kolmogorov interpretation by which ‘there exists x’ intuitively means ‘an algorithm to compute x is given’. A number of schools of constructive mathematics were developed, inspired by Brouwer’s intuition is mand invariably based on intuition is ticlogic, but with varying interpretations of what constitutes an algorithm. This paper deals with the dichotomy between constructive and non-constructive mathematics, or rather the absence of such an ‘excluded middle’. In particular, we challenge the ‘binary’ view that mathematics is either constructive or not. To this end, we identify a part of classical mathematics, namely classical Nonstandard Analysis, and show it inhabits the twilightzone between the constructive and non-constructive. Intuitively, the predicate ‘x is standard’ typical of Nonstandard Analysis can be interpreted as ‘x is computable’, giving rise to computable (and sometimes constructive) mathematics obtained directly from classical Nonstandard Analysis. Our results formalise Osswald’s longstanding conjecture that classical Nonstandard Analysis is locally constructive. Finally, an alternative explanation of our results is provided by Brouwer’s thesis that logic depend supon mathematics.

Redirecting​doi.orgMatches for: MR=3739620​mathscinet.ams.org