構成主義 (数学)

数学の哲学において、構成主義（こうせいしゅぎ、英: constructivism）とは、「ある数学的対象が存在することを証明するためには、それを実際に見つけたり構成したりしなければならない」という考えのことである。標準的な数学においてはそうではなく、具体的に見つけることなしに背理法によって存在を示す、すなわち存在しないことを仮定して矛盾を導くことがよくある。この背理法というものは構成的に見ると十分ではない。構成的な見地は、古典的な解釈をもって中途半端なままである、存在記号の意味を確かめることを含む。

構成主義には多くの形があり、以下のようなものが含まれる^[1]。

• ブラウワーによって創始された直観主義のプログラム
• ヒルベルトならびにベルナイスの有限主義（英語版）
• Shamin（英語版）ならびにMarkov（英語版）の構成的で再帰的な数学
• 構成的解析学（英語版）であるBishop（英語版）のプログラム
• CZF（英語版）やトポス論の研究のような構成的集合論（英語版）の研究

構成主義はしばしば直観主義と同一視されるが、直観主義は構成主義者のプログラムのひとつでしかない。直感主義では数学者個人の直観のなかに数学の基礎が置かれることを支持し、それによって数学は本質的に主観的活動となる^[2]。他の形の構成主義は、こうした直観的見地に基づくものではなく、数学に対する客観的見地と両立できるものである。

多くの構成主義的数学者が、本質的には排中律を含まない古典論理である、直観主義論理を用いている。排中律は、任意の命題に対して、その命題が真であるかもしくはその命題の否定が真であることを主張する。直観主義論理では、排中律を全否定するのではなく、排中律の特殊なケースを証明可能とする。これは単に、一般法則（排中律）を公理と仮定するわけではないということである。直観主義論理でも、（矛盾する複数の言明が同時に真にならないことを主張する）無矛盾律は有効である。

例えばハイティング算術（英語版）では、量化子を含まない任意の命題 p に対して、${\displaystyle \forall x,y,z,\ldots \in \mathbb {N} :p\vee \neg p}$ は定理であることを証明できる（ここで x, y, z ... は命題 p における自由変項である）。この意味で、古典論理においては有限に制限された命題をやはり真か偽であるとみなせるが、この二値性（英語版）を無限の集まりに言及する命題には拡張できない。

実際、直観主義者の学校の創始者であるブラウアーは、排中律を有限の認識から抽象的なものと捉え、そして認識論的に正当化（英語版）することなしに無限に適用した。例えばゴールドバッハの予想は、（2より大きい）どの偶数も2つの素数の和となることを主張する。特定の偶数に対して2つの素数の和であるか否かを確かめることは可能であるので（たとえば力まかせ探索で）、（2より大きい）任意の偶数は、2つの素数の和であるかそうでないかである。そしてこれまでのところ、各偶数は実際に2つの素数であることが上記のように確かめられている。

しかし、全ての偶数がゴールドバッハの予想を満たすことの証明も、ゴールドバッハの予想を満たさない偶数があることの証明も存在しない。それどころか、ゴールドバッハの予想の証明または反証が存在するかどうかすら不明である（ゴールドバッハの予想は従来型のZF集合論では決定不能かもしれない）。したがってブラウアーにとっては、「ゴールドバッハの予想が真である、あるいは偽である」という主張は正当化されない。また、この予想がいつか解かれたとしても、この主張を似た未解決問題に適用すれば同じ議論となる。ブラウアーにとっては、排中律はどの数学的問題にも解があると仮定するのと同じである。

公理として排中律を排除した場合、残る論理体系には古典論理が持たない存在性質（英語版）を持つ：${\displaystyle \exists _{x\in X}P(x)}$ が構成的に証明されているならばいつでも、実際に ${\displaystyle P(a)}$ は（少なくとも）1つの特定の ${\displaystyle a\in X}$ に対して構成的に証明される（この a のことをしばしば証拠(witness)と呼ぶ）。このように、数学的対象の存在の証明はその構成と紐付いている。

古典的な実解析において、実数を定義（英語版）する方法の一つは有理数のコーシー列の同値類である。

構成的数学において、実数を構成する方法の一つは、正の整数 n をとり有理数 f(n) を出力する関数 f と、n が大きくなるにつれて ƒ(n) の値は互いに近づくように、正の整数 n をとり正の整数 g(n) を出力する以下を満たす関数 g を併用することである。

