>>15
＞証明の効率の点では、最初から集合や実数の概念を認めるのと、ZFCまで遡るのとでは雲泥の差

効率の観点から言えば、現時点で定理として認められている
全ての定理を公理として採用すれば、それらの定理の証明コストはゼロだよ

「そこまで大きな公理系ではなく、ある程度の無駄はそぎ落としたい」

ということなら、極限まで無駄をそぎ落としたものが ZFC もしくは ZF になるので、
無駄を許容した公理系でも「ZF＋余計な公理」という形にしかならない

つまり、どうやってもZFは必須で、これに>>12(選択公理)を加味すると
「ZFCまでは必須」となってしまう。まあ正則性公理あたりは微妙なので、
「ZFCから正則性公理を抜いたもの」あたりが回答ということになり、
結局ZFCと大差ないよねっていう