Actually, in NBG you have explicitness of assumptions and of first-order logic β and at the same time axiom of induction is a single axiom.
Actually, if you care about cardinality, you need a well-specified set theory more than just axioms of reals. Second-order theory has a unique model, yes, but it has the notion of βallβ subsets, so it just smuggles some set theory without specifying it. As I understand, this was the motivation for Henkin semantics.
And if you look for a set theory (explicit or implicit) for reals as used in physics, I am not even sur you want ZFC. For example, Solovay has shown that you can use a set theory where all sets of reals are measurable without much risk of contradictions. After all, unlimited axiom of choice is not that natural for physical intuition.
Actually, in NBG you have explicitness of assumptions and of first-order logic β and at the same time axiom of induction is a single axiom.
Actually, if you care about cardinality, you need a well-specified set theory more than just axioms of reals. Second-order theory has a unique model, yes, but it has the notion of βallβ subsets, so it just smuggles some set theory without specifying it. As I understand, this was the motivation for Henkin semantics.
And if you look for a set theory (explicit or implicit) for reals as used in physics, I am not even sur you want ZFC. For example, Solovay has shown that you can use a set theory where all sets of reals are measurable without much risk of contradictions. After all, unlimited axiom of choice is not that natural for physical intuition.