${\displaystyle \forall n\ \forall i,j\geq g(n)\quad |f(i)-f(j)|\leq {1 \over n}}$

ƒ と g を併用すると、ƒ と g が表現する実数を任意精度の有理数近似として計算できる。

この定義のもとでは、e の単純な表現は以下のようになる：

${\displaystyle f(n)=\sum _{i=0}^{n}{1 \over i!},\quad g(n)=n.}$

この定義はコーシー列を用いた古典的な定義に、構成的な工夫を除いて対応する：古典的なコーシー列では、ある要素以降は列の各要素の距離が与えられた距離よりも小さくなるような要素が存在する、ということを要請する。構成的なバージョンでは、与えられた距離よりも実際に互いの距離が小さくなる要素を特定できることを要請する（このように特定された要素の位置は、しばしば収束係数（英語版）と呼ばれる）。事実、数学的言明

${\displaystyle \forall n:\exists m:\forall i,j\geq m:|f(i)-f(j)|\leq {1 \over n}}$

の標準的な構成的解釈（英語版）（BHK解釈）は、正確に収束係数を計算する関数が存在することである。このように、実数の2つの定義の違いは「すべての...に対して、...が存在する」という言明の解釈の違いにあると考えられる。

すると、上記の f と g のように、可算集合から可算集合へのどの関数が実際に構成できるのかという質問が湧き出る。構成主義の異なるバージョンでは、この点で解釈が分かれる。こうした構成は直観主義的視点である自由選択列（英語版）と同程度に広く、またはアルゴリズム（より専門的には計算可能関数）と同程度に狭く、あるいは未特定のまま定義できる。例えば、アルゴリズム的観点で考えた場合、ここで構成した実数は、本質的には古典的に計算可能数と呼ばれるものになるだろう。

上記のアルゴリズム的解釈を採用すると、濃度の古典的な概念と矛盾するように思われる。アルゴリズムに番号付けすることで、計算可能数が古典的に可算であることを示せる。それにもかかわらず、カントールの対角線論法から実数が非可算濃度を持つことがわかる。つまり、実数と計算可能数を同一視すると矛盾が生じる。さらに言えば、対角線論法は完全に構成的であると考えられる。

実際カントールの対角線論法は、自然数から実数への全単射を考えると、実数が関数の値域にないために矛盾が生じるという意味で、構成的に示せる。まず関数 T が自然数から実数への全射であると仮定して、関数 T を構成するアルゴリズムを番号付けする。しかし、アルゴリズムはこの制約を破ったり停止しない（T は部分関数である）可能性があり、各アルゴリズムに対して実数が対応する場合もそうでない場合もありうるため、要求された全単射は満たせない。簡潔に言えば、実数が（それぞれ）実効的に計算可能であるという立場においては、カントールの結果は実数が（全体として）再帰的に枚挙可能でないと解釈される。

それでもなお、T が自然数から実数への全射関数であるため、実数は可算個ほどもないと期待できるかもしれない。また、各自然数は自明に実数と解釈できるため、実数は可算個ほどもある。すなわち、実数はちょうど可算個であると言える。しかし、要求された全単射を構成していないため、こうした理由付けは構成的でない。このような状況で全単射の存在を証明する古典的な定理（カントール・ベルンシュタイン・シュレーダーの定理）は構成的でない。カントール・ベルンシュタイン・シュレーダーの定理は排中律を含意することが最近示されたため、それ故にこの定理の構成的証明は存在しえない^[3]。

構成的数学における選択公理の立ち位置は、構成主義者のプログラムによってアプローチが異なり、複雑な状況である。「構成的」の自明な意味の一つは、数学者が非公式に使う、「選択公理を除いたZF集合論で証明可能」である。しかし、より制限された形式の構成的数学を提案する者は、ZF自体が構成的システムになっていないと主張するかもしれない。

型理論（特に高階型理論）の直観的理論においては、様々な形式の選択公理が許容される。例えば公理 AC₁₁ は以下のように言い換えられる：「実数の集合上の任意の関係 R に対して、各実数 x に対して R(x,y) を満たす実数 y が存在することが証明されれば、実際にすべての実数に対して R(x,F(x)) を満たす関数 F が存在する。」類似した選択原理もすべての有限な型に対して許容される。これらの一見非構成的な原理を採用する動機は、「各実数 x に対して R(x,y) を満たす実数 y が存在する」ことの証明の直観的理解にある。BHK解釈（英語版）によれば、この証明は本質的に求められる関数 F であるとされる。直観主義者が許容する選択原理は排中律を含意しない。

