>>402
>　選択公理は代表の一意的な選択を可能としない
>→代表選択関数を１つ決めれば、述語論理の存在消去の推論が使えるのでアウト

これ、面白いし ”箱入り無数目”の理解にも繋がるから
少し掘り下げておく

”選択公理は代表の一意的な選択を可能としない”
で、以下背理法による
まず”選択公理は代表の一意的な選択は常に可能”と仮定する

反例を一つ示せば良い
下記のヴィタリ集合の構成が 反例になる

ヴィタリ集合 ja.wikipedia.org/wiki/%E3%83%B4%E3%82%A3%E3%82%BF%E3%83%AA%E9%9B%86%E5%90%88
で、”構成と証明”より
『有理数体 Q は実数体 R の普通の加法についての部分群を成す。なので加法の商群 R/Q (つまり、有理数分の差を持つ実数同士を集めた同値類による剰余群) は有理数集合の互いに交わらない"平行移動コピー"によって出来ている。この群の任意の元はある r ∈ R についての Q + r として書ける。
　R/Q の元は R の分割の1ピースである。そのピースは不可算個あり、各ピースはそれぞれ R の中で稠密である。R/Q の元はどれも [0, 1] と交わっており、選択公理によって [0, 1] の部分集合で、R/Q の代表系になっているものが取れる。このようにして作られた集合がヴィタリ集合と呼ばれているものである。すなわち、ヴィタリ集合 V は [0, 1] の部分集合で、各 r ∈ R に対して v − r が有理数になるような一意的な v を要素に持つものである。ヴィタリ集合 V は不可算であり、
u,v∈V,u≠v であれば v − u は必ず無理数である』

さて
＜補足＞
1）商 R/Q の同値類の代表は、本来は R全体に広がっているものだ
2）それでは ”一意”に不都合なので 上記のように 区間[0, 1]に集約することは可能
3）しかし、区間[0, 1]に集約しても ”一意”な代表には ほど遠い
4）もっと ”一意”に近づけないか？
　しかし、それは無理。人は、具体的な 商 R/Qの代表を持たない
　例えば、円周率πと対数の底e で π-eや π+e が、有理数か無理数かさえ 現時点では不明（下記 超越数 ご参照）
　だから π-eや π+e が出てきたとき これらの数が 既に Qとして代表が取られているのか？
　はたまた 新しい R/Q の代表として 取り上げるべきかが いまの人類には判断できない
　もっといえば、π-eと π+e を 別の類別とすべきかも判断できない！
5）まとめると、”数学的”に規定可能な条件を 選択公理に加えることは可能（例えば 区間[0, 1]から代表を選べ）
　しかし、(今の)数学で規定不可能な条件を 選択公理に加えることは無理ですｗ
　つまり ヴィタリ集合 一次元空間で R/Q さえ 代表の”一意”化は無理！ｗｗ
　まして、無限次元空間 R^Nのしっぽ同値の代表の”一意”化は絶対無理！ｗｗｗ

(参考)
ja.wikipedia.org/wiki/%E8%B6%85%E8%B6%8A%E6%95%B0
超越数
超越数かどうかが未解決の例
e+π,e−π,eπ,・・ などの円周率 π やネイピア数 e の大抵の和、積、べき乗は、有理数であるのか無理数であるのか超越的であるのか否かは証明されていない