Extensional axiom of choice という公理があるらしい

二年前に 直観主義と選択公理の話 という記事を書いたのですが,それに近い内容の論文を 2006 年に Martin-Löf が書いていたこと知りました。"100 Years of Zermelo’s Axiom of Choice: What was the Problem with It?" というタイトルの論文で,Springer から出版されています (http://link.springer.com/chapter/10.1007%2F978-1-4020-8926-8_10) が,同じ内容と思われる(確認してないけど) pdf が https://people.kth.se/~kurlberg/colloquium/2005/MartinLooef.pdf で公開されています。

この論文は,どうして選択公理は BHK 解釈のもとでは自然に成立するように思えるのに排中律を導くという非構成的性質を持つのか,ということを論じたもので,結論は「関数の存在はいえても,その外延性が保証できない,つまり等しい値に対して等しい結果を返すことが証明できないから」ということで上記の記事と一致しているようです。

Extensional axiom of choice

その論文中で導入されている extensional axiom of choice (ExtAC) という公理が面白かったので,それについて議論されていることをまとめておきます。技術的詳細には立ち入りません,というか以下の議論が正確にはどう形式化できるのかよく理解できてない部分があります。しかし詳細がわからなくても informal な説明としてはそれらしいものであると思います。

ExtAC は,普通の集合論の中ではただの AC と区別がつかないのですが,構成的型理論 (CTT) の中で考えると AC と同値ではない公理です。この ExtAC と AC の差を観察することで選択公理が成り立つ集合論が非構成的になる理由がわかる,という点が面白いところです。

ExtAC を考えるための前提として,型における等しさの概念は型そのものの定義とは別に与えられると考えることに注意が必要です。CIC のように inductive type をもつ型理論では identity type は一様に定義できますし,Martin-Löf 流の型理論でも同様のやり方で導入することができますが(propositional equality と呼んだりする),それとは別に等しさを考えるということです。別の言い方をすると,ただの型ではなく setoid を考えるということです。

いま I と S を型とし,その上の等しさが与えられたとして,それらを各々  =_I,  =_S と書くことにしましょう。これらの等号については,それぞれ I と S の上の同値関係であることしか仮定しません。また,以下 A は  I \times S 上の述語でこれらの等号を respect する(つまり  i =_I j かつ  x =_S y なら  A(i, x) \leftrightarrow A(j, y) である)ものとします。

まず,通常の選択公理 AC は

 \forall (i : I) \exists (x : S) A(i, x) \rightarrow (\exists f:  I \to S)(\forall i : I) A(i, f(i))*1

となります。これは等しさに言及しないバージョンで,この形のものは CTT で証明できるのでした。ただし, i =_I j だからといって  f(i) =_S f(j) かどうかはわからないことに注意しましょう。等号は任意に与えた同値関係としたのだから,確かに CTT における AC の証明はこれを満たす f を与えるとは限らないでしょう。

ExtAC は以下のように定式化されます。

 \forall (i : I) \exists (x : S) A(i, x) \rightarrow (\exists f:  I \to S)(\mathrm{Ext}(f) \wedge (\forall i : I) A(i, f(i)))

ただし Ext(f) は f が外延的であることを表す述語で,次のように定義されます。

 \mathrm{Ext}(f) = (\forall i, j : I) (i =_I j \to f(i) =_ S f(j))

また,正確には一番外側に  =_I, =_S を束縛する全称量化子(とそれらに関する諸々の条件)が付くと思いますが省略しています。

AC と違って,ExtAC は CTT では証明できません。論文中では,実は ZFC から CTT + ExtAC への翻訳が存在することが示されています("ZFC is interpretable in CTT + ExtAC" と書いてありますが,そういうことでしょう)。ということは,ラフな言い方をすると,集合論的な意味での AC に相当する型理論の公理は AC ではなく ExtAC であることがわかります。

証明の詳細をきちんと確かめていないのですが,だいたいどういうことかというと,集合論では集合の商をとることができるのがポイントになっているようです。このことは,与えられた同値関係の意味での同値性を,集合としての等しさに置き換えることができるということを意味します。もし述語 A が与えられた同値関係を保てば,A は商集合の上の述語としても well-defined ですから,先に商をとったうえで AC を使うことで ExtAC 相当のことができるのでしょう。

補足しておくと,通常の集合論においては等しさの概念は論理に組み込まれているものを使いますから,どんな関数も等しさを保存するということは集合論がその上に乗っているところの一階述語論理のレベルで保証されています。したがって,そもそも外延的でない関数など存在するはずがないので,Ext(f) は恒真であり,そのような述語は何を言っていないのと同じです。だから当然,ExtAC 相当のものを集合論で考えても,それはただの AC と同値です。したがって両者は集合論においては区別できません。

このように AC と ExtAC を区別したうえで議論をすると,集合論において選択公理がどのようにして構成的でない結論を導いているのかが見えやすくなります。両者の差は Ext(f) を要求するかどうかにあるわけだから,その違いが効いているということです。つまり Ext(f) を満たすような f を構成的に与えることはできないのです。これで最初に述べたように,選択関数が作れないのは選択できないからではなく外延性が保証できないからである,という結論に到達しました。

二年前の記事では同じ事情を「多価でもよいなら選択関数は存在する」という形で表現したのですが,今回紹介した Martin-Löf の議論はその別表現と言うことができるでしょう。

*1:ここでは量化子は他の結合子よりも強く結合することにします