もう一つ質問なんですが、基礎論を深くはやっていないからこそ抱いてる疑問です。

選択公理は全然自明じゃないから選択公理がないZFでどの程度の証明が出来るかに関心を持つのはごく普通だと思います
でも基礎論の議論(テキスト)でZFC^-という記述でZFCから巾集合公理を除いた物を意味させることがありますが、
巾集合公理はどっからどう見ても自明な公理なのに何でこんな公理を抜いた体型を考えるんですか？
どうせ公理を抜いた体系を考えるなら、正則性公理や置換公理を抜いた体系の方がまだいいような気がド素人には思えてしまいます。