直観主義と選択公理の話 - 論理とか計算機とか数学とか

下記の講義ノートを読んでいたら選択公理のことが書いてあって，それがおもしろかったのでこの記事を書こうとしています。

http://math.andrej.com/2005/08/23/realizability-as-the-connection-between-computable-and-constructive-mathematics/

直観主義と選択公理の関係って相性がよさそうな悪そうなよくわからないものなのですが，そのあたりの事情がちょっと整理できました。

BHK interpretation と選択公理

BHK (Brower-Heyting-Kolmogorov) interpretation というものがあります (http://en.wikipedia.org/wiki/Brouwer%E2%80%93Heyting%E2%80%93Kolmogorov_interpretation)。大雑把にいうと，証明とはその具体的証拠の構成のことである，というような立場から論理式あるいは数学的主張の意味を解釈することだとぼくは思っていますが，BHK interpretation を解説する記事ではないので詳しい説明は省きます。*1

その BHK interpretation によると， $\forall x. P(x)$ の証明は $x$ を入力すると $P(x)$ の証明を出力する手続きであり， $\exists x. P(x)$ の証明は具体的な値 $a$ と $P(a)$ の証明の組であると解釈されます。

この解釈に従って $\forall x \exists y. \varphi(x, y)$ の意味を考えるとどうなるでしょうか。この論理式の証明は， $x$ から $y$ (と $\varphi(x, y)$ の証明)を構成する手続きとなります。だとすると，素朴に考えて $\forall x \exists y. y \in A_x$ の証明は集合族 $A_x$ の選択関数を与えるような気がします。だから選択公理は BHK interpretation に基づくと非常にもっともらしい公理であるように思えます。

ところで，BHK interpretation のような「具体的な構成」を重視する考え方は構成的論理との親和性が高いとされています。実際，BHK interpretation に基づいて直観主義論理は自然に解釈できますが，排中律のような直観主義的に認められない公理を解釈するのはそれほど簡単ではありません。

そうすると，選択公理の主張は構成的なのでしょうか？一般にはその逆で，非構成的であると言われていますが。

選択公理 ⇒ 排中律

実は，集合論のいくつかの公理と選択公理を認めると排中律が証明できます。

やってみましょう。(http://plato.stanford.edu/entries/axiom-choice/#AxiChoLog にあるのと同じ方針です)

$A = \lbrace x \in \lbrace 0, 1 \rbrace \mid x = 0 \vee \varphi \rbrace$
$B = \lbrace x \in \lbrace 0, 1 \rbrace \mid x = 1 \vee \varphi \rbrace$
$X = \lbrace A, B \rbrace$

とおきます(ここで内包公理と非順序対の公理を使いました)。すると $0 \in A, 1 \in B$ から

$\forall x \in X, \exists a, a \in x$

がいえるので，選択公理を使って選択関数 $f: X \to \lbrace 0, 1 \rbrace$ がとれます。選択関数なので $f(A) \in A, f(B) \in B$ となることから

$(f(A) = 0 \vee \varphi) \wedge (f(B) = 1 \vee \varphi)$

がいえるのですが，これより

$(f(A) = 0 \wedge f(B) = 1) \vee \varphi$

となります。

だから， $f(A) = 0 \wedge f(B) = 1$ が成り立つと仮定して $\neg \varphi$ がいえれば排中律が示せたことになります。

いま，もし $\varphi$ が成立するなら $A, B$ の定義から $A = B = \lbrace 0, 1 \rbrace$ となるので(外延性公理)， $f$ が写像であることから $f(A) = f(B)$ でなければなりません。しかし，そうすると仮定から $0 = 1$ となって矛盾します。よって $f(A) = 0 \wedge f(B) = 1$ のとき $\neg \varphi$ であることがわかりました。

ということで，選択公理(といくつかの集合論の公理)から排中律が証明できました。

排中律というのは構成的立場からは認められない公理ですから，選択公理を認めるということは何か構成的でないことを認めるということのはずです。一方で，選択公理は BHK interpretation の自然な帰結であるようにも思われることは既に述べた通りです。これはいったいどういうことでしょうか。

やっぱり選択関数は作れない

もう一度さっきの排中律の証明に戻って，何をしているかよく見てみましょう。

$A, B$ はさっきと同じとして， $\forall x \in X, \exists a, a \in x$ の証明をきちんと書いてみます。

まず $x \in X$ とすると， $X$ の定義から $x = A \vee x = B$ となります。

$x = A$ のとき，定義から $0 \in a$ です。また $x = B$ のときは $1 \in x$ です。

よって，いずれにしても $x$ の要素があることがいえたので， $\forall x \in X, \exists a, a \in x$ が証明できました。この証明は直観主義論理での証明になっています。

BHK interpretation によれば，この証明は $x$ が与えられると $x$ の要素を構成する手続きになっているはずですが，それは具体的にどんなものでしょうか。証明の道筋を追ってみると，

$f(x) = \left\lbrace \begin{array}{ll} 0 \qquad (x = A) \\ 1 \qquad (x = B) \end{array} \right.$

のようなものを構成していることがわかるでしょう。

これが選択関数になっているのでは……と一瞬思うかもしれませんが，そうではありません。これだと，関数として well-defined とは限りません。 $A$ と $B$ に対して異なる値を返していますが，もしかしたら $A = B$ かもしれず，その場合は同じ結果を返さないといけないからです。

思うにここがポイントなのです。もしかしたら $A = B$ かもしれない。古典論理においては「もし $A = B$ だったら常に 0 を返し，そうでなければ上のようにする」という定義ができて，それで選択関数の存在がいえたことになるのですが，排中律がなければそのような場合分けはできず，選択関数が作れないのです。*2

今の議論からわかることは，選択公理が直観主義となじまない理由は，選択する手続きを与えることはできてもそれが関数になるかどうかがわからないからだ，ということです。手続きへの入力が等しくても，出力が等しいとは限らないからです。

ちょっと話が逸れますが，おもしろいことに，これはよく言われる選択公理の非構成的側面とは異なっています。一般に言われるのは，有限個の集合から要素を一つずつ選ぶのは有限だからできるが，無限個の集合から選ぶことは一般にはできそうにない，ということです。ところがいまここで見てきたことからすると，無限個の場合だけではなくて，有限個の集合からであってもちょうど一つずつ選ぶことは構成的にはできないのです。要素を取り出す手続きを与えようとしても，同じ集合から二つ以上取り出してしまうことがないという保証ができないからです。上でやった排中律の証明にもそういう事情が現れています。無限集合は出てきませんが，選択関数が関数であることを使っています。

多価選択関数

ところで，写像にはならないけれど $x$ から $y$ を計算する手続きは存在する，という主張は，多価でもよいなら選択関数が存在する，と言い換えることができます。

いま， $\forall x \in X \exists y \in Y \varphi(x, y)$ が成り立つとき， $\varphi$ の多価選択関数(一般的な用語ではありません)とは $X$ から $P(Y) \setminus \lbrace \emptyset \rbrace$ (空でない $Y$ の部分集合全体) への写像 $f$ で次を満たすものとします。

$\forall x \in X \forall y \in f(x) \varphi(x, y)$

(書き方が普通の集合論の選択公理と違いますが，だいたい同じと思って大目に見てください)

多価選択関数の存在をいうだけなら内包公理を使えばほぼ自明ですが，単に存在するだけではなくて，選択関数が計算可能であることまでいえる，ということがここでの主張です*3。例えば上に出てきた $\lbrace A, B \rbrace$ 上の(多価かもしれない)選択関数ですが，これは既に述べたような手続きで計算することができるので計算可能です。

一般に， $\forall x \in X \forall y \in Y. \varphi(x, y)$ が直観主義論理で証明できるならば，計算可能な多価選択関数が存在するということがいえます。これはかなり雑な表現で，定理の正確な主張を述べるにはいくつか準備が必要ですが，詳しいことは最初に挙げた講義ノートに書いてあります。主張は p. 22, Proposition 4.30 に載っています。

BHK interpretation が選択公理を導きそうだと思われたことの正確な定式化のひとつがこれだ，とも考えられるでしょう。

*1:説明を書こうとしたらうまくいかなくてこの記事の公開が滞りました

*2:ちなみに最初に排中律を導いたときにやったことはこの話を逆にたどったような形になっています。つまり，もし選択関数があるなら A = B かどうかが選択関数の値からわかってしまい，結果として排中律が導かれる，という議論でした。

*3:多価関数 f が計算可能とは，各入力(の名前) x に対して f(x) のある要素(の名前)を返す手続きが存在すること