“Family Tree” of Theorems

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.

• directed acyclic graph, hopefully – Yoav Kallus Jun 9 '15 at 16:49
• These dependencies are not unambiguous. There may be many different proofs of theorem $A$, some of which use theorem $B$, while others use theorem $C$, and still others prove $A$ first and derive $B$ and $C$ as corollaries. – Robert Israel Jun 9 '15 at 16:57
• You could get a well-defined graph describing the relationships between the results in a particular (traditional) exposition (i.e., textbook). – Jeff Strom Jun 9 '15 at 19:49
• @Goldstern but if you read in a textbook "Theorem H. Proof: follows from Z □" then "Theorem Z. Proof: follows from H □", you would throw the book in garbage. – Yoav Kallus Jun 9 '15 at 20:00
• A family tree for the definitions in a mathematical theory might also be a good idea that maybe is easier to realize. – Manfred Weis Jun 10 '15 at 6:17

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!

• What does a double-headed arrow mean in one of these diagrams (e.g. rmzoo.math.uconn.edu/wp-content/uploads/sites/841/2014/09/…)? I think what Menachem is asking about is dependencies -- i.e. what statements are used to prove what statements -- not implications. While the question of implications is also fascinating, I think it is orthogonal to the question Menachem was asking. – Yoav Kallus Jun 9 '15 at 19:14
• @YoavKallus: Double arrows usually mean that the converse implication is known to be false. Dependency is very hard to define rigorously. The connection is that if $A$ really depends on $B$ then it must be that $B$ implies $A$. Otherwise, we could use something strictly weaker than $A$ to prove $B$. (For example, $A \lor B$ could be used instead of $A$.) There doesn't seem to be any other purely mathematical ways of defining "dependency". There are, of course, historical and sociological ways to define dependency that behave differently. – François G. Dorais Jun 9 '15 at 20:14
• Just to clarify, I think the double arrows your are talking about are the double stroked arrows, not the double headed arrows. – Yoav Kallus Jun 9 '15 at 20:24
• @YoavKallus Sorry, I misread your description of the arrows. I guess you mean the equivalences rather than the strict implications. – François G. Dorais Jun 10 '15 at 14:17

Concerning (parts of) algebraic geometry, the Stacks Project offers so-called dependency graphs.

Formal vs self-organised knowledge systems: a network approach

A.P. Masucci, Physica A 390 (2011) 4652-4659 (arXiv:1105.1058)

In this work we consider the topological analysis of symbolic formal systems in the framework of network theory. In particular we analyse the network extracted by Principia Mathematica of B. Russell and A.N. Whitehead, where the vertices are the statements and two statements are connected with a directed link if one statement is used to demonstrate the other one. We compare the obtained network with other directed acyclic graphs, such as a scientific citation network and a stochastic model. We also introduce a novel topological ordering for directed acyclic graphs and we discuss its properties in respect to the classical one. The main result is the observation that formal systems of knowledge topologically behave similarly to self-organised systems.

This paper looks at how logical statements such as theorems are organized in specific expository works (like the Principia). As others have noted in the comments, outside such organized works, the dependencies can be ambiguous as theorems can have alternate proofs. Moreover, the order of deriving theorems is not canonical so that if all proof paths were included, cycles will have formed. The Principia is as good as any work to start with, but I would really love to see a similar analysis on Bourbaki and on Euclid's Elements.

Figure from the paper: distribution of in and out degrees in the Principia DAG, in the DAG of citations, and in a stochastic generative model.

There are fairly recent dependency graphs relating to Euclid's Book 1, Elements, in the literature. See A Boxer's paper in Bridges Art/Math 2015 Also see M. Schiefsky (Harvard Classics) and Boman (Penn State Math) and Nyugen (Berkeley) for overviews and graphs. The most interesting is that of Jesse Atkinson, Bridges Art/Math 2016, that shows a 3-D in-tree dependency graph of Euclid's proof of the Pythagorean Theorem (1.47) embedded in a discussion about the overall role of 1.45 and 1.47 in that book. It is an elegant "little" paper, by an undergraduate math student, to say the least.