# Is there a known way to formalise notion that certain theorems are essential ones?

• Suppose You ask a question beginning from "Why some structure is..." or "Why some object has property..." and several answers arises. Which criteria do You use to qualify which answer is correct?

For example here You may find interesting picture (gzipped postscript file) of proofs formalized in Mizar system.. Mizar library of formalized theorems is really huge. On the picture You may see, that theorems arises from other and are used in proofs of another ones, forming big graph of structure of theorems formalized in Mizar so far. If I may read something from this graph, there is no theorem which will have more that 3 or 4 incoming edges what means there is no theorem which is used in more that 3 or 4 proofs. Of course there are some with 5 incoming edges, but in fact there is many theorems which have more or less equal number of incoming edges, which may mean that most theorems are equivalently important. Maybe it should be measured by tree deepness? Maybe there is something like Google page rank algorithm for theorems?

Probably we would like to have such relation: "theorems recognized as important should be influential, or foundational for broad area of theory".

• I understand that one may believe that this is a real state of matter, but are there any strict results based on real data in this matter?

By real data I mean at best proof theory analysis, or even citation analysis, but not someone opinion (which of course may be enlightening and inspirational). I would like to learn something about structure of deductive theories, and not about "real practice". It is the same as in real life: we try to measure risks, and income rate not based on someone opinion but on facts. Could we know the facts here?

It seems from Mizar graph ( which is the only one accessible for me in this area) I could not find any object which will correspond to our intuition of importance of theorems. Maybe this is effect of present Mizar state of affair, and in bigger/other system, some theorems begin central one? Are there any conditions to state such position?

• What about other proof assistants, as Isabelle or COQ. Is there any similar graph from other systems suitable for such analysis?
-
Kakaz, you're asking a lot of questions here. (I count 16.) I suspect you'll get a better response if you make the question much shorter and more focussed. At present I find it very difficult to see what would qualify as a definitive answer. – Tom Leinster Mar 12 '10 at 11:53
For what it's worth, I find this question very interesting, and also would like to know how one can distinguish formally which theorems are 'important'. It may be that instead of looking at how often a theorem is used, one could look at how many different proofs there are for a given theorem (i.e number of outgoing edges). The example I'm thinking of is quadratic reciprocity. It would be interesting to see a graph that tries to show all proofs of simpler theorems, rather than one proof of a hard theorem. – Zavosh Mar 12 '10 at 20:46
Also for what it's worth, I think that whether a theorem is "important" is subjective, and to a certain extent also controlled by fashion within mathematics---which areas are currently moving fast due to clear motivations and goals and so on. I hence think that there is no formal way for deciding whether a theorem is important. – Kevin Buzzard Mar 13 '10 at 8:51
@Kevin--One can imagine a setup based on PageRank. While (most) theorems are tautologies, some are more closely related than others. Some get used elsewhere in actual human proofs quite a bit, most not so much. So, make a list of the theorems in the literature (easier said than done, of course, even in principle b/c of variations on individual theorems) and make them vertices. Put a directed edge when one theorem is used to prove another. Then use PageRank to order the theorems based on their utility in the actual literature. – Steve Huntsman Mar 13 '10 at 14:49
Joel- I'm not sure I really agree that what you've written actually answers kakaz's question (it, for example, doesn't involve any actual data about what theorems mathematicians actually use), but I've reopened the question so you have a chance to answer. – Ben Webster Mar 14 '10 at 3:15

Although your question is vague in certain ways, one robust answer to it is provided by the subject known as Reverse Mathematics. The nature of this answer is different from what you had suggested or solicited, in that it is not based on any observed data of mathematical practice, but rather is based on the provable logical relations among the classical theorems of mathematics. Thus, it is a mathematical answer, rather than an engineering answer.

The project of Reverse Mathematics is to reverse the usual process of mathematics, by proving the axioms from the theorems, rather than the theorems from the axioms. Thus, one comes to know exactly which axioms are required for which theorems. These reversals have now been carried out for an enormous number of the classical theorems of mathematics, and a rich subject is developing. (Harvey Friedman and Steve Simpson among others are prominent researchers in this area.)

