14
$\begingroup$

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.

Improve this question
$\endgroup$
13
  • 10
    $\begingroup$ directed acyclic graph, hopefully $\endgroup$
    – Yoav Kallus
    Commented Jun 9, 2015 at 16:49
  • 4
    $\begingroup$ 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. $\endgroup$
    – Robert Israel
    Commented Jun 9, 2015 at 16:57
  • 3
    $\begingroup$ You could get a well-defined graph describing the relationships between the results in a particular (traditional) exposition (i.e., textbook). $\endgroup$
    – Jeff Strom
    Commented Jun 9, 2015 at 19:49
  • 2
    $\begingroup$ @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. $\endgroup$
    – Yoav Kallus
    Commented Jun 9, 2015 at 20:00
  • 2
    $\begingroup$ A family tree for the definitions in a mathematical theory might also be a good idea that maybe is easier to realize. $\endgroup$
    – Manfred Weis
    Commented Jun 10, 2015 at 6:17

4 Answers 4

Reset to default
12
$\begingroup$

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!

Improve this answer
$\endgroup$
4
  • $\begingroup$ 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. $\endgroup$
    – Yoav Kallus
    Commented Jun 9, 2015 at 19:14
  • 2
    $\begingroup$ @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. $\endgroup$
    – François G. Dorais
    Commented Jun 9, 2015 at 20:14
  • $\begingroup$ Just to clarify, I think the double arrows your are talking about are the double stroked arrows, not the double headed arrows. $\endgroup$
    – Yoav Kallus
    Commented Jun 9, 2015 at 20:24
  • $\begingroup$ @YoavKallus Sorry, I misread your description of the arrows. I guess you mean the equivalences rather than the strict implications. $\endgroup$
    – François G. Dorais
    Commented Jun 10, 2015 at 14:17
5
$\begingroup$

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

Improve this answer
$\endgroup$
1
3
$\begingroup$

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 3 of Mascuni 2011 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.

Improve this answer
$\endgroup$
2
$\begingroup$

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.

Improve this answer
$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .