Has anyone worked out a formal, general-enough definition of what is 'useful', so that it could reflectively be used in mathematics? I am aware of the work in [utility theory](http://en.wikipedia.org/wiki/Useful) from economics (but originally from the Bernoullis and improved by von Neumann, so very much 'mathematical'). Such a formalization should be adequate to decide if a particular definition (or theorem) is considered 'useful'.


Note that I fully expect *utility* to be a relative notion, in other words I don't expect anything to be 'universally useful'. I have some tentative definitions, but before I spend too much time working this out, I would like to know if this has already been done mathematically (as the work of economists on this is [expectedly] too biased towards economic utility).


A concrete example: 20 years ago, elliptic curves would have been considered 'not useful' in the context of cryptography, now it is considered 'useful'. **This can be made completely formal**. [In other words, my question is about what has been done before, not a discussion of what this is, which if off-topic for MO].



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](https://mathoverflow.net/questions/17964/is-there-a-known-way-to-formalise-notion-that-certain-theorems-are-essential-on/18141#18141), 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](http://en.wikipedia.org/wiki/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.


