数学ガール／計算可能性解析学

　「微妙だ」とミルカさんが言った。
　僕たちの前のカードには、こう書いてある。

$[a,b]$ を計算可能な閉区間、 $f:[a,b]\rightarrow\mathbb{R}$ を計算可能関数とする。このとき、 $f(a)$ と $f(b)$ の間にある任意の計算可能実数 $d$ に対して、ある計算可能実数 $c\in[a,b]$ が存在して、 $f(c)=d$ が成り立つ。

　「微妙？」テトラちゃんがカードを見つめながら言った。僕も、どこが微妙なのかわからない。カードには、定理が明瞭に書いてあるだけだ。
　「証明してみれば見えてくる。とりあえず、証明してみよう。中間値の定理のよく知られた証明をひねるだけでできる」と言ってミルカさんは僕のほうを見た。証明しろということらしい。
　「一般性を失うことなく、 $[a,b]=[0,1]$ , $f(a)<0$ , $f(b)>0$ , $d=0$ と仮定できる」
　僕はカードの下のほうに書き足した。

$f:[0,1]\rightarrow\mathbb{R}$ を計算可能関数で、 $f(0)<0$ と $f(1)>0$ をみたすものとする。このとき、ある計算可能実数 $c\in[0,1]$ が存在して、 $f(c)=0$ が成り立つ。

（ここに、「一般性を失うことなく……仮定できる」の説明を入れるといいかも）
　僕は続けた。
　「ある $m/2^n\in[0,1]$ （ただし、 $m$ と $n$ は正整数）が $f(m/2^n)=0$ をみたすときは、 $c$ として $m/2^n$ をとるとよい。そこで、そのような $m$ と $n$ が存在しない場合を考える。数列 $\{a_n\}$ と $\{b_n\}$ をこう定義する」
　 $a_0=0,\quad b_0=1$ .
　 $f((a_n+b_n)/2)<0$ のとき、 $a_{n+1}=(a_n+b_n)/2,\quad b_{n+1}=b_n$ .
　 $f((a_n+b_n)/2)>0$ のとき、 $a_{n+1}=a_n,\quad b_{n+1}=(a_n+b_n)/2$ .
　「区間縮小法より、 $\{a_n\}$ と $\{b_n\}$ は共通の極限値 $c$ をもつ。各 $n$ について $f(a_n)<0$ だから、 $f(c)\le0$ が成り立つ。同じく $f(b_n)>0$ だから、 $f(c)\ge0$ が成り立つ。したがって、 $f(c)=0$ が成り立つ。ここまでで、非計算版の証明終わり」
　この後はミルカさんが引き継いだ。
　「あとは、この証明で出てくる $c$ の計算可能性を確かめれば良い。ある $m$ と $n$ で $f(m/2^n)=0$ が成り立ち、 $c=m/2^n$ とおいたときについては、有理数は計算可能実数である事実からOK。そのような $m$ と $n$ が存在せず、区間縮小法で $c$ を構成したときについては、要するに、 $\{a_n\}$ と $\{b_n\}$ を順番に出力するアルゴリズムを書き下せば良い訳だ。きちんと書き下すと長くなるが」
（ここで、実際に書き下すと良いかも）
　「中間値 $d$ を与える $c$ は計算できるんですね」とテトラちゃんが言った。
　ミルカさんの返事は意外だった。
　「それは違う。計算可能な $f$ と計算可能な $d$ に対して計算可能な $c$ が存在することを示しただけだ。 $f$ と $d$ から $c$ を計算できることは示していない」
　「え、でも、証明では $f$ と $d$ から $c$ を構成していますよね」
　「まだ、気づかないかな」
　「……」
　「ある $m/2^n$ で $f(m/2^n)=0$ であるか、そのような $m/2^n$ は存在しないかは、実効的に判定できない」
　「あ、ああああああああっ！」
　テトラちゃんが大きな声を上げる。だから、ここは図書室だというのに。でも、叫びたくなる気持ちはよくわかる。
　ミルカさんは詠唱するように言う。
　「この証明は、計算可能な対象の存在を示しているが、それを計算する手続きは与えていない。実は、この証明がまずいのではなく、そのような手続きは本当に存在しないことがわかっている。この定理は本当に微妙なんだ」
　「計算可能なものがあることは証明できるのに、それを計算する手続きはない。お、おかしい！」
　テトラちゃんはまだ混乱している。
（このあと、どうしよう？）