パラレルワールドをチラ見する

ちゃんと理解していない直観主義的解析学

ブラウワー流の直観主義的な解析学では、普通の解析学とは異なることが証明されるらしい。今回は、それをチラ見する*1。

1. 自由選列と連続性原理
2. 内容を見る
- 2-1. 排中律
- 2-2. 関数の連続性
3. まとめ

1. 自由選列と連続性原理

ブラウワー流の解析学では、直観主義論理を採用するほかに、自由選列というアイディアで実数の構成を行うという特色があります。

例えば、自然数列 $a_n$ を考えると、ブラウワー的直観主義では「完結した数列全体」という考えは妥当ではないとされます。したがって、今、数列の第100項目までを開けたのであれば、

・ $a_0$ ～ $a_{99}$ までは、構成済み（確定した）対象

であり、

・ $a_{100}$ 以降については、まだ構成されていない（確定したものと扱うことができない）対象

となっていることになります。自由選列は、このような未構成の部分について、「多かれ少なかれ自由に進行する無限系列」という捉え方をします*2。

今回は、実数が関わるので、自然数列ではなく有理数列を、もっと言うと、コーシー列になるような有理数列を考えます。なので、コーシー列の範囲内で、自由に進行するかもしれない数列というものを使っていくことにします。

※ここでは、コーシー列を、収束速度付きのものとして、

$\forall n, i, j [n \lt i, j \to |a_i - a_j| \lt 2^{-n}$ ]

とします。

「任意の実数」について何かを示そうとする場合、第 $n$ 項まで開けたときに、

・規則で完全に制御されていて第 $n+1$ 項が予想できる数列*3

以外に、

・コーシー列の枠内で第 $n+1$ 項が予想できない数列

についても成立するような議論をしなければなりません。

ということは、コーシー列の全体を見ないと分からないような性質は、ブラウワー流では許されないということです。逆に言うと、実数に関する命題は、「コーシー列の途中までを見て分かる」ようなものになっているということになります。

ということで、ブラウワー流解析学では、「任意の実数 $a$ が性質 $P$ を満たす」と言えるときには、 $a$ と $P$ に応じて決まる自然数 $n$ が存在して、コーシー列の第 $n$ 項までを見れば、 $P(a)$ であることが分かるようにできている･･･ということが言えるはずです。

このとき、 $0 \leq i \leq n$ で $|a_i - b_i| \lt 2^{-i}$ となるようなコーシー列 $b_n$ があったとすると、第 $n$ 項までは $a_n$ と区別が付かないはずです*4。つまり、「コーシー列の第 $n$ 項までを見れば、 $P(a)$ であることが分かる」のであれば、 $b_n$ でも性質 $P$ が成り立っていると言えることになります。

これを定式化すると、コーシー列 $a_n$ と $b_n$ が第 $N$ 項まで区別が付かないことを、 $b \in a_N$ と書くことにして*5、

$(1) \quad \forall a P(a) \to \forall a \exists n \forall b \in a_n P(b)$

のような感じになるはずです*6。

(1)のような式が連続性原理と呼ばれるもので、ブラウワー流解析学に特有のもの（＝普通の解析学と食い違いが生じるモト）です。

2. 内容を見る

2-1. 排中律

ブラウワー流の解析学では、一部の排中律を否定できます。

具体的には、

$(2) \quad \forall a [\forall n (a_n = 0) \lor \neg \forall n (a_n = 0)$ ]

のような形の排中律を否定できます*7。

否定の導入を使用したいので、(2)を仮定しておきます。

で、(1)を $\lor$ 用に変形して、

$(3) \quad \forall a (P(a) \lor Q(a)) \to \forall a \exists n (\forall b \in a_n P(b) \lor \forall b \in a_n Q(b))$

とします。(2)と(3)より、

$(4) \quad \forall a \exists n (\forall b \in a_n \forall m (b_m = 0) \lor \forall b \in a_n \neg \forall m (b_m = 0))$

です。

ここで、場合分けを考えます。

(i) $\forall b \in a_n \forall m (b_m = 0)$ の場合

${a_n} = 0, 0, ...$ というような数列を持ってきたとき、ある $N$ が存在して、

$|b_n - 0| \lt 2^{-N}$

となるようなすべての $b_n$ で $b_n = 0$ ということを主張する文ですが、 $b_n$ の条件からは、 $n = N+100$ とかを構成したときに $2^{-(N+100)}$ とかになるようなものを排除できません（もちろんこの例は、全ての $n$ で0と等しくはなりません）。したがって、この主張は不成立ということになります。

(ii) $\neg \forall b \in a_n \forall m (b_m = 0)$ の場合

