Consistency strength needed for applied mathematics

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?

-
I think you referring to reverse mathematics. This science investigates which axioms are required for a certain theorem. –  Lucas K. Feb 8 '11 at 22:22
An important question in this respect is 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
"Does anyone believe that the difference between the Lebesgue and Riemann integrals can have physical significance, and that whether say, an airplane would or would not fly could depend on this difference? If such were claimed, I should not care to fly in that plane." (Richard Hamming) –  Terry Tao Feb 9 '11 at 13:16

The research area known as Reverse Mathematics is concerned with finding out the weakest theory that suffices to prove a given mathematical statement over a very weak base theory. The project has now been successfully carried out for a huge proportion of the theorems of classical mathematics, many of which would seem to be central for any robust effort in applied mathematics. So it seems to me that the answer to your question is provided by the precise reverse mathematical strength of the principal classical theorems used in whatever branch of applied mathematics you have in mind, which I expect might include much of classical analysis and other areas.

There is a particularly good book on reverse mathematics by Stephen Simpson, and the topic has been mentioned several times here on MathOverflow.

One surprising outcome of the work is that numerous classical theorems have turned out to be equivalent to each other, grouped in a comparatively small number of equivalence classes. Follow the link above for information about the five principal theories.

-
Thanks for the reference to reverse mathematics. From a first glance at the theorems listed for each theory in the Wikipedia article, it is obvious that WKL0 is needed for applied mathematics, but for the stronger systems this is at least not obvious at first sight. So I could now reframe my question as follows: Are any theorems from the stronger Reverse Mathematics theories needed in applied mathematics? Is there any need to go beyond these five systems to something as strong as ZFC? Do the five theories of reverse mathematics have different consistency strengths? –  Marcos Cramer Feb 8 '11 at 23:24
The Wikipedia page says $ACA_0$ is necessary for some results in analysis including Bolzano-Weierstrass and Arzela-Ascoli. Can you really do applied mathematics without these? –  Tom Ellis Feb 9 '11 at 9:59
It seems unlikely to me that what people usually call "applied mathematics" will require more than ACAo. The proof theoretic ordinal of that theory is the same as Peano arithmetic, and so is not particularly "large" in the realm of proof theoretic ordinals. –  Carl Mummert Feb 9 '11 at 23:09
@Marcos: To your last question, see en.wikipedia.org/wiki/Ordinal_analysis for precise strengths of these five systems, and others. The first two theories, $RCA_0$ and $WKL_0$, have the same strength, namely $\omega^\omega$, and then $ACA_0$ is somewhat higher at $\epsilon_0$. And like Carl says it's unlikely you'll find anything physically applicable going beyond that. –  Daniel Mehkeri Feb 10 '11 at 3:23

It seems like your interest is mainly in the philosophical side of your question, so I'd like to address that directly, although I'm not even close to being a philosopher of mathematics.

It is not strictly true that an empiricist viewpoint can only justify the consistency strength needed for immediate application. The empiricist argument that you give in your question for believing mathematics sounds a lot like Quine. Quine like you, argued for accepting the validity of (some) mathematics because of the utility of mathematics in the sciences. Other mathematics he did not accept because he could not think of scientific applications. For example, Quine advocated consistent use of the axiom of constructibility ($V=L$) throughout mathematics because he thought that doing so would suffice for the purposes of applied mathematics.

The problem with this viewpoint is that it draws a ragged edge through the heart of mathematics, denying the validity of important work that often motivates and interconnects with mathematics on the other (justifiable to Quine) side of the barrier. (For example, there is an MO question that I can't find right now about theorems that were first proved using the axiom of choice, and later proved with weaker hypotheses; similar examples exist of theorems first proved using large cardinal axioms, and later shown to follow from ZFC alone.)

It is possible to be an empiricist and also accept the validity of the entire mathematical enterprise. A strong proponent of such a view is Penelope Maddy. I particularly recommend her book Second Philosophy in this context. Her arguments are delicate, so I will avoid trying to summarize them. However, like Quine, she accepts the validity of some mathematics because of its importance in applications, while, unlike Quine, she accepts the rest of mathematics because of the inherent unity of mathematics and the unreasonability of any cutting of mathematics into philosophically justified and unjustified pieces.

-

Actually thinking about this further, "applied mathematics" has traditionally meant differential equations, as used in (say) mechanical engineering or aeronautics. But going just by deployment in real-world applications, of course it can include a lot of algebra and logic (think of group theory in crystallography, or model checking in computer hardware verification).

In particular, formal theorem checkers (proof assistants) are used in hardware and software verification, such as in checking CPU designs for correct arithmetic since the famous Pentium FDIV bug. HOL Light is an example of such a verification program. You write your program in the form of a proof, and HOL Light checks the proof. But HOL Light is itself a complicated program, subject to having bugs and inconsistency, so you really want a proof of correctness of the proof checker and for the consistency of its underlying logic (i.e. that it will never accept a proof of "false") before you can rely on it. By Gödel's second incompleteness theorem HOL Light cannot prove its own consistency: you have to use a version augmented with an additional axiom to prove the consistency of the unaugmented version.

The additional axiom used is "there exists an inaccessible cardinal K". Then of course $V_K$ is a model of the theory and the verifier can check this.

So there, then, is a use of large cardinals in applied mathematics.

I think I've seen some other descriptions of the above, and something like it for Coq. I'm having trouble finding much, but there's at least a mention of the issue here: http://www.cs.ru.nl/~freek/notes/pcpc.pdf

-
Nice one. However you then need an even larger cardinal to show that it is consistent to assume the existence of an inaccessible cardinal... This is where my original concern comes back, and with it the possibility to found mathematics empirically. If HOL Light does not have a larger consistency strength then that needed for applied mathematics (now refraining to include a consistency proof of HOL Light into applied mathematics), then HOL Light can be justified on empirical grounds, and you don't need a proof of its consistency. Hence the inaccessible cardinal is not needed in applied math. –  Marcos Cramer Feb 10 '11 at 10:59