しかし、構成的集合論に対する特定の公理系においては、en:Diaconescu-Goodman-Myhill theorem が示すように、選択公理が（他の公理が存在する状況で）排中律を含意する。構成的集合論には弱形式の選択公理を含むものがあり、たとえば Myhill の集合論における従属選択公理のようなものがある。

古典的な測度論は、ルベーグ測度の古典的な定義では集合の測度や関数の積分を具体的に計算する方法を表現しないため、基本的に非構成的である。実際、関数を「実数を入力して実数を出力する」という規則として考えると、関数の積分を計算するアルゴリズムが存在し得ない。これはどのアルゴリズムも一度に有限個の関数値しか呼び出せず、非自明な精度の積分を計算するには有限個の値では足りないためである。この難問の解決策として、初めて Bishop (1967) が実行した方法は、収束係数に関する情報を含む、(連続率が既知の) 連続関数の点単位の極限として記述された関数のみを考えることである。測度論を構成主義化する利点は、集合が構成的に完全測度であると証明できるならば、その集合内の点を探すアルゴリズムが存在するということである（Bishop (1967)を再度参照）。例えば、このアプローチはどの底でも正規数となる実数を構成するのに使うことができる^[要出典]。

伝統的に、数学的構成主義に対して、敵対的ではないにしても、疑念を抱く数学者も存在する。その主な理由は、構成的解析論に数学的構成主義がもたらす制限によるものである。この見地は1928年、ダフィット・ヒルベルトにより、自身の著書『Grundlagen der Mathematik』の中で以下のように強力に表現された。「数学者から排中律を取り上げることは、いわば天文学者に望遠鏡を禁止するか、ボクサーに拳を禁止するのと同じである。」^[4]

Errett Bishop は、自身の 1967年の著書 Foundations of Constructive Analysis^[5] で、構成主義的な枠組みにおいて、多くの従来的な解析学を改良することによる懸念を払拭するために働きかけた。

ほとんどの数学者が、構成的手法に基づく数学のみが健全であるという構成主義者の論文を採用しないにもかかわらず、構成的手法は特定のイデオロギーに依存しない層の興味を惹きつけ始めている。例えば、解析学の構成的な証明では、構成的手法では古典的手法を使うのより容易に理論の証拠を見つけうるという制約の中でやりくりするというやり方で、証拠の抽出(witness extraction)を保証しうる。構成的数学への応用は、型付きラムダ計算、トポス理論、圏論的論理学（英語版）にも見られ、これらは基礎的な数学や計算機科学の注目すべき主題である。代数学では、トポスやホップ代数といったテーマに対して、その構造は構成的理論であるという内的言語（英語版）(internal language)を支持している。そうした言語内で扱うことは、可能な具体的代数の集合やその準同型について推論するといった手段で外的に扱うよりも、しばしば直観的かつ柔軟である。

物理学者リー・スモーリンは Three Roads to Quantum Gravity の中で以下のように著している：トポス理論は「宇宙論の正しい形式の論理」である（30ページ）、「『直観論理』と呼ばれる、その最初の形式において」（31ページ）、「この種の論理では、観測者が宇宙に関して主張できることは少なくとも3つのグループに分けられる：真と判断できるもの、偽と判断できるもの、そして現時点でその真偽を判断できないものである。」（28ページ）

• レオポルト・クロネッカー（古い構成主義、準直観主義）
• ライツェン・エヒベルトゥス・ヤン・ブラウワー（直観主義の創始者）
• A. A. Markov （ロシアの構成主義の学校の始祖）
• アレン・ハイティング（直観主義論理と直観主義理論の定式化）
• ペール・マルティン＝レーフ（構成的型論理の創始者）
• Errett Bishop （古典主義との無矛盾性を主張する構成主義を推進）
• パウル・ローレンツェン（構成的解析を開発）
• Martin Hyland （実現可能性における効果的トポス（英語版） の発見）

• Troelstra, A. S. (1977a). “Aspects of constructive mathematics”. Handbook of Mathematical Logic. pp. 973-1052 
• Troelstra, A. S. (1977b). “Choice sequences”. Oxford Logic Guides. ISBN 0-19-853163-X 

• 直観主義論理
• 直観主義型理論
• 構成的解析学（英語版）
• 構成的超準解析（英語版）

• 計算可能性理論
• 構成的証明（英語版）
• 有限の立場（英語版）
• ゲーム意味論
• 直観主義