Given that we can never proof the consistency of a theory for the foundations of mathematics in a weaker system, one could seriously doubt whether any of the commonly used foundational frameworks (ZFC or other axiomatisations of set theory, second-order PA, type theory) is actually consistent (and hence true of some domain of objects). One of the ways to justify a certain framework for the foundations of mathematics is by adopting an empiricist stance in the philosophy of mathematics and argue that mathematics must be right because it correctly explains natural phenomena that we observe (i.e. is needed in empirical sciences), and that hence some foundational framework unifying our mathematical knowledge is justified.

Now different foundational frameworks have different consistency strengths. For example, ZFC with some large cardinal axiom (which one might want to accept in order to do category theory more comfortably) has a greater consistency strength than just ZFC. The above justification would only justify a foundational framework of a given consistency strength if that consistency strength is needed for some application of mathematics to empirical sciences.

Have there been any investigations into the question which consistency strength in the foundational framework is needed for applied mathematics? Is there any application of mathematics to empirical sciences which requires a large cardinal? Is maybe something of consistency strength weaker than ZFC enough for applied mathematics? Have any philosophers of mathematics asked questions like these before?

Is the axiom of choice relevant for applications of mathematics to empirical sciences ?It is often used, through theorems of Functional Analysis, but thus might be due to our lazyness. – Denis Serre Feb 9 '11 at 7:16