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?
 A: Edited 3/10/2017
Very large cardinals around the rank-into-rank area potentially have applications in cryptography. Rank-into-rank cardinals produce self-distributive algebras which may be used as platforms or to produce platforms for authentication schemes and key exchange protocols. Therefore, if these self-distributive algebras are seriously considered as platforms for new cryptosystems, then one will need all of the large cardinal hierarchy in order to research applied mathematics.
Recall that a rank-into-rank embedding is an elementary embedding $j:V_{\lambda}\rightarrow V_{\lambda}$. Let $\mathcal{E}_{\lambda}$ denote the collection of all rank-into-rank embeddings $j:V_{\lambda}\rightarrow V_{\lambda}$. Define a binary operation $*$ on $\mathcal{E}_{\lambda}$ by letting $j*k=\bigcup_{\alpha<\lambda}j(k|_{V_{\alpha}})$. Then $(\mathcal{E}_{\lambda},*)$ satisfies the self-distributivity identity $j*(k*l)=(j*k)*(j*l)$. If $\gamma$ is a limit ordinal with $\gamma<\lambda$, then define a congruence $\equiv^{\gamma}$ on $(\mathcal{E}_{\lambda},*)$ by letting
$j\equiv^{\gamma}k$ if and only if $j(x)\cap V_{\gamma}=k(x)\cap V_{\gamma}$ whenever $x\in V_{\gamma}$. Then my question and answer shows that the algebra $(\mathcal{E}_{\lambda}/\equiv^{\gamma},*)$ is locally finite and hence locally computable.
The non-abelian group based cryptosystems can generally be modified to produce cryptosystems that could use any left-distributive algebra as a platform. For example, in this paper, the authors have modified the Anshel-Anshel-Goldfeld key exchange to produce a cryptosystem that could use any left-distributive algebra as a platform. Furthermore, the Ko-Lee key exchange also could be modified to produce a cryptosystem for left-distributive algebras. In this paper, Using shifted conjugacy in braid-based cryptography, Dehornoy proposes an authentication scheme that can use any self-distributive algebra as a platform (though you need to tweak this cryptosystem if the self-distributive algebra is not left-cancellative) rather than just conjugacy on groups (Dehornoy had the platform shifted conjugacy on braid groups in mind, but this platform was later shown to be insecure).
Dehornoy in 4 remarks that the combinatorial complexity of the Laver tables and the fact that the classical Laver tables produce extremely fast growing functions suggests that the classical Laver tables or similar structures may be a good platform for his authentication scheme or some other cryptosystem. However, the classical Laver tables are currently a very insecure platform for all cryptosystems. First of all, $A_{48}$ is the largest classical Laver table which has even been computed. Therefore, the classical Laver table based cryptosystems only provide at most 48 bits of security. Furthermore, the homomorphisms between the classical Laver tables allow one to easily write computer programs that break all cryptosystems based on the classical Laver tables. My generalized Laver tables which you can compute online here are not a secure platform for self-distributive algebra based cryptosystems either since it is easy to factorize elements in generalized Laver tables. Fortunately, unless I have simply overlooked something, the ternary Laver tables so far appear to be plausible platforms for these self-distributive algebra based cryptosystems. Click here for a ternary Laver table calculator on my website.
Of course, it is way to soon to comment on the security or the insecurity of these ternary Laver table based cryptosystems, and much more research needs to be done on cryptography based on Laver-like algebra. These line of investigation have barely been researched, but I have recently proposed a polymath project to promote an investigation into these directions of inquiry.
A: 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
A: In the link below you can find something on the issue of the foundational framework consistency and applications of mathematics to an empirical science (economics) as well as a mention relating large cardinals and the cognitive abilities of economic agents.
http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.98.169&rep=rep1&type=pdf
A: 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.
A: 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.
A: To answer your question

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?

Solomon Feferman's article Why a little bit goes a long way: Logical foundations of scientifically applicable mathematics, in PSA 1992, Vol. II, 442-455, 1993. Reprinted as Chapter 14 in In the Light of Logic, 284-298.  ( http://math.stanford.edu/~feferman/papers/psa1992.pdf ) might be of interest.