The main, perhaps surprising conclusion of the project of Reverse Mathematics is that it turns out that almost every theorem of classical mathematics is provably equivalent, over a very weak base theory, to one of five possibilities. That is, most of the theorems of classical mathematics turn out to be equivalent to each other in five large equivalence classes.

For example,

• Provable in and equivalent to the theory RCA0 (and each other) are: basic properties of the natural/rational numbers, the Baire Cateogory theorem, the Intermediate Value theorem, the Banach-Steinhaus theorem, the existence of the algebraic closure of a countable field, etc. etc. etc.

• Equivalent to WKL0 (and each other) are the Heine Borel theorem, the Brouer fixed-point theorem, the Hahn-Banach theorem, the Jordan curve theorem, the uniqueness of algebraic closures, etc. , etc. etc.

• Equivalent to ACA0 (and each other) are the Bolzano-Weierstraus theorem, Ascoli's theorem, sequential completeness of the reals, existence of transcendental basis for countable fields, Konig's lemma, etc., etc.

• Equivalent to ATR0 (and each other) are the comparability of countable well orderings, Ulm's theorem, Lusin's separation theorem, Determinacy for open sets, etc.

• Equivalent to Π11 comprehension (and each other) are the Cantor-Bendixion theorem and the theorem that every Abelian group is the direct sum of a divisible group and a reduced group, etc.

The naturality and canonical nature of these five axiom systems is proved by the fact that they are equivalent to so many different classical theorems of mathematics. At the same time, these results prove that those theorems themselves are natural and essential in the sense of the title of your question.

The overall lesson of Reverse mathematics is the fact that there are not actually so many different theorems, in a strictly logical sense, since these theorems all turn out to be logically equivalent to each other in those five categories. In this sense, there are essentially only five theorems, and these are all essential. But their essential nature is mutable, in the sense that any of them could be replaced by any other within the same class.

I take this as a robust answer to the question that you asked (and perhaps it fulfills your remark that you thought ideally the answer would come from proof theory). The essential nature of those five classes of theorems is not proved by looking at their citation statistics in the google page-rank style, however, but by considering their logical structure and the fact that they are logically equivalent to each other over a very weak base theory.

Finally, let me say that of course, the Reverse Mathematicians have by now discovered various exceptions to the five classes, and it is now no longer fully true to say that ALL of the known reversals fit so neatly into those categories. The exceptional theorems are often very interesting cases which do not fit into the otherwise canonical categories.

-
Your answer is very interesting, and in some sense globally, which means that You answer regards to the whole mathematics. I would like to state certain objections to Your very good answer. First :It is nearly ideal answer, and I learn a lot after recognizing this approach. But, as You may find at Simpson webpage, and within his publications, he states that is not the case that "fundamental theorems" are necessary "the most interesting ones". So as we know by reverse mathematics which theorems are ** fundamental ** we still do not know what ** "the interesting" ** mean – kakaz Mar 14 '10 at 10:07
Second : as every mathematical theory may be regarded as more or less separated one ( I know it is disputable), there should be explicite criteria which allows us at least to perform exactly the same analysis as with reverse mathematics but localized only to certain theory, for example only for complex functions. We may think of stating axioms for such theory ( and it may be different than $RCA_0$ etc), and still we may look for criteria of importance. So as Your answer may be concerned as great example of some approach it is not description of the method. – kakaz Mar 14 '10 at 10:12
Third : during discussion with Scot Morison on meta he states: "the trivial answer that there is no natural decomposition of mathematical truth into "theorem" nuggets, and the granularity of a chosen decomposition is just as much (actually, maybe more so!) a product of the social environment". I would be appreciated if he or someone else may say something similar here. Is that true that there is no such decomposition, so only relation to axioms are the only possible here? So I state this clear as last question in comment below. – kakaz Mar 14 '10 at 10:15
Is that true that there is no natural decomposition of mathematical truth into theorems? Is that true that the only natural is dichotomy axioms - theorems, where axioms are given and known, whilst theorems are only particular way of description of theory? Are theorems only arbitrary chosen kind of notation for consequences of axioms? – kakaz Mar 14 '10 at 10:20
So Joel, let me wait for a few hours maybe someone will say here something interesting. If not I will accept Your answer because it is obviously useful and at least formally correct. – kakaz Mar 14 '10 at 10:23