When we say, "ZFC can found most of mathematics," what do we really mean?

Question

ZFC works as a foundation because it can prove many sentences that are "translations" of theorems from "standard" mathematics into the language of ZFC.

But there's a subtlety. When we say, "ZFC can found most of mathematics," what do we really mean?

Do we mean

1. ZFC proves most theorems (suitably translated into the language of sets) in the mathematics literature
2. A metatheory that makes sense of "consistency" + the assumption that ZFC is consistent can be used to prove most theorems (suitably translated into the language of sets) in the mathematics literature
3. A metatheory that makes sense of "models" + the assumption that ZFC has a model can be used to prove most theorems (suitably translated into the language of sets) in the mathematics literature
4. A metatheory that makes sense of "models" + the assumption that ZFC has a standard model can be used to prove most theorems (suitably translated into the language of sets) in the mathematics literature
5. Something else?

Answer 1

We mean that we can formalize the needed languages, and theories, and we can prove the existence of sufficient models for "regular mathematics" from ZFC.

This means that within any model of ZFC we can show that there are sets which we can interpret as the sets for "regular mathematics". Sets like the real numbers with their order, addition, and so on. And all the statements that you have learned in calculus about the real numbers and continuous functions, and so on -- all these can be made into sets which represent them and we can write proofs (which are other sets) and prove that these proofs are valid, and so on. All this within sets, using nothing but $\in$.

The key issue is that all this happens internally, so it happens within every model of ZFC, or rather in every universe (even if it is not assumed to be a set in a larger universe on its own).

Answer 2

I don't think it has anything to do with models of ZFC, so I'd say (1) is the closest. Of course it's not the sheer number of statements ZFC proves that is important, it's the fact that among those statements one can find, for almost any mathematical theorem, a formal theorem of ZFC that captures the meaning of that theorem (albeit in a very pedantic way.)

The main exception to this is theorems of set theory itself, which may require something like ZFC + large cardinal axioms to prove.

Answer 3

Only (1). Unformalized mathematics does not refer to its own consistency or existence of its own models, and its translation into a system like ZFC would not, either.