可算選択公理と実数

構成的数学に基づいて解析学を展開し、プログラミングでそれを実装するようなコンテンツを作れないかなあと去年ぐらいから考えています。

構成的数学と一口に言っても、選択公理をどのくらい認めるかによっていくつか流儀があります。Bishopの構成的数学は従属選択公理 (dependent choice) を認めていますが、人によっては可算選択公理 (countable choice) すら使いたくないかもしれません。

Bishop流の構成的数学では、古典数学とそう変わらない実数論が展開されています。これは可算選択公理が使える、という点が大きそうです。

それでは、可算選択公理を仮定しない構成的数学だと実数の概念がどうなるか気になるのが人情だと思います。

可算選択公理と実数

まず、いくつかある実数の構成方法が同値ではなくなります。実数のポピュラーな構成法はDedekind切断によるものと、有理数のCauchy列を同値関係で割るものがありますが、これらが同値ではなくなります。そして、Cauchy列についてもmodulus of convergence（訳すなら「収束の尺度」とかでしょうか）を持つものと、持たないものに分裂します。（それぞれ、Dedekind実数、modulated Cauchy実数、modulatedではないCauchy実数、と呼ぶことにします。）

実数には重要な性質がいくつかあります。「Cauchy列について完備である（実数のCauchy列が収束する）」とか「非可算である（Cantorの対角線論法）」とかです。それぞれ検討してみましょう。

Cauchy列についての完備性は、Dedekind実数については言えるようですが、Cauchy実数についてはどうでしょうか。

簡単のために、modulated Cauchy実数からなるmodulated Cauchy列を考えましょう。方針としては、有理数近似を並べて対角線の要素を選んでいくと良さそうです。\(a_0=[(a_{00},a_{01},a_{02},\ldots)]\), \(a_1=[(a_{10},a_{11},a_{12},\ldots)]\), \(a_2=[(a_{20},a_{21},a_{22},\ldots)]\)とあったら\([(a_{00},a_{11},a_{22},\ldots)]\)で実数を構成すれば良いでしょう。が、しかし。

「有理数近似を並べる」というところで可算選択公理を使っているのではないでしょうか？それとも可算選択公理なしで「有理数近似の対角線を選ぶ」ということができるのでしょうか？これが疑問の一つです。

実数の非可算性についても考えましょう。Bishopの構成的数学では、「いかなる実数列\((a_n)\)に対しても、\(x\neq a_n\)となる実数\(x\)が存在する」というようなことが言えます（Constructive Analysis, 2.19）。ここでポイントになるのが、「実数\(x<y\), \(z\)に対して、\(z<y\)または\(x<z\)が成り立つ」（弱い比較）という性質です。これを可算無限回使えば実数の非可算性が言えます。

まあ、そんな感じなので、この論法は可算選択公理がないと成り立たなさそうです。実際に、Dedekind実数が可算になるトポスが構成できる（もちろん可算選択公理は成り立たない）ようです。

Cauchy実数の場合ですが、「有理数近似の対角線を選ぶ」ことができれば、上述の性質に頼らずに実数の非可算性が言えるかもしれません。

可算選択公理とどう向き合うべきか

そもそも、「プログラムで実装したい」という用途を念頭に置いたときに、可算選択公理を使って良いのか、避けるべきなのか、よくわかりません。

プログラム的には、「実数列から有理数近似を対角線状に取り出す」ことは問題なく書けます。そうであれば、可算選択公理はプログラムで「使える」と考えて良いのでしょうか？

あるいは、「列」の定義をいじって、「自然数全体\(\mathbf{N}\)からの写像」ではなく「自然数全体\(\mathbf{N}\)からのprefunction」とすれば、可算選択公理を回避できるのではないでしょうか？それとも、これもある種の可算選択公理を認めていることになるのでしょうか？

独学でやっているとこういう疑問が出てきた時に聞ける人がいなくて困りますね。mathoverflowとかで聞けばいいのだろうか。

もっと視野を広げて、既存の定理証明支援系が実数をどう扱っているのかも確認したほうがいいかもしれません。

Spread the love