構成的証明：明示的な構成によって存在を示す数学的証明

手法と特徴

構成的証明の典型的な特徴には、直接的な構成、アルゴリズムによる記述、明示的な評価範囲がある。代表的な構成的方法として、次のものが挙げられる。

• 明示的な例または公式を提示すること。
• 有限時間内に必要な対象を得るアルゴリズム、または段階的な手続きを与えること。
• 構成的帰納法を用いて、より大きい対象や精度の高い対象を構築すること。
• 近似手続きを実用的にする有効な評価や誤差範囲を示すこと。

構成的証明では、排中律や、古典的証明で用いられる非構成的な存在原理への依存を避けることが多い。

歴史と哲学的背景

構成的方法を求める考え方は、数学における存在をより厳格に解釈すべきだと主張した直観主義者や、ほかの構成主義的学派の研究に哲学的な根源をもつ。こうした見解に関係する人物には、20世紀初頭の直観主義者や、後の構成的解析の支持者が含まれる。構成的アプローチは、証明がアルゴリズムに対応する計算可能性理論や型理論の発展にも影響を与えた。

例と応用

構成的証明は、数学と計算機科学の広い分野で応用される。数論や代数学では、構成的証明によって明示的な解、またはそれを見つけるアルゴリズムが得られる。解析学や数値数学では、構成的な存在証明はしばしば収束する反復法の形をとる。論理学と言語プログラミングでは、カリー＝ハワード対応が構成的証明を実行可能なプログラムと結び付け、証明からコードを抽出することを可能にする。これに対し、古典的証明の一部は間接的に存在を示す。よく知られた非構成的な例では、場合分けを用いて、有理数乗が有理数となる二つの無理数の存在を結論するが、両方を直ちに特定するわけではない。

区別と注目すべき点

構成的証明と非構成的証明は、相補的な道具である。古典数学は、論理的に妥当であれば通常、非構成的な存在証明を受け入れる一方、構成的数学は明示的な構成を要求する。最初は非構成的に証明された多くの定理に、後に構成的証明が与えられており、その際には追加のアルゴリズム的洞察が得られることも多い。証明の様式と方法論については、一般的な証明の方法に関する議論も参照されたい。

関連項目：構成的数学、証明のアルゴリズム的内容、構成的証明からの証明抽出。