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の選択公理の構成的でない部分というのは、「選択関数の存在」ではなく「選択関数の外延性」だったということがわかる。
