構造性證明

構造性證明（英語：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是有理數。考慮數字$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釋義
• 直覺類型論
• 經典邏輯
• 中間邏輯
• 線性邏輯
• 柯里-霍華德同構
• 可計算性邏輯
• 博弈語義