背理法による証明の例として、よく「\(\sqrt{2}\)が無理数であること」が挙がる。大まかな流れは以下の通りだ：
「\(\sqrt{2}\)が有理数だったと仮定し、\(\sqrt{2}=p/q\)（\(p\), \(q\)は互いに素）とおく。すると\(2q^2=p^2\)で、左辺が偶数なので右辺も偶数、よって\(p\)は\(p=2p’\)と書ける。すると\(q^2=2p’^2\)が得られて、\(q\)も偶数ということになる。これは『\(p\)と\(q\)は互いに素』という仮定に反する。よって、\(\sqrt{2}\)は有理数ではない（無理数である）。」
さて、数学の一部の流儀では使用する論理を制限することがある。構成的数学というのがその例で、大まかには「排中律を使わないような数学」つまり「直観主義論理に基づいた数学」が構成的数学になる（Brouwerの「直観主義」とは違うので注意されたい。あと、構成的数学の中でも選択公理をどの程度認めるかでバリエーションがあるようだ）。「\(\sqrt{2}\)が無理数である」という上記の証明は、構成的数学では受け入れられるのだろうか？
世間で「背理法」と呼ばれる論法は、論理の推論規則としては2種類に分けられる：「否定の導入」と「狭義の背理法（ヤバい方の背理法）」だ。否定の導入は、「Pであることを仮定したら矛盾した。よってPの否定（¬P）が成り立つ」というやつで、狭義の背理法は「¬Pを仮定したら矛盾した。よってPが成り立つ」というやつだ。そして、直観主義論理では否定の導入は問題なく使えて、狭義の背理法は（一般には）使えない。
最初の「\(\sqrt{2}\)が無理数であること」の証明を見直すと、使っている背理法は「否定の導入」であり、そうすると直観主義論理に基づいた数学である構成的数学でも問題なく成り立ちそうだ。……本当に？
最初に書いた「\(\sqrt{2}\)が無理数であること」の証明がそのまま通用するには、「無理数」の定義が「有理数ではない数」つまり「その数が有理数と仮定すると矛盾すること」である必要がある。構成的数学での無理数の定義はこれで良いのだろうか？
数学の基礎を弱めた時、この場合は使う論理を古典論理から直観主義論理に変えるということだが、古典的には（古典論理に基づいた数学では）同値だった条件が構成的には同値ではなくなるということがよく起こる。その結果、古典数学で一つの名前がついていた概念が構成的数学ではいくつもの概念に分裂することがある。例えば、環論の一意分解整域（UFD）は構成的数学では4つか5つくらいの概念に分裂する（詳しくはMines, Richman, Ruitenburg「A Course in Constructive Algebra」などを参照。ただし一部の定義に欠陥が含まれるので鵜呑みにはしないこと）。
無理数の定義に戻るが、論理的な否定、「〜と仮定すると矛盾する」という性質は構成的数学ではあまり出番がない。例えば、実数\(x\)の逆数を取る時は、「\(x=0\)と仮定すると矛盾する」という条件では弱く、「\(x\)が0から離れていること（apartness）」つまり「\(x<0\)または\(x>0\)である」という条件を要請する。古典数学での「\(x\neq 0\)」という条件が構成的数学では「\(\lnot(x=0)\)」と「\(x⋕0\)（これは\(x<0\lor x>0\)のこと）」に分裂するのだ。後者の方が好まれる理由は、そちらの方が有意義なデータを含んでいるから、とでも言うべきだろうか。だから、「無理数」の定義も、有意義なデータを含んでいるものにする動機がある。
つまり、古典数学での「実数\(x\)が無理数である」という条件は、構成的数学では「\(x\)が有理数だと仮定すると矛盾する」と「どんな有理数\(r\)を取っても、\(x\)は\(r\)から離れている（\(x⋕r\)）」に分裂し、後者の方が有意義なデータを含んでいると考えられる。
実際、Bishop, Bridges「Constructive Analysis」のChapter 2のProblem 10では後者の「どんな有理数\(r\)を取っても〜」という言い方で無理数（irrational）を定義している。nLabの「irrational number」では両者を「weakly irrational」と「strongly irrational/strictly irrational」と区別している。
結論としては、最初に書いた「\(\sqrt{2}\)が無理数であることの証明」は「無理数」を弱い意味で定義すれば構成的数学でも有効だが、定義が弱いのであまり価値がないということになる。自分で書きながらゴールポストずらしみたいだなあと思ってしまうが、ゴールポストが分裂したのだから仕方がない。
もっとも、最初の証明を「狭義の無理数」でも成立するように書き換えるのは難しいことではない。要は与えられた有理数\(r\)に対して\(r<\sqrt{2}\)か\(r>\sqrt{2}\)が成り立つことを言えば良いのだ。証明のスケッチは以下のようになるだろう：
「有理数\(r\)が与えられたとする。有理数は比較ができるので、\(r^2\)と\(2\)を比較する。つまり『\(r^2<2\)または\(r^2=2\)または\(r^2>2\)』が成り立つ。場合分けをするが、\(r^2=2\)はありえない（冒頭の証明の議論を参照！）。\(r^2<2\)ならば\(r<\sqrt{2}\)である。\(r^2>2\)ならば、\(r\)の符号で\(r<\sqrt{2}\)か\(r>\sqrt{2}\)かが決まる。」
「\(r^2<2\)ならば\(r<\sqrt{2}\)である。」の部分は少し議論が要るかもしれないが、「\(r\)と0を比較して\(r\geq 0\)であれば\(0<2-r^2=(\sqrt{2}-r)(\sqrt{2}+r)\)の両辺を\(\sqrt{2}+r\)で割る」というような感じでできるだろう。
そんな感じでここ数年は構成的数学に興味があるのだが、いかんせん完全に独学なので、変なことを言ってないか心配になる。この記事の内容程度なら大丈夫だと思うけど、どうかな……。