Choice Principle と選択公理 - 論理とか計算機とか数学とか

「構成的プログラミングの基礎」という本を読んでいたら choice principle のことが書いてあって，この間書いた直観主義と選択公理のことと一見噛み合わない内容だったので，どういうことか考えてみた話を。

Choice Principle

次の公理のことを choice principle 略して CP と呼びます。

$\forall x. \exists y. A(x, y) \to \exists f. \forall x. \exists y. (f(x) = y \wedge A(x, y)$

考えている論理が何かを指定していませんが，「構成的プログラミングの基礎」では型なしλ項を項とする述語論理で考えていました。以下でも型なしλ計算(に定数を追加したもの)を考えます。(ペアノ算術みたいに関数が表現できる体系だったら同じような話ができそうな気はしますが)

また realizability interpretation を，λ式を realizer として自然に与えることにします。

CP is realizable

まず，CP は realizer をもつことが示せます。具体的に書くと

$\lambda r.\langle \lambda x.\pi_1(r(x)), \lambda x. \langle \pi_1(r(x)), \langle 0, \pi_2(r(x))\rangle \rangle$

が realizer になることが確かめられます。 $\langle\rangle, \pi_1, \pi_2$ は対と射影，0 は自然数の 0 です(この部分は等式の realizer を書けばよいので，0 でなくても何でもかまわないのですが)。

簡単に説明すると， $r$ が $\forall x. \exists y. A(x, y)$ の realizer， $\lambda x. \pi_1(r(x))$ が $f$ に入るべき関数で，その後ろの部分が $\forall x. \exists y. (f(x) = y \wedge A(x, y)$ の realizer になります。

だから $\forall x. \exists y. A(x, y)$ の realizer $r$ があれば，選択関数が具体的に $\lambda x.\pi_1(r(x))$ として得られます。

CP と排中律は矛盾する

次に，CP と排中律を仮定すると矛盾が導けることが証明されています。

$A(x, y) \equiv (y = \top \wedge x(x) \downarrow) \vee (y = \bot \wedge x(x) \uparrow)$

を考えます。ただし $\top, \bot$ はそれぞれ真と偽を表すブール値， $\downarrow$ は値が存在する(簡約が停止する)こと， $\uparrow$ は値が存在しないことを表す述語です。

排中律から $A(x, y)$ が成立することは明らかなので，CP によってある $f$ があって $\forall x. A(x, f(x))$ が真になります。

いま， $g = \lambda x. (f(x) \to \Omega; 0)$ とおきます。ここで右辺の括弧内は "if $f(x)$ then $\Omega$ else $0$ " を表します。 $A(g, f(g))$ が成り立つことと $A$ の定義より

$(f(g) = \top \wedge g(g) \downarrow) \vee (f(g) = \bot \wedge g(g) \uparrow)$

が成立します。ところが $g$ の定義から $g(g) = f(g) \to \Omega; 0$ なので $f(g) = \top \wedge g(g) \downarrow$ のときは

$f(g) = \top \wedge g(g) \downarrow$

$\Longrightarrow f(g) = \top \wedge (f(g) \to \Omega; 0) \downarrow$

$\Longrightarrow (\top \to \Omega; 0) \downarrow$

$\Longrightarrow \Omega \downarrow$

となって矛盾です。同様に $f(g) = \bot \wedge g(g) \uparrow$ のときも $0 \uparrow$ となって矛盾が導かれます。

これで CP と排中律が両立しないことがわかりました。

何が問題なのか

それで，この議論のどこが疑問だったかというと，

選択関数は必ずしも構成的には作れないはずだったが，CP はどうして realizable なのか (realizer があれば選択関数が取り出せるのでは?)
選択公理と排中律は矛盾しないのに，CP と排中律が矛盾するのはなぜか

の二点です。選択公理と CP はよく似たことを主張しているのに，どうしてこんなに違う結果が出るのか，結論だけ見るとかなり不思議な気がしました。

とりあえず考えてみた

最初の疑問については，そんなにはっきりした答えが出せていないのですが，選択関数が作れないのが等しさを保つように作れないからだったことを考えると，realizer から取り出せる「選択関数」も等しさを保たないのではないかと推測できます。ただし問題になるのは，この場合の「等しさ」とは何かということです。例えばβ同値なんかを考えた場合には保存されるはずです。realizer から取り出せる関数はλ式だからです。そういうλ計算の中に自然に存在する等しさではなくて，もっと非自明な等しさを考えたときには保存されないということなのでは，と思います。

例えば，集合を(λ式でエンコードして)扱う場合を考えるとどうでしょうか。集合の間には外延性の公理という形で非自明な等しさが入っています。選択公理から排中律を導く際にも外延性公理が使われていましたし，こういう種類の等しさだったら保存しないのかもしれません。λ計算の中で集合論がどのくらい書けるか知らないしすぐにはわからないのですが，外延性公理のようにλ計算の外から持ち込まれたような等しさの概念が存在する際には，その意味での等しさは保存しない realizer になっているということなんじゃないかと(何らかの形で検証したわけではありませんが)思いました。

二つ目の疑問については，CP の主張をよく見るとわかります。関数 $f$ が存在する，と言っていますが，どこに存在するのでしょうか。ここでは，λ式を対象とする論理を考えているので，この存在は「λ式として存在する」(別の言い方をするとλ定義可能である)という意味のはずです。そうすると，その関数は必然的に計算可能です。一方，普通の選択公理の場合には，そんなことはありません。選択関数が計算可能でない場合もたくさんあります。ここが大きな違いなのでしょう(公理としてというより，そもそも考えている体系が両者で異なると考えたほうがよいのかもしれません)。

上の証明もそこの違いを利用しています。λ式で書けない(計算不可能な)選択関数しかないような $A$ を持ってくることで CP から矛盾を出しているわけです。上で与えた $A(x, y)$ の中身は，要するに「 $y$ の値が $x$ の停止性の真偽に一致する」であり，これは決定不能ですから構成的には証明できないのですが，一方で非構成的には排中律から導けます。CP によるとここから停止性の決定手続きが出てくるので矛盾する，というわけです。

テキストには，「CP は選択公理よりは Church's thesis に近い」という意味のことが書いてありましたが，ここまで考えてその意味がなんとなくわかってくるような気がしました。