2

Sorry if this feels a bit squishy, but I'm wondering if there is any published work trying to give a fully formal definition of the notion of a useful theorem. I mean, in mathematics we all know that some theorems seem to be quite powerful while others seem almost virtually useless outside of a single application. Has anyone tried to use this idea to give a Kolmogorov complexity inspiredish definition of a useful theorem? Or demonstrated no such definition will work?

I'm thinking something along the lines of: A theorem $\phi$ is useful for an axiomitizatoin $A$ to the extent to which adding $\phi$ to $A$ (asymptotically) reduces the length of the proofs of the theorems of $A$. For instance, maybe look at how adding $\phi$ affects the number of characters needed to prove all theorems in $T_n$ and let $n$ go to infinity. Here $T_n$ is something like a the $< n$ symbol $A$ theorems or the $A$ theorems with proof length $<n$).

Anyway, I just provided that to give a flavor of what kind of thing I sorta mean. I'm just wondering if there is anything published vaguely in the area.

EDIT: When I say work, I mean that it validates the idea that some theorems are more useful than others in some natural sense rather than one which is totally dependent on our aesthetic judgements about which results we care about proving.

Peter Gerdes
  • 2,613
  • 2
    Sort of similar discussion at: https://mathoverflow.net/questions/3776/when-are-two-proofs-of-the-same-theorem-really-different-proofs – Sam Hopkins May 22 '22 at 03:15
  • 5
    If $\phi$ is a theorem of $A$ already, then adding $\phi$ as an axiom to $A$ can only result in a constant speedup. – Noah Schweber May 22 '22 at 03:20
  • Sorry, yes, but we can look at how it helps when we add it to weaker systems. I admit I kinda blurred that idea together in my head with the idea of those proof systems that only let each result be used once when I was writing the post (in which case each time you want to use a result you have to reprove it so adding it to axioms could result in more than constant speedup). – Peter Gerdes May 22 '22 at 03:32
  • but yah, after a brief thought, neither of those ideas are going to be very interesting imo. Is there a better one. – Peter Gerdes May 22 '22 at 03:46
  • 2
    Something you'd need to address after making a formal definition of a useful theorem is convincing people that the formal definition is itself useful. Giving something the name "useful" doesn't mean it actually is useful. Some concepts and theorems were not recognized as being profoundly important until many years after being introduced (look at how long people ignored Grassmann's attempts at setting up abstract linear algebra), and it's hard to believe pure reason can identify something as being useful before it actually turns out to be useful. – KConrad May 22 '22 at 04:56
  • Asymptotically, adding a fixed theorem cannot help by more than an additive constant. Nonasymptotically, every theorem which is not an axiom reduces the length of some theorems, such as itself, or things like arbitrarily bracketed conjunctions of copies of itself; you can surely arrange an exponential number (in the length of $\phi$) of such “theorems”. I don’t think there is a useful definition of usefulness along such quantitative lines. – Emil Jeřábek May 22 '22 at 06:09
  • 3
    It is true that for the purposes of solving a single question $Q$, any gven theorem $\phi$ can only achieve a constant speedup. But if one has a large number $Q_1,\dots,Q_n$ of questions one is interested in, knowing that $\phi$ is available as a theorem can reduce the net cost $\sum_{i=1}^n \hbox{proof complexity}(Q_i)$ by as much as $Cn$. One could imagine proposing the growth rate of this net cost saving as a function of $n$ as a measure of "usefulness", but one has to agree on what the natural body of test questions $Q_i$ is first. – Terry Tao May 22 '22 at 16:31
  • 3
    Also, in practice, it is not so much the raw Kolmogorov-type proof complexity of a question that is of relevance, but how likely it is for a mathematician in the field to find a proof, which is more akin to computing the "harmonic measure" of that question relative to the current boundary of mathematical knowledge in the field, and even for a single question this might be significantly reduced by adding $\phi$ to this boundary. But this is extremely hard to formalise as we do not currently have a realistic metamathematical model for the thought processes of mathematicians. – Terry Tao May 22 '22 at 16:34
  • Interesting, my initial motivation was actually because I was curious if you could come up with a definition of useful that could be applied by an unguided theorem prover w/o human judgement (eg as a guide to what results) were worth saving for later use as lemmas. (maybe not as good as human judge but was thinking maybe you could do things like replace the Bitcoin mining proof of work w/ finding a sufficiently useful new theorem). But then I just got curious if you could do it even if you didn't demand it be a computable/practical property. – Peter Gerdes May 22 '22 at 20:40
  • Can you give some examples of useful theorems? Eg I know calculus is useful, but it would be odd to go from there to saying that the fundamental theorem of calculus is useful. –  May 25 '22 at 02:53
  • By useful, the idea I had in mind was just that some results are more helpful in proving other results than others (taking into account their length so you can't just and together more and more true statements). For instance, the claim that every quadratic poly over C has a root is less useful than the claim that every poly over C has a root since they the same length and the later helps prove more statements. – Peter Gerdes May 25 '22 at 03:03

0 Answers0