数学哲学において、構成主義は、数学的対象が存在することを証明するためには、その対象を具体的に見つける(あるいは「構成する」)必要があると主張する。これに対し、古典数学では、対象が存在しないと仮定し、その仮定から矛盾を導き出すことで、対象を明示的に「見つける」ことなく、数学的対象の存在を証明することができる。このような矛盾による証明は非構成的とみなされ、構成主義者はこれを拒否するかもしれない。構成主義的な観点では、存在量化子の検証的解釈が伴うが、これは古典的な解釈とは相容れない。
構成主義には多くの形態がある。[ 1 ]これらには、ブロウワーによって創設された直観主義のプログラム、ヒルベルトとベルネイスの有限主義、シャニンとマルコフの構成的再帰数学、ビショップの構成的解析のプログラムが含まれる。[ 2 ]構成主義には、 CZFのような構成的集合論の研究やトポス理論の研究も含まれる。
構成主義はしばしば直観主義と同一視されるが、直観主義は構成主義のプログラムの一つに過ぎない。直観主義は、数学の基礎は個々の数学者の直観にあると主張し、それによって数学は本質的に主観的な活動であるとする。[ 3 ]他の形態の構成主義は、この直観の観点に基づいておらず、数学に対する客観的な観点と両立する。
構成的な数学の多くは直観主義論理を用いますが、これは本質的には排中律を除いた古典論理です。排中律とは、任意の命題について、その命題が真であるか、あるいはその否定が真であるかのどちらかであるという法則です。これは排中律が完全に否定されているという意味ではなく、排中律の特殊なケースは証明可能です。単に、一般的な法則が公理として仮定されていないだけです。矛盾律(矛盾する命題が同時に真であることはあり得ないという法則)は依然として有効です。
例えば、ヘイティング算術では、量化子を含まない任意の命題pに対して、これは定理です(ここで、 x、y、z ...は命題pにおける自由変数です)。この意味では、有限に限定された命題は、古典数学と同様に、真か偽かのどちらかであるとみなされますが、この二値性は無限の集合を参照する命題には適用されません。
実際、直観主義学派の創始者であるLEJ・ブロウワーは、排中律は有限の経験から抽象化され、正当化なしに無限に適用されていると考えていた。例えば、ゴールドバッハ予想は、2より大きい偶数はすべて2つの素数の和であるという主張である。任意の偶数が2つの素数の和であるかどうかを(例えば総当たり探索によって)テストすることは可能であるので、それらの偶数は2つの素数の和であるか、そうでないかのどちらかである。そして、これまでのところ、このようにテストされた偶数はすべて実際に2つの素数の和であった。
しかし、それらすべてがそうであるという既知の証明はなく、また、それらすべてがそうではないという既知の証明もありません。さらに、ゴールドバッハ予想の証明または反証が必ず存在するかどうかもわかっていません(この予想は、従来のZF集合論では決定不能である可能性があります)。したがって、ブロウワーによれば、「ゴールドバッハ予想は真であるか、そうでないかのどちらかである」と主張することは正当化されません。そして、この予想はいつか解決されるかもしれませんが、この議論は同様の未解決問題にも適用されます。ブロウワーにとって、排中律は、すべての数学的問題には解が存在すると仮定することに等しいのです。
排中律を公理から除外すると、残りの論理体系は古典論理にはない存在特性を持つ。建設的に証明されれば、実際には少なくとも一つの特定の事柄について建設的に証明されているしばしば「証拠」と呼ばれる。したがって、数学的対象の存在証明は、その構成可能性と結びついている。
古典的な実解析では、実数を定義する一つの方法は、有理数のコーシー列の同値類として定義することである。
構成的数学では、実数を構成する一つの方法は、正の整数を取る関数ƒとして構成することである。そして、有理数ƒ ( n ) と、正の整数nを入力として正の整数g ( n )を出力する関数gを出力します。
したがって、 nが増加するにつれて、 ƒ ( n )の値はどんどん近づいていきます。ƒとgを一緒に使用することで、それらが表す実数に限りなく近い有理数近似値を計算できます。
この定義に基づくと、実数eの簡単な表現は次のようになります。
この定義は、コーシー列を用いた古典的な定義に対応しますが、構成的なひねりが加えられています。古典的なコーシー列では、任意の距離に対して、(古典的な意味で)列の中に、それ以降のすべての要素がその距離よりも近くなる要素が存在することが求められます。構成的なバージョンでは、任意の距離に対して、実際に列の中でこのことが起こる点を指定できることが求められます(この必要な指定は、しばしば収束係数と呼ばれます)。実際、数学的記述の標準的な構成的解釈は、
収束係数を計算する関数の存在こそが、まさにその関数の存在を意味する。したがって、実数の2つの定義の違いは、「すべての…に対して…が存在する」という命題の解釈の違いと考えることができる。
そうなると、上記のfやgのような可算集合から可算集合への関数が実際にどのような形で構成できるのかという疑問が生じる。構成主義の様々なバージョンはこの点に関して意見が分かれる。構成は、直観主義的な見解である自由選択列として広く定義することも、アルゴリズム(より技術的には計算可能な関数)として狭く定義することも、あるいは定義しないままにしておくこともできる。例えば、アルゴリズム的な見解を採用すると、ここで構成された実数は、古典的には計算可能な数と呼ばれるものに本質的に該当する。
上記のアルゴリズム的解釈は、古典的な基数概念と矛盾するように思われる。アルゴリズムを列挙することで、計算可能な数は古典的に可算であることを示すことができる。しかし、ここでカントールの対角線論法は、実数の基数が非可算であることを示している。実数を計算可能な数と同一視することは、矛盾となる。さらに、対角線論法は完全に構成的であるように思われる。
実際、カントールの対角線論法は、自然数と実数の間の全単射が与えられた場合、関数の範囲に含まれない実数を構成し、それによって矛盾を確立するという意味で、構成的に提示することができる。関数Tを構成するアルゴリズムを列挙することができる。この関数 T については、最初は自然数から実数への関数であると仮定する。しかし、各アルゴリズムには、制約を満たさない、あるいは非終結である(Tは部分関数である)可能性があるため、対応する実数が存在する場合と存在しない場合がある。したがって、これは必要な全単射を生成することができない。要するに、実数は(個別に)効果的に計算可能であるという見解をとる人は、カントールの結果を、実数(集合的に)は再帰的に列挙可能ではないことを示すものとして解釈する。
それでも、 Tは自然数から実数への部分関数であるため、実数は可算数に過ぎないと考える人もいるかもしれない。そして、すべての自然数は自明に実数として表すことができるので、実数は可算数以上である。したがって、実数は正確に可算数である。しかし、この推論は構成的ではなく、必要な全単射を構成しない。このような状況で全単射の存在を証明する古典的な定理、すなわちカントール・ベルンシュタイン・シュレーダーの定理は非構成的である。最近、カントール・ベルンシュタイン・シュレーダーの定理は排中律を含意することが示され、したがってこの定理の構成的証明は不可能であることが示された。[ 4 ]
構成的数学における選択公理の位置づけは、様々な構成主義的プログラムのアプローチの違いによって複雑化している。数学者が非公式に用いる「構成的」という言葉の単純な意味の一つは、「選択公理を用いずにZF集合論で証明可能」である。しかし、より限定的な形式の構成的数学の提唱者たちは、ZF自体は構成的な体系ではないと主張するだろう。
直観主義的な型理論(特に高次型算術)では、選択公理の多くの形式が許容されます。たとえば、公理 AC 11 は、実数の集合上の任意の関係Rについて、各実数xに対してR ( x , y )が成り立つ実数yが存在することを証明した場合、実際にはすべての実数に対してR ( x , F ( x )) が成り立つ関数 F が存在する、と言い換えることができます。同様の選択原理は、すべての有限型に対して受け入れられています。これらの一見非構成的な原理を受け入れる動機は、「各実数 x に対して R ( x , y )が成り立つ実数yが存在する」という証明に対する直観主義的な理解にあります。BHK解釈によれば、この証明自体が本質的に望ましい関数Fです。直観主義者が受け入れる選択原理は、排中律を暗示するものではありません。
しかし、構成的集合論の特定の公理系では、ディアコネスキュ=グッドマン=マイヒル定理が示すように、選択公理は(他の公理が存在する場合)排中律を必然的に含意する。構成的集合論の中には、マイヒルの集合論における従属選択公理のように、選択公理のより弱い形式を含むものもある。
古典的な測度論は、根本的に非構成的である。なぜなら、ルベーグ測度の古典的な定義では、集合の測度や関数の積分を計算する方法が記述されていないからである。実際、関数を単に「実数を入力として実数を出力する」規則と考えるならば、関数の積分を計算するアルゴリズムは存在しない。なぜなら、どのアルゴリズムも一度に有限個の関数の値しか呼び出すことができず、有限個の値では非自明な精度で積分を計算するには不十分だからである。この難問に対する解決策は、ビショップ(1967)で最初に行われたように、収束率に関する情報を持つ連続関数(連続係数が既知)の点ごとの極限として記述される関数のみを考慮することである。測度論を構成的にする利点は、集合が構成的にフル測度であることを証明できれば、その集合内の点を見つけるアルゴリズムが存在することである(これもビショップ(1967)を参照)。
伝統的に、数学者の中には、数学的構成主義に対して、敵対的とまではいかなくとも疑念を抱いている者がいる。これは主に、数学的構成主義が構成的解析に制約をもたらすと彼らが考えていたためである。こうした見解は、1928年にデイヴィッド・ヒルベルトが『数学の基礎』の中で、「数学者から排中律を奪うことは、例えば、天文学者に望遠鏡の使用を禁じたり、ボクサーに拳の使用を禁じたりするのと同じである」と力強く表明した。[ 5 ]
エレット・ビショップは、1967年の著書『構成的分析の基礎』[ 2 ]の中で、伝統的な分析を構成的な枠組みの中で発展させることによって、これらの不安を払拭しようと努めた。
ほとんどの数学者は、構成主義の主張である「構成的方法に基づく数学のみが正当である」というテーゼを受け入れていないものの、構成的方法はイデオロギーとは無関係な観点からますます注目を集めている。例えば、解析学における構成的証明は、証拠抽出を保証する可能性があり、構成的方法の制約内で作業することで、古典的な方法を用いるよりも理論の証拠を見つけやすくなる。構成的数学の応用は、基礎数学やコンピュータ科学における注目すべき分野である型付きラムダ計算、トポス理論、圏論にも見られる。代数学では、トポスやホップ代数などの実体に対して、構造は構成的理論である内部言語をサポートしており、その言語の制約内で作業することは、可能な具体的な代数とその準同型集合について推論するなどの外部手段で作業するよりも、多くの場合、より直感的で柔軟である。
物理学者のリー・スモーリンは著書『量子重力への三つの道』の中で、トポス理論は「宇宙論にとって適切な論理形式である」(30ページ)、「初期の形態では『直観主義論理』と呼ばれていた」(31ページ)と述べている。「この種の論理では、観察者が宇宙について述べることができる命題は、少なくとも三つのグループに分けられる。すなわち、真であると判断できるもの、偽であると判断できるもの、そして現時点では真偽を判断できないものである」(28ページ)。
{{cite book}}: CS1メンテナンス: パブリッシャーの場所 (リンク){{cite book}}: CS1 maint: bot: 元の URL の状態が不明です (リンク)