- 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?