pr.probability - Formal definition of 'useful' ?

It seems to me that you have two questions here.

First, you inquire about a formal account of "usefulness". I believe that this is already provided by the formal mathematical accounts of utility in utility theory. The concept of utility in that theory is extremely flexible, not limited to economics or any other specific endeavor. Thus, it seems able to provide for any account of "usefulness" you may have in mind. Let's just say that the utility provided by a given thing is equal to the "usefulness" you had in mind for it.

Your second question is more directly aimed at analyzing the usefulness of various specific mathematical ideas. For this question, I'm not sure that what is lacking is a formal definition of usefulness. After all, even if one knows a lot of formal utility theory, it doesn't help you to find out which flavor of ice cream your child likes best. Rather, what one would seem to want is ways of measuring various specific measurable aspects of that utility function. Thus, it is a problem of measurement, rather than formal theory. In the case of measuring the importance of utility or usefulness of various mathematical theorems or definitions, several people have suggested a page-rank type calculation, based on citation statistics, which I find interesting.

Another approach to this second question is the one I described in my answer to the question here, which is to analyze the mathematical relationships between the various theorems of mathematics, over a very weak base theory. This subject is known as Reverse Mathematics, and one of the most surprising conclusions (not at all obvious) of this research effort is that the great majority of classical mathematical theorems (and contemporary ones as well) fall into one of five equivalence classes. That is, most theorems turn out to be logically equivalent to one of the big five. This kind of analysis may lead you to abandon what might otherwise have been a tempting principle: that logically equivalent theorems should be equally useful.