数学构成主义

构造主义者的数学使用构造性逻辑，该逻辑将真实性和证明等同起来。要构造性的证明${\displaystyle P\lor Q}$ ，我们必须证明${\displaystyle P}$ 或${\displaystyle Q}$ ，或两者同时成立。要构造式的证明${\displaystyle \exists _{x\in X}P(x)}$ ，我们必须给出一个特定的${\displaystyle a\in X}$ 和一个${\displaystyle P(a)}$ 的证明。要构造式的证明${\displaystyle \forall _{x\in X}P(x)}$ ，我们必须给出一个算法，它对于每个${\displaystyle a\in X}$ 输出一个${\displaystyle P(a)}$ 的证明。

构造主义同时拒绝采用无穷对象，例如无穷集合和序列。

实分析中的例子

在经典实分析中，实数构造的方法之一是把它作为有理数的柯西列对。这个构造在构造主义数学中不成立，因为序列是无穷的。

作为替换，我们把实数表示为一个算法${\displaystyle f}$ ，它取一个正整数${\displaystyle n}$ 然后输出一对有理数${\displaystyle (f_{\ell }(n),f_{r}(n))}$ 使得

${\displaystyle m\leq n\implies f_{\ell }(m)\leq f_{\ell }(n)}$ 

${\displaystyle m\leq n\implies f_{r}(n)\leq f_{r}(m)}$ 

${\displaystyle 0\leq f_{r}(n)-f_{\ell }(n)\leq {1 \over n}}$ 

使得当${\displaystyle n}$ 增大，区间${\displaystyle [f_{\ell }(n),f_{r}(n)]}$ 变小，而前${\displaystyle n}$ 个这种区间的交不空。我们使用${\displaystyle f}$ 来计算它所表示的实数的任何精度的有理数近似。

在这个定义下，实数${\displaystyle {\sqrt {2}}}$ 可以用一个算法表示，它对于每个${\displaystyle 0\leq i\leq n}$ 计算出最大的整数${\displaystyle a_{i}}$ 使得${\displaystyle a_{i}^{2}\leq 2i^{2}}$ 然后输出${\displaystyle \left(\mathrm {max} \left\{{a_{i} \over i}\right\},\mathrm {min} \left\{{a_{i}+1 \over i}\right\}\right)}$ 。

这个定义和采用柯西列的经典定义相关，除了要求序列是构造式的：也就是说，我们有个计算第${\displaystyle n}$ 个序列中的元素的算法，所以有一个计算任意精确的对${\displaystyle {\sqrt {2}}}$ 的有理数近似的算法。

注意构造性要求使得上述定义和通常非构造主义的实数定义不相容：因为每个算法${\displaystyle \xi }$ 必须是一个有限指令集${\displaystyle \Sigma }$ 上的有限序列，存在一个双射函数${\displaystyle f:\Sigma ^{*}\rightarrow \mathbb {N} }$ 。所以所有算法的集合和所有自然数的集合有同样的基数。当使用一个非构造式的定义时，康托对角线论证证明实数比自然数有更高的基数。

传统上，数学家对于数学构造主义曾经持怀疑态度，如果不是完全反对的话，很大程度上这是因为它对构造分析的限制．

这些观点希尔伯特在1928年曾有强烈表示．他在《数学基础》（Die Grundlagen der Mathematik）写道：“把排中律从数学家那里拿走，就像把望远镜从天文学家那里拿走，或是从拳击手那里把拳头拿走一样”[1] （排中律在构造性逻辑中不成立）。

Errett Bishop（英语：Errett Bishop），在他1967年的著作《构造性分析学基础》（Foundations of Constructive Analysis）中，作了很多驱散这种恐怖，他的办法是用构造性的框架中发展出传统的分析学的大部分．

但是，不是所有数学家都认为Bishop非常成功，因为的他的书必须比经典分析教科书更复杂．

无论如何，多数数学家不认为应该把自己限制到构造主义方式，甚至当可以这样做时。^[1]

• 克罗内克（Leopold Kronecker）
• L.E.J. Brouwer
• 保罗·洛伦岑
• Errett Bishop

• 构造性逻辑
• 构造主义类型理论
• 构造主义分析
• 可计算性逻辑

• 数学直觉主义
• 直觉主义类型理论
• 有限主义
• 博弈语义学
• 构造性证明

• 可计算逻辑主页