Answer by none for Consistency strength needed for applied mathematics

2011-02-09T19:33:08Z

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

User none - MathOverflow

Answer by none for Consistency strength needed for applied mathematics