- 472 名前：１３２人目の素数さん mailto:sage [2005/05/28(土) 20:33:23 ]
- >>470
ずっと前からそう思ってたんだけど最近になって必ずしも構成的ではないんじゃないかと思い始めた。
集合族 {A_i} について ∀i∃x(x∈A_i) が証明できたとしても、
それは i が一つ与えられれば A_i の要素を取り出せるということでしかない。
その要素の構成は i の表し方に依存しないとは限らない。
だとすれば ∀i∃x(x∈A_i) の証明から構成される選択関数は、
普通にいう関数(つまり外延的関数)には必ずしもならなくて、
i=j であっても f(i)=f(j) だとは限らないような関数になるのでは？
というのがその理由なんですが。
ところでこれ、等号の公理のことと関連してますね。書いてから気付いたんですが。
