查看“︁构造性证明”︁的源代码

'''构造性证明'''（{{lang-en|Constructive proof}}）是[[数学证明]]方法的一种，通过直接或间接构造出具有命题所要求的性质的实例来完成证明。与构造性证明相对的概念是[[非构造性证明]]{{notetag|有时也称为存在性证明或[[存在性定理|纯粹存在性证明]]}}。后者只证明满足命题要求的物体存在，而不提供具体的实例或构造这样的实例的方法。

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

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

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

初次使用非构造性证明解决之前的问题的例子，被认为是[[希尔伯特零点定理]]和[[希尔伯特基定理]]。{{notetag|此段可参见英文维基}}

==例子==

===非构造性证明===

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

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

以下证明是1953年由Dov Jarden提出的，最晚从1970年开始被用作非构造性证明的经典例子：<ref>[[J. Roger Hindley]], "The Root-2 Proof as an Example of Non-constructivity", unpublished paper, September 2014, [http://www.users.waitrose.com/~hindley/Root2Proof2014.pdf full text] {{webarchive|url=https://web.archive.org/web/20141023060917/http://www.users.waitrose.com/~hindley/Root2Proof2014.pdf|date=2014-10-23}}</ref><ref>Dov Jarden, "A simple proof that a power of an irrational number to an irrational exponent may be rational", ''Curiosa'' No. 339 in ''[[Scripta Mathematica]]'' '''19''':229 (1953)</ref>

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

更具体地：

*我们在先前已经知道<math>\sqrt{2}</math>[[2的算术平方根|是无理数]]，2是有理数（請參照[[2的算術平方根]]的無理數證明)。考虑数字<math>q = \sqrt{2}^{\sqrt2}</math>，它要么是有理数，要么是无理数。
*如果<math>q</math>是有理数，那么原命题成立，此时<math>a</math>和<math>b</math>都是<math>\sqrt{2}</math>。
*如果<math>q</math>是无理数，那么原命题也成立，此时<math>a</math>为<math>\sqrt{2}^{\sqrt2}</math>而<math>b</math>为<math>\sqrt{2}</math>，由于：
:<math>\left (\sqrt{2}^{\sqrt2}\right )^{\sqrt2} = \sqrt{2}^{(\sqrt{2} \cdot \sqrt{2})} = \sqrt{2}^2 = 2</math>。

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

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

===构造性证明===

对上面的例子，''构造性''证明会给出一个实际的例子，如：
:<math>a = \sqrt{2}\, , \quad b = \log_2 9\, , \quad a^b = 3\, .</math>
已知[[2的算术平方根]]是无理数，而3是有理数。<math>\log_2 9</math>同样是无理数，因为如果他可以写作<math>m \over n</math>，那么根据[[对数]]运算法则，9<sup>''n''</sup>会等于2<sup>''m''</sup>，然而前者是奇数，后者是偶数（奇数的整数次方还是奇数，偶数的整数次方还是偶数）。

==注释==
{{notefoot}}
==参见==
* [[直觉主义]]
* [[BHK释义]]
* [[直觉类型论]]
* [[经典逻辑]]
* [[中间逻辑]]
* [[线性逻辑]]
* [[柯里-霍华德同构]]
* [[可计算性逻辑]]
* [[博弈语义]]
==参考资料==
{{reflist}}
[[Category:证明]]
[[Category:数学推理]]
[[Category:数理逻辑]]