スレ主です
落ちこぼれの基礎論くんへの選択公理の講義追加

「具体的」>>141という幼稚な用語を使う君へ
基礎論の公理系では、「構成的」という用語が適切だろう（下記）

そして
・選択公理の必要性は、集合族が有限か、可算か、非可算かで分かれる
・また、下記”Martin-Löf 型理論と高次のHeyting 算術”では、選択公理では別の手段で実現できるとある

「具体的」？ アホや

https://en.wikipedia.org/wiki/Axiom_of_choice
Axiom of choice
In constructive mathematics
(google訳(抜粋))
構成的数学において
上で説明したように、ZFC では、選択公理は、明示的な例が構築されていないにもかかわらず、オブジェクトの存在が証明される「非構築的な証明」を提供できます。ただし、ZFC はまだ古典論理で形式化されています。選択公理は、非古典的論理が使用される構成数学の文脈でも徹底的に研究されています。選択公理のステータスは、構成数学の種類によって異なります。

Martin-Löf 型理論と高次のHeyting 算術では、選択公理の適切なステートメントは (アプローチに応じて) 公理として含まれるか、定理として証明可能です。[11]

構成的集合論では、ディアコネスクの定理は、選択公理が排中律を暗示していることを示しています（マルティン・レフ型理論ではそうではありませんが）。したがって、選択公理は一般に構成的集合論では利用できません。この違いの原因は、型理論の選択公理が、構成的集合論の選択公理が持つような拡張性の特性を持たないことです。[13]

構成的集合論の一部の結果では、可算選択の公理や従属選択の公理が使用されていますが、これらは構成的集合論における排中律を意味しません。特に可算選択の公理は構成数学で一般的に使用されますが、その使用法にも疑問があります。[14]