What is Realistic Mathematics?

When Solovay showed that ZF + DC + "all sets of reals are Lebesgue measurable" is consistent (assuming ZFC + "there is an inaccessible cardinal" is consistent), there was an expectation among set-theorists that analysts (and others doing what you call realistic mathematics) would adopt ZF + DC + "all sets of reals are Lebesgue measurable" as their preferred foundational framework. There would be no more worries about "pathological" phenomena (like the Banach-Tarski paradox), no more tedious verification that some function is measurable in order to apply Fubini's theorem, and no more of various other headaches. But that expectation wasn't realized at all; analysts still work in ZFC. Why? I don't know, but I can imagine three reasons.

First, the axiom of choice is clearly true for the (nowadays) intended meaning of "set". Solovay's model consists of certain "definable" sets. Although there's considerable flexibility in this sort of definability (e.g., any countable sequence of ordinal numbers can be used as a parameter in such a definition), it's still not quite so natural as the general notion of "arbitrary set." So by adopting the new framework, people would be committing themselves to a limited notion of set, and that might well produce some discomfort.

Second, it's important that Solovay's theory, though it doesn't include the full axiom of choice, does include the axiom of dependent choice (DC). Much of (non-pathological) analysis relies on DC or at least on the (weaker) axiom of countable choice. (For example, countable additivity of Lebesgue measure is not provable in ZF alone.) So to work in Solovay's theory, one would have to keep in mind the distinction between "good" uses of choice (countable choice or DC) and "bad" uses (of the sort involved in the construction of Vitali sets or the Banach-Tarski paradox). The distinction is quite clear to set-theorists but analysts might not want to get near such subtleties.

Third, in ZF + DC + "all sets of reals are Lebesgue measurable," one lacks some theorems that analysts like, for example Tychonoff's theorem (even for compact Hausdorff spaces, where it's weaker than full choice). I suspect (though I haven't actually studied this) that the particular uses of Tychonoff's theorem needed in "realistic mathematics" may well be provable in ZF + DC + "all sets of reals are Lebesgue measurable" (or even in just ZF + DC). But again, analysts may feel uncomfortable with the need to distinguish the "available" cases of Tychonoff's theorem from the more general cases.

The bottom line here seems to be that there's a reasonable way to do realistic mathematics without the axiom of choice, but adopting it would require some work, and people have generally not been willing to do that work.

I think you need to be clearer about how directly useful you need your mathematical concepts to be to the study of the real world. For example, suppose you find PDEs useful for modelling physical phenomena, certain concrete Banach spaces useful for studying PDEs, and the abstract theory of Banach spaces useful for understanding the concrete ones, then you'll have to allow the Hahn-Banach theorem, since that is undeniably useful in the abstract theory of Banach spaces. The Hahn-Banach theorem is slightly weaker than the axiom of choice, but the usual proof of it uses the axiom of choice. Does that make the axiom of choice realistic after all?

In the other direction, one might say that even very large positive integers are not realistic. For example, the number 123871205412470874297947938271423698765734564756028492656 has no direct role to play in physics.

For this kind of reason, I think it may be very hard to come up with a precise characterization of realistic mathematics, but I'd be interested to see some attempts.

At the other side, existence of large cardinals, non-measurable subsets of the reals, etc. are not (immediately) useful for such a study.

I don't know about non-measurable subsets, but large cardinals are definitely useful for ordinary applied mathematics of the kind I do (theoretical computer science). The reason is twofold.

First, I design programming languages, and modern programming languages are type theories -- so assertions about whether all programs in a given language are total or not can boil down to assertions about the existence of large cardinals. Meta-mathematically, this is a trivial point, but often people don't immediately see that large cardinals amount to facts about the termination of computer programs.

Secondly, we need things like functor categories to organize the semantics of programming languages, which call for (weak) large cardinal axioms. Here's a simple example.

In a language like Java, the execution of a program can create objects which live in the computer's memory. However, even though the concrete memory is addressed by integers, Java only lets you test whether two objects are equal or not, and doesn't let you compare objects for their relative position in the address space. So, when you give a semantics to such a language, we want to ensure that the meaning of a program is invariant under permutations of the address space (ie, you can move objects around, without changing the observable behavior of the program).

One approach to this problem (invented by Stark and Pitts) is to give semantics in terms of functor categories. To model this permutation business, we start with the category $I$ of finite sets and injective maps. The idea is that each object of the category is a set of locations, and an injection gives you a map renaming some locations and allocating some more. Then, you model the types of your programming language as presheaves on $I$, and model the programs as natural transformations between the functors $[I^\mathrm{op}, \mathrm{Set}]$. This way, the semantics can't even speak about ill-behaved elements which don't respect the invariant, since every denotation is by construction natural.

You can ask whether this is necessary, and of course it isn't: we could just use a simple transition relation to model the semantics. The trouble is that this misses the point! The purpose of the semantics is to make it easy to reason about our programs, and to that end we want to work in a way where the properties we want to use are "come for free" rather than being laboriously pushed through every proof that might involve them.