9
$\begingroup$

In mathematics, one often makes (proves) statements on the basis of:

  1. Previously proven statements
  2. Axioms

I like to think of these dependencies as a directed graph, with edges from the accepted statements (from 1. or 2.) to the new statements.

Often times, the same statement can be proven from many (potentially infinite) different statements, so one can imagine, many variants of this graph. Similarly, there is a potentially infinite number of statements one can prove.

Still, has there even been an attempt to visualize, perhaps at a very high level, what a graph like this would look like across all branches of mathematics, say, assuming that one starts with ZFC and only considers the most well known theorems, and commonly taught statements and proofs?

Taking this a step further, would it make sense to consider a minimum spanning graph that cover well known theorems in mathematics? If so, how could one measure the goodness of a graph (or a proof) for a given set of statements? (can the "intuitive complexity of this graph" be captured?).

If I had to collapse this into a single question: Is this problem actively studied? Or is it something that draws little interest in mathematics?

$\endgroup$
  • 6
    $\begingroup$ It might be a web rather than a tree. $\endgroup$ – Michael Hardy May 15 '14 at 19:36
  • 2
    $\begingroup$ One problem with this idea is that there is no objective consensus about when one idea directly follows from another. For instance, Person A might be happy with the $\text{Statement}_1 \Rightarrow \text{Statement}_2$ and have a directed edge $1 \to 2$, but Person B might insist that this should be factored as $\text{Statement}_1 \Rightarrow \text{Statement}_{1'} \Rightarrow \text{Statement}_2$ and we should have the path $1 \to 1' \to 2$. $\endgroup$ – Sammy Black May 15 '14 at 19:41
  • 1
    $\begingroup$ @user815423426 : For one thing, a theorem can have many different proofs. And often any of many different characterizations of a concept can be taken to be the definition. $\endgroup$ – Michael Hardy May 15 '14 at 19:42
  • 2
    $\begingroup$ It has the feel of a category since composition is just transitivity of logical implications and identity maps are tautologies. $\endgroup$ – Sammy Black May 15 '14 at 19:44
  • 3
    $\begingroup$ Have you seen metamath? They have at least the first of your desiderata, namely a proof of many advanced theorems of mathematics completely formally, from first principles. I don't know if they have done any analysis of the resulting graph, but they might have, and if not they certainly have the data that you want to analyze. $\endgroup$ – MJD May 15 '14 at 19:50
4
$\begingroup$

"Still, has there even been an attempt to visualize, perhaps at a very high level, what a graph like this would look like across all [emphasis added] branches of mathematics, say, assuming that one starts with ZFC and only considers the most well known theorems, and commonly taught statements and proofs?"

This is impossible, even if one wanted to visualize what such a graph looks like just in the case of propositional calculus, if we allow derived rules of inference (and don't mathematicians commonly make use of derived rules of inference?).

For instance, let's say we considered a propositional calculus with just 1: CpCqp and 2: CCpCqrCCpqCpr with detachment as the sole primitive rule of inference (I use Polish notation). Now all proofs can get represented by a proof tree like the following:

      X   Y
       \ /
        Z

where some substitution instance of X and Y have gotten used to infer Z by detachment, where X and Y already belonged to our theorem list. So all permissible proofs in this propositional calculus can get represented by such trees which only use the rule of detachment.

However, due to the rule of detachment there exists a powerful meta-theorem which says that

"if $\gamma$ $\vdash$ C$\alpha$$\beta$, then {$\gamma$, $\alpha$} $\vdash$ $\beta$".

Now from that meta-theorem and having CCpCqrCCpqCpr as a axiom, we have as a derivable rule {C$\alpha$C$\beta$$\gamma$, C$\alpha$$\beta$, $\alpha$} $\vdash$ $\gamma$. Thus, there exist proofs with a structure like the following:

 A  B  C
  \ | /
    D

It also holds that we have derivable rules for all theorems in this system, and some have some bajillion of antecedents! (by "bajillion" I mean whatever you consider a large number). This implies that there exist theorems with proof-trees like the above far too long to represent with all the resources of planet Earth just in propositional calculus.

So, even within one branch of mathematics producing such a graph leads to problems, because the number of proof methods is by no means small. Producing such a graph across all branches of even this propositional calculus produces difficulties, at least if we allow derivable rules of inference.

That isn't to say that such a graph would come as useless. However, you'll need to fix the rules of inference allowed, and you'll need to disallow derivable rules of inference, and consequently such a graph won't cover all branches of a subject.

| cite | improve this answer | |
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.