${a_n} = 0, 0, ...$ というような数列を持ってきたとき、ある $N$ が存在して、

$|b_n - 0| \lt 2^{-N}$

となるようなすべての $b_n$ で $b_n = 0$ ではないということを主張する文ですが、 $b_n$ の条件は別に、「すべての $n$ で $b_n =0$ となる数列」を排除する訳ではありません。そのため、すべての $n$ で $b_n =0$ となる数列がそのまま反例となります。したがって、この主張は不成立ということになります。

(i)と(ii)により、(4)はいずれにせよ成立しない（どちらの場合も反例を構成可能）ということが分かりました。したがって、否定の導入により、元々の仮定を否定して、

$\neg \forall a [\forall n (a_n = 0) \lor \neg \forall n (a_n = 0)$ ]

であることが分かりました。

2-2. 関数の連続性

連続性原理の考え方は、実数関数にも適用されます*8。

これまでの考え方からすると、関数の値となる実数（コーシー列）を第 $N$ 項まで計算しようと思ったときには、入力値となる実数（コーシー列）の第 $M$ 項までを見ればＯＫ･･･という仕組みになっているはずです。

さて、関数が点 $x_0$ で連続であるとは、次のようなことでした。

どんなに小さい正の実数 $\epsilon$ （※正なので $\epsilon \gt 0$ ）を持ってきても、それに対して正の実数 $\delta$ （※正なので $\delta \gt 0$ ）を取ってきて、 $|x - x_0| \lt \delta$ を満たす任意の実数 $x$ で、

$|f(x) - f(x_0)| \lt \epsilon$

となる。

最後の条件は、 $0 \lt 2^{-n} \lt \epsilon$ となる $2^{-n}$ において、

$|f(x) - f(x_0)| \lt 2^{-n}$

となればよい*9ので、実際にはそちらを使用します。

今回のコーシー列の定義から、 $f(x_0)$ の値を $\pm 2^{-n}$ の精度で確定させようとする場合は、数列 ${f(x_0)}_n$ の第 $n$ 項までを構成できればよいはずです。上の関数における連続性原理の考え方から、対応する $m$ が存在して、数列 $x_{0n}$ の第 $m$ 項までが分かれば、目的は達成されることになる･･･はずです。

これは、 $x \in x_{0m}$ を満たす任意の $x$ についても、同じことが成り立つということなので、 ${f(x)}_n$ の第 $n$ 項までを構成してみると、 $f(x_0)$ の値と $\pm 2^{-n}$ の差でしか違わないことになります。

ここで「 $x \in x_{0m}$ を満たす」が $|x_m - x_{0m}| \lt 2^{-m}$ を、「 $f(x_0)$ の値と $\pm 2^{-n}$ の差でしか違わない」が $|f(x) - f(x_0)| \lt 2^{-n}$ を意味することを思い起こすと、 $\delta = 2^{-m}$ としたときに、関数の連続の定義に当てはまっていることが分かります。

関数 $f$ には特に条件はつけていませんでした。

ということは、ブラウワー流の解析学においては、「実数全域を定義域とする実数関数は、すべて連続になる」という定理が成り立つことになります。普通の解析学では普通に不連続関数が存在するので、かなり奇異な主張をしているように見えます。が、連続性原理を認めてしまうと、この定理が成立してしまうのです。

3. まとめ

ブラウワー流の解析学では、普通あり得ないような定理が成り立つ*10。

*1:ベースは、

金子洋之(1990) 「選列と論理Ⅰ：直観主義解析学における連続性原理」北海道大學文學部紀要, 39(1), 17-50

ですが、もちろんちゃんと理解していない

*2:金子(1990)p.23より孫引き

*3:予想はできるが、まだ構成された訳ではないので存在はしていない

*4:コーシー列的観点で

*5:金子(1990)と定義が違うけど、たぶん大丈夫じゃないかと思う（無根拠）。

*6:たぶん

*7:金子(1990) pp.39-40

*8:ここから先は完全に五里霧中

*9:コレたぶん $0 \lt 2^{-n} \lt \epsilon$ となる $2^{-n}$ が存在することの証明が必要。

おそらく、連続性原理から示せるんじゃないかと思っているが、よく分からない。

*10:Q. じゃあまともに数学できないのでは？

A. 英語版WikipediaのConstructive analysis - Wikipediaを見ると、中間値の定理そのものは成り立たないが、中間値の定理っぽい定理は成り立つ（任意精度で0に近づけることができる）ので、それっぽい代替手段を駆使すれば結構いける。

ブラウワー流とは異なるが、ビショップ流が結構色々できることを示したらしい。