実用上数学ができるために「公理」は何なのか

多くの数学者は、別に公理的集合論や数理論理学の原理まで遡って数学をやっているわけではない
ということは、ある程度の厳密性を犠牲にしても、「これを認めれば実用上十分に数学ができる」という概念の集まりがあるはず
それは一体何なのか

>>14

とりあえず選択公理は必要(>>12)
空集合が扱えないと問題外なので、空集合の公理も必要
和集合とベキ集合が扱えないと問題外なので、和集合の公理とベキ集合の公理も必要
置換公理がないとロクな集合が作れないので、置換公理も必要
外延性公理がないと集合の等しさに関する議論が崩壊する(異なる表現方法で記述した本質的に同一の集合が
実際に等しいことが証明できなくなる)ので、外延性公理も必要
対の公理がないと {x,y} という2元からなる集合が扱えず問題外なので、対の公理も必要

無限公理の必要性は微妙だが、どのみち自然数がないと困るので、無限公理に近しい公理は必須
正則性公理は通常の数学では必要ないと思う

このように、実用上数学に必要な公理を並べてみたら、ZFCと大差ない
「じゃあお前は全て∅から構成してろよ」じゃないんだよ
実際に1つ1つの公理を精査したら「必要」なんだから。

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

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

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

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

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