構成的数学
概要
構成的数学（constructive mathematics）とは、存在の証明には対象を作る手続きが、選言の証明にはどちらが成り立つかの指定が含まれるという直観主義論理の読み方に従って、排中律を一般の原理としては使わずに数学を展開する立場である。排中律を除くと、2 進列についての全知原理 LPO・WLPO・LLPO や Markov の原理が証明できなくなり、正則な有理数列で表した実数について「$x=y$ または $x$ と $y$ は離れている」は LPO と、「$x\ne y$ なら離れている」は Markov の原理とちょうど同値になる。代わりに有理数 $a<b$ について「$a<x$ または $x<b$」のような近似的な比較が構成的に成り立ち、近似的な中間値の定理などの基礎になる。選択公理は排中律を導くので採らず、可算選択や従属選択を前提にすることが多い。
「方程式に解がある」と証明したとき、その証明から解を実際に取り出せるだろうか。古典論理では、「解がないと仮定すると矛盾する」ことを示せば存在の証明になる。しかしこの証明は、解がどこにあるかを何も教えないことがある。構成的数学は、存在の証明にはその対象を作る手続きが含まれていなければならない、という約束のもとで数学を展開する立場である。そのために論理を直観主義論理に取り替え、排中律を一般の原理としては使わない。
排中律を使わないと、古典的には当たり前の主張のいくつかが証明できなくなる。代表例が「任意の実数 $x$ について $x=0$ または $x\ne0$」である。この記事では、こうした主張が証明できない理由を、全知原理と呼ばれる 2 進列についての弱い排中律と、実数についての主張とが同値になることとして正確に述べ、証明する（thm-cmath-reals-omniscience）。これは、ある定理がどの非構成的な原理と同じ強さかを調べる構成的逆数学の最も基本的な例でもある。
定義
構成的数学（constructive mathematics）とは、直観主義論理を用いて数学を展開する立場の総称である。とくに次の読み方（BHK 解釈）に従う。
- $\exists x\,\varphi(x)$ の証明は、具体的な対象 $t$ と $\varphi(t)$ の証明の組を与える。
- $\varphi\lor\psi$ の証明は、$\varphi$ と $\psi$ のどちらを証明するかの指定と、その証明を与える。
- $\lnot\varphi$ は $\varphi\to\bot$（$\varphi$ から矛盾が出ること）を意味する。
排中律 $\varphi\lor\lnot\varphi$ は、個々の $\varphi$ について証明できたときにだけ使う。
排中律を否定するわけではない。直観主義論理では $\lnot\lnot(\varphi\lor\lnot\varphi)$ が証明できる（直観主義論理 の命題「直観主義論理で証明できる式」）ので、「$\varphi$ でも $\lnot\varphi$ でもない命題」を作ることはできない。構成的数学で証明した定理は、古典論理でもそのまま定理である。
構成的数学にはいくつかの流儀がある。Brouwer の直観主義数学、Markov の流れをくむ再帰的構成的数学、Bishop の構成的解析学（BISH と略される）、Martin-Löf の型理論である（SEP22 §3）。この記事は Bishop の流儀に従い、自然数と有理数の通常の算術、可算選択と従属選択を前提にする（SEP22 §4）。ただし以下の証明はどれも選択原理を使わない。
決定可能な命題と全知原理
自然数や有理数の等号・大小は決定可能である。すなわち、有理数 $p,q$ について $p=q$ か $p\ne q$ か、$p\le q$ か $q< p$ かを有限回の計算で決められる。そこで、各項が $0$ か $1$ である数列 $\alpha=(\alpha(1),\alpha(2),\dots)$（2 進列）は、項ごとには決定可能な命題の列とみなせる。全知原理は、無限個の項をまとめて調べられると主張する原理である。
2 進列 $\alpha$ について、次の原理を考える。
- LPO（limited principle of omniscience）：すべての $n$ で $\alpha(n)=0$ であるか、または $\alpha(n)=1$ となる $n$ が存在する。
- WLPO（weak LPO）：すべての $n$ で $\alpha(n)=0$ であるか、またはそれが成り立たない。
- LLPO（lesser LPO）：$\alpha(n)=1$ となる $n$ が高々 1 つなら、偶数番目の項がすべて $0$ であるか、奇数番目の項がすべて $0$ である。
- MP（Markov の原理）：「すべての $n$ で $\alpha(n)=0$」が成り立たないなら、$\alpha(n)=1$ となる $n$ が存在する。
それぞれ「すべての 2 進列 $\alpha$ について」の形の主張として扱う。
どの原理も排中律から従うので、古典論理では正しい。構成的数学で証明できないことの理由は、BHK 解釈で読むと LPO が「任意の 2 進列について 1 が現れるかどうかを決める手続き」を要求するからである。たとえば $\alpha(n)$ を「$4,6,\dots,2n+2$ がすべて 2 つの素数の和なら $0$、そうでなければ $1$」と定めると、$\alpha$ は計算できる 2 進列だが、LPO をこの $\alpha$ に当てはめると Goldbach 予想の真偽が決まってしまう（SEP22 §1）。このように、ある主張から LPO などの非構成的な原理が導けることを示して、その主張が構成的には証明できないことの根拠とする論法を Brouwer 型の反例という。
LPO $\Rightarrow$ WLPO $\Rightarrow$ LLPO である。また LPO は「WLPO かつ MP」と同値である。
要点：どれも 2 進列の各項が決定可能であることだけを使う。
詳しい証明を開く
LPO $\Rightarrow$ WLPO：$\alpha(n)=1$ となる $n$ があれば「すべての項が $0$」は成り立たない。
WLPO $\Rightarrow$ LLPO：$\alpha$ の 1 が高々 1 つとし、$\beta(n):=\alpha(2n)$ に WLPO を当てはめる。$\beta$ の項がすべて $0$ なら偶数番目の項がすべて $0$ である。そうでないとき、奇数 $m$ をとる。$\alpha(m)$ は $0$ か $1$ であり、$\alpha(m)=1$ なら 1 は高々 1 つなので偶数番目の項はすべて $0$ となって仮定に反する。よって $\alpha(m)=0$ であり、奇数番目の項はすべて $0$ である。
LPO $\Rightarrow$ MP：「すべての項が $0$」が成り立たないとき、LPO の 2 つの場合のうち前者は矛盾し、矛盾からは何でも従うので、どちらの場合も $\alpha(n)=1$ となる $n$ が得られる。
WLPO かつ MP $\Rightarrow$ LPO：WLPO で「すべての項が $0$」か、その否定かが決まる。否定の場合は MP で $\alpha(n)=1$ となる $n$ が得られる。$\square$
実数
構成的数学では、実数を収束の速さを指定した有理数列で表す（SEP22 §2）。収束の速さを指定するのは、近似値を計算できるようにするためである。
有理数列 $x=(x_n)_{n\ge1}$ が正則であるとは、すべての $m,n\ge1$ で
$$
\lvert x_m-x_n\rvert\le\frac1m+\frac1n
$$
となることをいう。正則な有理数列を実数とよび、実数 $x,y$ について次のように定める。
- $x=y$ $:\iff$ すべての $n$ で $\lvert x_n-y_n\rvert\le\dfrac2n$。
- $x\mathrel{\#}y$（$x$ と $y$ は離れている）$:\iff$ ある $n$ で $\lvert x_n-y_n\rvert>\dfrac2n$。
- $x< y$ $:\iff$ ある $n$ で $y_n-x_n>\dfrac2n$。$x\le y$ $:\iff$ すべての $n$ で $x_n\le y_n+\dfrac2n$。
有理数 $q$ は定数列 $(q,q,\dots)$ と同一視する。
$x\mathrel{\#}y$ は「$x$ と $y$ が違うことを、有限の精度で目撃できる」という正の情報である。古典論理では $x\mathrel{\#}y$ と $x\ne y$ は同じことだが、構成的にはそうとは限らない（thm-cmath-reals-omniscience の 3）。
実数 $x,y,z$ について次が成り立つ。
- $x=y$ であることと、$x\mathrel{\#}y$ でないことは同値である。
- $=$ は同値関係である。
1：各 $n$ で $\lvert x_n-y_n\rvert\le2/n$ か $\lvert x_n-y_n\rvert>2/n$ かは有理数の比較なので決定可能である。$x=y$ かつ $x\mathrel{\#}y$ なら、ある $n$ で両方が成り立ち矛盾する。逆に $x\mathrel{\#}y$ でないなら、各 $n$ で $\lvert x_n-y_n\rvert>2/n$ は成り立たず、決定可能性により $\lvert x_n-y_n\rvert\le2/n$ である。
2：反射性と対称性は定義から明らかである。推移性を示す。$x=y$、$y=z$ とし、$n$ を固定する。任意の $m$ について、正則性と仮定から
$$
\lvert x_n-z_n\rvert\le\lvert x_n-x_m\rvert+\lvert x_m-y_m\rvert+\lvert y_m-z_m\rvert+\lvert z_m-z_n\rvert\le\Bigl(\frac1n+\frac1m\Bigr)+\frac2m+\frac2m+\Bigl(\frac1m+\frac1n\Bigr)=\frac2n+\frac6m
$$
である。もし $\lvert x_n-z_n\rvert>2/n$ なら、$6/m<\lvert x_n-z_n\rvert-2/n$ となる $m$ がとれて矛盾する。比較の決定可能性により $\lvert x_n-z_n\rvert\le2/n$ である。$\square$
主定理：実数の比較と全知原理
主定理の証明の要点は、実数の比較を 2 進列に翻訳すること（lem-cmath-compare）と、逆に 2 進列を実数に符号化すること（lem-cmath-encode）である。先にこの 2 つの補題を示す。
実数 $x,y$ に対し、2 進列 $\beta_{x,y}$ を、$\lvert x_n-y_n\rvert>2/n$ なら $\beta_{x,y}(n)=1$、そうでなければ $0$ と定める。このとき $x=y$ はすべての $n$ で $\beta_{x,y}(n)=0$ であることと同値であり、$x\mathrel{\#}y$ は $\beta_{x,y}(n)=1$ となる $n$ が存在することと同値である。
$\beta_{x,y}(n)$ は有理数の比較で決まるので 2 進列である。2 つの同値は def-cmath-real をそのまま言い換えたものである。$\square$
2 進列 $\alpha$ に対し $r_n:=\sum_{k=1}^{n}\alpha(k)2^{-k}$ とおくと、$r_\alpha:=(r_n)_n$ は実数であり、次が成り立つ。
- $r_\alpha=0$ $\iff$ すべての $k$ で $\alpha(k)=0$。
- $r_\alpha\mathrel{\#}0$ $\iff$ $\alpha(k)=1$ となる $k$ が存在する。
正則性。$m< n$ なら $0\le r_n-r_m\le\sum_{k=m+1}^{n}2^{-k}<2^{-m}\le\dfrac1m\le\dfrac1m+\dfrac1n$ である（$2^m\ge m$ を使った）。
鍵となる不等式。$\alpha(k)=1$ とし、$N:=2^{k+1}+1$ とおくと、$N\ge k$ なので $r_N\ge2^{-k}$ であり、$N>2^{k+1}$ から $2/N<2^{-k}$ である。よって $\lvert r_N\rvert>2/N$ である。$(\ast)$
1：$r_\alpha=0$ とし、$k$ を固定する。$\alpha(k)$ は $0$ か $1$ であり、$\alpha(k)=1$ なら $(\ast)$ が $r_\alpha=0$（$\lvert r_N\rvert\le2/N$）に反する。よって $\alpha(k)=0$ である。逆にすべての項が $0$ なら、すべての $r_n$ が $0$ なので $r_\alpha=0$ である。
2：$r_\alpha\mathrel{\#}0$ なら、ある $n$ で $r_n>2/n>0$ である。$r_n$ は $\alpha(1),\dots,\alpha(n)$ の有限和なので、$k=1,\dots,n$ を順に調べれば $\alpha(k)=1$ となる $k$ が見つかる。逆に $\alpha(k)=1$ なら $(\ast)$ により $r_\alpha\mathrel{\#}0$ である。$\square$
直観主義論理のもとで、次が成り立つ。
- LPO $\iff$ すべての実数 $x,y$ について $x=y$ または $x\mathrel{\#}y$。
- WLPO $\iff$ すべての実数 $x,y$ について $x=y$ または $\lnot(x=y)$。
- MP $\iff$ すべての実数 $x,y$ について、$\lnot(x=y)$ ならば $x\mathrel{\#}y$。
- すべての実数 $x$ について $x\le0$ または $0\le x$ が成り立つなら、LLPO が成り立つ。
1。LPO を仮定し、実数 $x,y$ をとる。LPO を $\beta_{x,y}$ に当てはめると、すべての項が $0$ か、項 $1$ が存在するかのどちらかであり、lem-cmath-compare によりそれぞれ $x=y$、$x\mathrel{\#}y$ である。逆に右辺を仮定し、2 進列 $\alpha$ をとる。右辺を $r_\alpha$ と $0$ に当てはめると、$r_\alpha=0$ か $r_\alpha\mathrel{\#}0$ であり、lem-cmath-encode によりそれぞれ「すべての項が $0$」「項 $1$ が存在する」である。
2。WLPO を $\beta_{x,y}$ に当てはめると、「すべての項が $0$」かその否定が得られ、lem-cmath-compare によりそれぞれ $x=y$、$\lnot(x=y)$ である。逆に右辺を $r_\alpha$ と $0$ に当てはめ、lem-cmath-encode の 1 で読み替えれば WLPO の結論を得る。
3。MP を仮定し、$\lnot(x=y)$ とする。lem-cmath-compare により「$\beta_{x,y}$ の項がすべて $0$」が成り立たないので、MP により項 $1$ が存在し、$x\mathrel{\#}y$ である。逆に右辺を仮定し、「$\alpha$ の項がすべて $0$」が成り立たないとする。lem-cmath-encode の 1 により $\lnot(r_\alpha=0)$ であり、右辺から $r_\alpha\mathrel{\#}0$、同じ補題の 2 により $\alpha(k)=1$ となる $k$ が存在する。
4。$\alpha$ を、1 が高々 1 つの 2 進列とし、$s_n:=\sum_{k=1}^{n}(-1)^k\alpha(k)2^{-k}$ とおく。prf-cmath-encode と同じ評価 $\lvert s_n-s_m\rvert\le\sum_{k=m+1}^n2^{-k}<2^{-m}$ により $s=(s_n)$ は実数である。仮定から $s\le0$ か $0\le s$ である。
$s\le0$ の場合、偶数 $k$ をとる。$\alpha(k)=1$ と仮定すると、1 は高々 1 つなので $j\ne k$ では $\alpha(j)=0$ であり、$n\ge k$ で $s_n=2^{-k}$ である。$N:=2^{k+1}+1$ とおくと $s_N=2^{-k}>2/N$ となり、$s\le0$（すべての $n$ で $s_n\le2/n$）に反する。よって $\alpha(k)=0$ であり、偶数番目の項はすべて $0$ である。$0\le s$ の場合は、奇数 $k$ について $s_n=-2^{-k}$ となることから同様に、奇数番目の項がすべて $0$ である。これが LLPO である。$\square$
1〜3 は、古典的には当然の 3 つの主張が、それぞれちょうど LPO・WLPO・MP の強さをもつことを示している。とくに 3 は、「$0$ でない実数は $0$ から離れている」という素朴な推論が、無限の探索を必ず終えられるという Markov の原理と同じであることを意味する（SEP22 §2 は同じ同値を述べている）。
4 から、二分法による中間値の定理の通常の証明は構成的でないことが分かる。区間の中点 $c$ で「$f(c)<0$ か $0\le f(c)$ か」を判定する段で、4 の左辺と同じ種類の、実数の符号の判定を使っているからである。実際、「$[0,1]$ 上の連続関数 $f$ が $f(0)f(1)<0$ を満たせば、$0< x<1$ かつ $f(x)=0$ となる $x$ が存在する」という形の中間値の定理から LLPO が導かれる（SEP22 §2。この記事では証明しない）。
構成的に使える代わりの原理
実数の三分法の代わりに構成的数学で使うのが、次の「近似的な比較」である。
実数 $x$ と有理数 $a< b$ について、$a< x$ または $x< b$ である。
$n(b-a)>4$ となる正の整数 $n$ をとり、$c:=(a+b)/2$ とおく。$x_n\ge c$ か $x_n< c$ かは有理数の比較なので決定できる。$x_n\ge c$ なら $x_n-a\ge(b-a)/2>2/n$ なので、def-cmath-real により $a< x$ である。$x_n< c$ なら $b-x_n>(b-a)/2>2/n$ なので $x< b$ である。$\square$
この命題は $x$ の近似値を 1 つ計算するだけで結論を出すので、どちらの場合かを実際に決める手続きを含んでいる。これを使うと、連続関数 $f\colon[0,1]\to\mathbb{R}$ が $f(0)\le0\le f(1)$ を満たすとき、任意の $\varepsilon>0$ について $\lvert f(x)\rvert<\varepsilon$ となる $x$ が存在するという近似的な中間値の定理が、従属選択公理を使って構成的に証明できる（Bau17 Proposition 5.2・Theorem 5.4。この記事では証明しない）。零点そのものではなく、要求された精度の近似解を与える定理であり、数値計算の二分法が実際に行っていることに対応する。
例と反例
集合が有限であるとは、ある $n\in\mathbb{N}$ について $\{1,\dots,n\}$ と全単射で結ばれることをいう（$n=0$ なら空集合）。「有限集合の部分集合はつねに有限である」という主張は、排中律と同値である（Bau17 Theorem 2.1）。
実際、排中律を仮定すれば、有限集合 $A=\{a_1,\dots,a_n\}$ の部分集合 $B$ について各 $a_i$ が $B$ に属するかどうかが決まり、属さないものを取り除けば $B$ の数え上げが得られる。逆に、命題 $P$ をとり、$B:=\{0\mid P\}\subset\{0\}$（$P$ が成り立つときだけ $0$ を含む集合）を考える。$B$ が有限なら $\{1,\dots,n\}$ との全単射があり、$n=0$ か $n\ge1$ かは決定できる。$n=0$ なら $B$ は空なので、$P$ を仮定すると $0\in B$ となり矛盾し、$\lnot P$ である。$n\ge1$ なら $B$ は元をもち、その元は $0$ だから $P$ が成り立つ。よって $P\lor\lnot P$ である。
構成的数学では、有限集合の部分集合は「属するかどうかが決定可能なとき」に限って有限になる。
任意の空でない集合の族が選択関数をもつという選択公理を構成的数学に加えると、排中律が導かれる（Diaconescu の定理。証明は 排中律 の定理「Diaconescu の定理」、Bau17 Theorem 1.3）。そのため構成的数学では選択公理をそのままの形では採らない。一方、添字が自然数の場合の可算選択公理や従属選択公理は、Bishop の流儀では受け入れられることが多い（SEP22 §4）。選択公理の使い方を細かく区別する習慣が構成的数学で保たれているのはこのためである。
ここで「空でない」は「元が存在する」（inhabited）の意味である。構成的には、$\lnot(A=\emptyset)$ から $A$ の元の存在は出ないので、2 つは区別される。
反例の表
| 外す条件 | 反例 | 成り立たなくなること |
|---|---|---|
| 実数を表す列の正則性（def-cmath-real） | $x_n=0$、$y_n=2/n$、$z_n=4/n$ | $=$ の推移性（lem-cmath-equality）。$\lvert x_n-y_n\rvert\le2/n$、$\lvert y_n-z_n\rvert\le2/n$ だが $\lvert x_n-z_n\rvert=4/n$ |
| $a< b$ の真の不等号（prop-cmath-located） | $a=b=0$、$x=0$ | 「$a< x$ または $x< b$」。$0<0$ はどの $n$ でも $0-0>2/n$ とならないので成り立たない |
| LLPO の「1 は高々 1 つ」（def-cmath-omniscience） | すべての項が $1$ の列 | 「偶数番目がすべて $0$ か奇数番目がすべて $0$」。どちらにも $1$ がある |
1 行目の $y,z$ は正則でない。たとえば $\lvert y_1-y_n\rvert=2-2/n$ は $n\ge4$ で $1+1/n$ を超える。
逆数学・モデルとの関係
構成的逆数学。thm-cmath-reals-omniscience のように、構成的な基礎（BISH）の上で、古典的な定理がどの非構成的な原理（LPO・WLPO・LLPO・MP・排中律など）と同値になるかを調べる研究を構成的逆数学という（SEP22 §5）。Brouwer 型の反例は、その片方向「定理 $\Rightarrow$ 非構成的な原理」を与えるものと見られる。古典論理の上で集合存在公理の強さを測る逆数学とは、基礎の論理も測る物差しも異なる。
モデル。全知原理が構成的に証明できないことは、それが偽になる解釈を作ることで確かめられる。計算可能な関数だけを使う実現可能性の解釈では、「$x=0$ または $x\ne0$」を実現するプログラムがあれば停止問題が解けてしまうので、この主張は実現されない（Bau17 §3.2）。位相空間上の層のトポスでは、真理値は開集合であり、排中律が成り立たない（Bau17 §3.3）。トポスの中で論理式を解釈する仕組みは 内部論理 で述べる。
関連項目
参考文献
Mathpediaは寄付と、参考文献の書籍リンク（Amazonアソシエイト）の紹介料で運営されています。 支援について ／ 寄付する
