トップ «前の日記(2009-07-08) 最新 次の日記(2009-07-12)» 月表示 編集

日々の流転


2009-07-11 [長年日記]

λ. “100 years of Zermelo's axiom of choice: what was the problem with it?” by Per Martin-Löf

2004年にワークショップ「Types for Verification」で聴いたとき には断片的にしか理解できなかったので、ちゃんと読んでみた。

選択公理は非構成的だと非難されることがあったが、Brouwer-Heyting-Kolmogorov解釈(BHK解釈)的な観点からは
(∀i : I)(∃x : Si)A(i,x) → (∃f : Πi : ISi)(∀i : I)A(i,f(x))
という形の選択公理は完全に構成的*1(参考: Agda による選択公理の証明)。その一方で、(ある種の直観主義的集合論であるところの)トポスの理論では選択公理から排中律を導くことが出来る。その違いは何でどこに問題があるのか、という話。

ここではZermeloの選択公理の形式化のうち「集合Sの分割が与えられたときに、Sの部分集合S1で、分割の各部分A,B,C,…との共通部分が1要素になるようなものが存在する」を、集合を型理論での extentional set *2 とする解釈で解釈したものを考え、分析している。

前述の構成的な選択公理からZermeloの選択公理を証明することはできないが、これを拡張した外延的な選択公理
ExtAC = (∀i : I)(∃x : Si)A(i,x) → (∃f : Πi : ISi)(Ext(f) ∧ (∀i : I)A(i,f(x)))
where Ext(f) = (∀i,j : I)(i =I j → f(i) =S f(j))
からは証明可能で、さらに同値になる。

ただし、当然ながらExtACのうちの選択関数fがExt(f)を満たすという部分は実際には導くことが出来ない部分なわけで、こうして構成的な世界で考えてみると、Zermeloの選択公理の構成的でない部分というのは、「選択関数の存在」ではなく「選択関数の外延性」だったということがわかる。

関連

*1 何故ならば、集合が空でないことを証明することは、具体的な要素を選び出すことに等しいため。

*2 setoidという呼び方の方が一般的だと思うが