構成主義 (数学)
構成的なバージョンでは、与えられた距離よりも実際に互いの距離が小さくなる要素を特定できることを要請する(このように特定された要素の位置は、しばしば収束係数(英語版)と呼ばれる)。事実、数学的言明
∀ n : ∃ m : ∀ i , j ≥ m : | f ( i ) − f ( j ) | ≤ 1 n {\displaystyle \forall n:\exists m:\forall i,j\geq m:|f(i)-f(j)|\leq {1 \over n}}
の標準的な構成的解釈(英語版)(BHK解釈)は、正確に収束係数を計算する関数が存在することである。このように、実数の2つの定義の違いは「すべての...に対して、...が存在する」という言明の解釈の違いにあると考えられる。
すると、上記の f と g のように、可算集合から可算集合へのどの関数が実際に構成できるのかという質問が湧き出る。構成主義の異なるバージョンでは、この点で解釈が分かれる。こうした構成は直観主義的視点である自由選択列(英語版)と同程度に広く、またはアルゴリズム(より専門的には計算可能関数)と同程度に狭く、あるいは未特定のまま定義できる。例えば、アルゴリズム的観点で考えた場合、ここで構成した実数は、本質的には古典的に計算可能数と呼ばれるものになるだろう。
特定の偶数に対して2つの素数の和であるか否かを確かめることは可能であるので(たとえば力まかせ探索で)、(2より大きい)任意の偶数は、2つの素数の和であるかそうでないかである。そしてこれまでのところ、各偶数は実際に2つの素数であることが上記のように確かめられている。
しかし、全ての偶数がゴールドバッハの予想を満たすことの証明も、ゴールドバッハの予想を満たさない偶数があることの証明も存在しない。それどころか、ゴールドバッハの予想の証明または反証が存在するかどうかすら不明である(ゴールドバッハの予想は従来型のZF集合論では決定不能かもしれない)。したがってブラウアーにとっては、「ゴールドバッハの予想が真である、あるいは偽である」という主張は正当化されない。また、この予想がいつか解かれたとしても、この主張を似た未解決問題に適用すれば同じ議論となる。ブラウアーにとっては、排中律はどの数学的問題にも解があると仮定するのと同じである。
公理として排中律を排除した場合、残る論理体系には古典論理が持たない存在性質(英語版)を持つ: ∃ x ∈ X P ( x ) {\displaystyle \exists _{x\in X}P(x)} が構成的に証明されているならばいつでも、実際に P ( a ) {\displaystyle P(a)} は(少なくとも)1つの特定の a ∈ X {\displaystyle a\in X} に対して構成的に証明される(この a のことをしばしば証拠(witness)と呼ぶ)。このように、数学的対象の存在の証明はその構成と紐付いている。