构造性证明

构造性证明（英语：Constructive proof）是数学证明方法的一种，通过直接或间接构造出具有命题所要求的性质的实例来完成证明。与构造性证明相对的概念是非构造性证明。后者只证明满足命题要求的物体存在，而不提供具体的实例或构造这样的实例的方法。

构造性证明也可以指数学构成主义中被认可的一种更强的证明。数学构成主义是数学哲学的一支，它认为要证明一个对象的存在，必须将其构造出来。因此，他们拒绝使用如排中律，无穷公理和选择公理这样的公理。同时也有一些用语和以往不同，例如或的语意会比基础数学中的更强。

数学构成主义拒绝使用反证法，然而爆炸原理在一些数学构成主义的变体中是被接受的，包括直觉主义。

历史

直到十九世纪结束，所有的数学证明使用的还是构造性证明。第一个使用非构造性方法的是格奥尔格·康托尔的无限集合理论，以及对实数的形式化定义.

初次使用非构造性证明解决之前的问题的例子，被认为是希尔伯特零点定理和希尔伯特基定理。

例子

非构造性证明

考虑对质数有无穷个的证明。欧几里得的证明本身是构造性的，不过有一种常用的方法来简化欧几里得的证明，它先假设质数的数量是有限的，那么必然会有一个最大的质数，将它记为n。然后考虑n! + 1（n阶乘加1），这个数字要么本身是质数，要么是合数且存在一个大于n的质因子，因为小于等于n的质数除它都余1。通过得出和命题的假设矛盾的结论，我们并不需要指出一个确定的质数，就可以证明存在一个大于n的质数。

再考虑证明这个命题：“存在无理数$a$和$b$，使$a^{b}$是有理数”。这个证明可以被构造性地证明，也可以被非构造性地证明，我们将对比两种证明方式。

以下证明是1953年由Dov Jarden提出的，最晚从1970年开始被用作非构造性证明的经典例子：

CURIOSA
339. 对一个无理数的无理数次方可以是有理数的简单证明
${\sqrt {2}}^{\sqrt {2}}$要么是有理数，要么是无理数。如果它是有理数，那么我们的命题得证。如果它是无理数，$({\sqrt {2}}^{\sqrt {2}})^{\sqrt {2}}=2$，我们的命题得证。
     Dov Jarden     Jerusalem

更具体地：

• 我们在先前已经知道${\sqrt {2}}$是无理数，2是有理数（请参照2的算术平方根的无理数证明)。考虑数字$q={\sqrt {2}}^{\sqrt {2}}$，它要么是有理数，要么是无理数。
• 如果$q$是有理数，那么原命题成立，此时$a$和$b$都是${\sqrt {2}}$。
• 如果$q$是无理数，那么原命题也成立，此时$a$为${\sqrt {2}}^{\sqrt {2}}$而$b$为${\sqrt {2}}$，由于：

$\left({\sqrt {2}}^{\sqrt {2}}\right)^{\sqrt {2}}={\sqrt {2}}^{({\sqrt {2}}\cdot {\sqrt {2}})}={\sqrt {2}}^{2}=2$。

这个证明是非构造性的，因为它依赖了这样的陈述：“q要么是有理数，要么是无理数”，这是排中律的一个应用，而构造性证明里排中律是无效的。这个非构造性证明并没有构造一个实际的a和b，它只是考察了由排中律给出的两种可能性。我们并不知道这两种可能性哪个是真实的，${\sqrt {2}}^{\sqrt {2}}$究竟是不是无理数。

实际上根据格尔丰德-施奈德定理，我们可以得知${\sqrt {2}}^{\sqrt {2}}$是一个无理数，但是它和这个非构造性证明的正确性无关。

构造性证明

对上面的例子，构造性证明会给出一个实际的例子，如：

$a={\sqrt {2}}\,,\quad b=\log _{2}9\,,\quad a^{b}=3\,.$

已知2的算术平方根是无理数，而3是有理数。$\log _{2}9$同样是无理数，因为如果他可以写作$m \over n$，那么根据对数运算法则，9ⁿ会等于2^m，然而前者是奇数，后者是偶数（奇数的整数次方还是奇数，偶数的整数次方还是偶数）。

参见

• 直觉主义
• BHK释义
• 直觉类型论
• 经典逻辑
• 中间逻辑
• 线性逻辑
• 柯里-霍华德同构
• 可计算性逻辑
• 博弈语义