# 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
• You say "T" in an applied context and I say "ZFC proves T", reducing the consistency strength "needed" for my statement to well below PA. Why would you need more? – Matt F. Aug 16 '16 at 1:41

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.

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.

• Very interesting paper which indeed does provide a partial answer to my questions. Thanks! – Marcos Cramer Feb 9 '11 at 14:05

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.

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

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