[Math] “Family Tree” of Theorems

reverse-mathsoft-question

Is anyone aware of any attempt to describe the dependencies of theorems (perhaps in mathematics generally, perhaps in some limited areas) in the form of a "family tree"? That is, each node on the tree might correspond to a theorem, and branches would indicate dependencies between theorems? I realize that this would not constitute an actual tree — as there can exist loops — but this sort of meta-description of theorems might provide some insight not available in other manners.

[Added:] Except in some very formalized proof systems, making the notion of dependency precise is probably difficult, if not impossible. But colloquially, people will often make statements such as "Theorem A is used / can be used to prove Theorem B". I'm sure everyone here can think of many such statements to which few will object. For those cases, it might be very nice to have some accessible database with this information. Not only might the data in this "graph" be practically useful (e.g., I want to write an expository paper about five interesting consequences of the Borsuk-Ulam theorem), but perhaps even some "meta-data" might provide valuable insight. Just a thought.

Best Answer

The idea of "dependencies" is somewhat ill-defined. The Reverse Mathematics Program has one way of defining dependencies by comparing the theorems over a very weak base theory called RCA0. To see nice diagrams stemming from this program, check out the Reverse Mathematics Zoo!