- 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?
Best Answer
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.