たとえば、排中律により不自然な写像が場合分けによって容易に構成され、 それが直観的内容を直載に表現する種々の枠組みの不備を糾弾しインフォーマ ルのレッテルを押し続けてきた。不自然なものが建設的な自然な議論を数学の 表舞台から駆逐し、数学の記述に不必要で有害な複雑性をもたらしてきたとい える。
残念な事に、今世紀初めから続けられている構成数学者の試みは、背理法 による存在証明(存在しないと仮定すると矛盾するから存在する)を拒絶して 行う構成的存在証明が不必要に煩雑であり背理法なしには実際の数学研究はで きないという印象を一般の数学者には与えているように思われる。そして、構 成的議論の重要性は計算機科学の進展からある程度認識されるようにはなった が、数学の内部では構成主義はいまなお、その存在理由が風変わりな「趣味」 にしか求められないものと思われている。
しかし実はそうではなく、構成的議論あるいはその根源といえる排中律の 否定は数学全体に極めて重要な意義を持つ事が最近明らかになってきた。すな わち、1970年代に Lawvere によって、トポス理論の構築を通して 構成的議論 の本当の意味は、種々の数学的定式化に依存しない数学的真理を与えるという 点にある、ということを明らかになったのである。これにより、排中律の否定 は数学の議論を煩雑にするのではなく、それとは正反対に,構成的議論で得ら れた真理は、広い数学的分野に意味があることが明らかになっただけでなく、 べき零無限小に基づく総合的微分幾何学が展開されることにより、これまで発 見論的な役割しかしていなかったような議論が数学研究の本質的」な議論を与える力があること事が実証されたのである。
J.L Lambek and P.J. Scott, Introduction to higher order categorical logic, Cambridge University Press, 1986. J.L. Bell, Toposes and Local set Theories, An Introduction, Clarendon Press, Oxford 1988. C. McLarty, Elementary Categories, Elementary Toposes, Clarendon Press, Oxford 1995.