>>491-492
>だいたい、a = { x | 1=1 }が集合なら、分出して b = { x ∈ a | x ∉ x } も集合なんだから結局矛盾するだろ

なんだ、それ言いたかったの？
命題：P→Q
P：a = { x | 1=1 }が集合
Q：直観主義ではラッセルのパラドックスが起きて、結局矛盾する
かな？

さて、仮定”P：a = { x | 1=1 }が集合”が真ならば、P→Qが導けて”命題：P→Q”真？って、証明としてどうか？
そも、仮定”P：a = { x | 1=1 }が集合”が真の証明がない
つまり、「”P：a = { x | 1=1 }が集合”が偽」で、「命題：P→Qが真」と主張しても、全く面白くない

例えば、
P：私が数学の神なら Q：数学フィールズ賞が取れる 「命題：P→Qが真」
P：宝くじ当たったら Q：大金持ちになれる 「命題：P→Qが真」
（仮定Pが偽なら”命題：P→Q”は常に真）

仮定Pにデタラメ書いて
Q：直観主義ではラッセルのパラドックスが起きて、結局矛盾する という

直観主義が、分かってない？
直観主義は、下記でもどぞ

(参考)
https://lkozima.はてなブログ.com/entry/2013/01/04/231525
論理とか計算機とか数学とか lkozima
2013-01-04
直観主義と選択公理の話
下記の講義ノートを読んでいたら選択公理のことが書いてあって，それがおもしろかったのでこの記事を書こうとしています。

http://math.andrej.com/2005/08/23/realizability-as-the-connection-between-computable-and-constructive-mathematics/

直観主義と選択公理の関係って相性がよさそうな悪そうなよくわからないものなのですが，そのあたりの事情がちょっと整理できました。

BHK interpretation と選択公理
BHK (Brower-Heyting-Kolmogorov) interpretation というものがあります (http://en.wikipedia.org/wiki/Brouwer%E2%80%93Heyting%E2%80%93Kolmogorov_interpretation)。大雑把にいうと，証明とはその具体的証拠の構成のことである，というような立場から論理式あるいは数学的主張の意味を解釈することだとぼくは思っていますが，BHK interpretation を解説する記事ではないので詳しい説明は省きます。*1

選択公理 ⇒ 排中律
実は，集合論のいくつかの公理と選択公理を認めると排中律が証明できます。

やってみましょう。(http://plato.stanford.edu/entries/axiom-choice/#AxiChoLog にあるのと同じ方針です)

ということで，選択公理(といくつかの集合論の公理)から排中律が証明できました。

排中律というのは構成的立場からは認められない公理ですから，選択公理を認めるということは何か構成的でないことを認めるということのはずです。一方で，選択公理は BHK interpretation の自然な帰結であるようにも思われることは既に述べた通りです。これはいったいどういうことでしょうか。

やっぱり選択関数は作れない