A bird's eye view of (fragments of) propositional calculus in set.mm

[Benoit]

Hi all,

I was tinkering with some visualizations of set.mm, and I thought those two graphs could be of interest to some of you. They are the dependency graphs among theorems of intuitionistic implicational calculus and of propositional calculus using implication, negation and biconditional.  In other words, theorems up to ~loowoz and up to ~imim21b respectively.

Benoît

[Norman Megill]

Stephen Wolfram has been investigating dependencies between theorems, including Metamath's set.mm, and has written up some findings here:
https://writings.stephenwolfram.com/2020/09/the-empirical-metamathematics-of-euclid-and-beyond/

He mentions that ~syl is the most popular set.mm theorem (as we know).  It appears that ~syl isn't the most prominent in your propcalc.pdf; instead, I think ~id and ~a1i have the most arrows pointing to them.  Apparently ~syl is mostly referenced after the prop calc section.

Norm