In[]:=
HistogramLeafCount/@
[◼]
PatternsToSymbols
VertexList
[◼]
TwoWayRuleTokenEventGraph

[◼]
AxiomaticTheoryTWP
["WolframAxioms"],2,"Identity"True,_TwoWayRule,{1},AspectRatio->12,Frame->True,ChartStyleOrange
Out[]=
Editing Note: (a) Add whatever colors to plot style (b) vertical shift via #2 if necessary.
In[]:=
AbsoluteTiming​​GraphDat=
[◼]
TwoWayRuleNestGraph
[x_∘y_<->(y_∘x_)∘y_,(a∘b)∘a,8];​​
Out[]=
{3841.01,Null}
Show​​ListLinePlot[​​MapIndexed[(LeafCount[#1]+1)/2+.2&,​​FindPath[GraphDat,(a∘((b∘a)∘(a∘b)))∘a,b∘a,{6,7},All],{2}],​​PlotStyle->{Gray},FillingAxis,​​FillingStyle->Directive[Opacity[.05],Lighter[LightGray]]],​​ListLinePlot​​MapIndexed[(LeafCount[#1]+1)/2+0.2(#2[[1]]-1)&,​​FindPath[GraphDat,(a∘((b∘a)∘(a∘b)))∘a,b∘a,5,All],{2}],​​PlotStyle->Directive[AbsoluteThickness[5],#]&/@
,
,
,​​FillingAxis,FillingStyle->Directive[Opacity[.05],Lighter[LightGray]],​​Plot[2,{x,1,8},PlotStyleDirective[Gray,Dashed]],​​Frame->True,PlotRange->{{1,8},{0,9}},​​FrameTicks->{{Range[9],None},{Range[8],None}}
ParallelTableWithaon=
[◼]
EnumerateBooleanExpressions
[p,Take[{a,b,c,d},n]]/.{Equal->Equivalent,OverBar->Not,Wedge->And,Vee->Or},{Length@aon,Style[Length@Select[aon,TautologyQ]]},{p,2,5},{n,3}
In[]:=
[◼]
EnumerateBooleanExpressions
[2,Take[{a,b,c,d},2]]/.{Equal->Equivalent,OverBar->Not,Wedge->And,Vee->Or}
Out[]=
{a⧦b,a⧦!a,a⧦!b,!a⧦!b}
In[]:=
[◼]
EnumerateBooleanExpressions
[3,Take[{a,b,c,d},2]]/.{Equal->Equivalent,OverBar->Not,Wedge->And,Vee->Or}
Out[]=
{a⧦b,a⧦!a,a⧦!b,a⧦a&&a,a⧦a||a,a⧦a&&b,a⧦a||b,a⧦b&&a,a⧦b||a,a⧦b&&b,a⧦b||b,!a⧦!b,a&&a⧦!a,!a⧦a||a,a&&b⧦!a,!a⧦a||b,b&&a⧦!a,!a⧦b||a,b&&b⧦!a,!a⧦b||b,a⧦a&&!a,a&&!a⧦!a,a⧦!a&&a,!a&&a⧦!a,a⧦!a&&!a,!a&&!a⧦!a,a⧦a||!a,!a⧦a||!a,a⧦!a||a,!a⧦!a||a,a⧦!a||!a,!a⧦!a||!a,a⧦!(a&&a),!a⧦!(a&&a),a⧦!(a||a),!a⧦!(a||a),a⧦a&&!b,a&&!b⧦!a,a⧦!a&&b,!a&&b⧦!a,a⧦!a&&!b,!a&&!b⧦!a,a⧦a||!b,!a⧦a||!b,a⧦!a||b,!a⧦!a||b,a⧦!a||!b,!a⧦!a||!b,a⧦!(a&&b),!a⧦!(a&&b),a⧦!(a||b),!a⧦!(a||b),a⧦b&&!a,b&&!a⧦!a,a⧦!b&&a,!b&&a⧦!a,a⧦!b&&!a,!b&&!a⧦!a,a⧦b||!a,!a⧦b||!a,a⧦!b||a,!a⧦!b||a,a⧦!b||!a,!a⧦!b||!a,a⧦!(b&&a),!a⧦!(b&&a),a⧦!(b||a),!a⧦!(b||a),a⧦b&&!b,b&&!b⧦!a,a⧦!b&&b,!b&&b⧦!a,a⧦!b&&!b,!b&&!b⧦!a,a⧦b||!b,!a⧦b||!b,a⧦!b||b,!a⧦!b||b,a⧦!b||!b,!a⧦!b||!b,a⧦!(b&&b),!a⧦!(b&&b),a⧦!(b||b),!a⧦!(b||b),a⧦!(a&&!a),!a⧦!(a&&!a),a⧦!(!a&&a),!a⧦!(!a&&a),a⧦!(!a&&!a),!a⧦!(!a&&!a),a⧦!(a||!a),!a⧦!(a||!a),a⧦!(!a||a),!a⧦!(!a||a),a⧦!(!a||!a),!a⧦!(!a||!a),a⧦!(a&&!b),!a⧦!(a&&!b),a⧦!(!a&&b),!a⧦!(!a&&b),a⧦!(!a&&!b),!a⧦!(!a&&!b),a⧦!(a||!b),!a⧦!(a||!b),a⧦!(!a||b),!a⧦!(!a||b),a⧦!(!a||!b),!a⧦!(!a||!b),a⧦!(b&&!a),!a⧦!(b&&!a),a⧦!(!b&&a),!a⧦!(!b&&a),a⧦!(!b&&!a),!a⧦!(!b&&!a),a⧦!(b||!a),!a⧦!(b||!a),a⧦!(!b||a),!a⧦!(!b||a),a⧦!(!b||!a),!a⧦!(!b||!a),a⧦!(b&&!b),!a⧦!(b&&!b),a⧦!(!b&&b),!a⧦!(!b&&b),a⧦!(!b&&!b),!a⧦!(!b&&!b),a⧦!(b||!b),!a⧦!(b||!b),a⧦!(!b||b),!a⧦!(!b||b),a⧦!(!b||!b),!a⧦!(!b||!b)}
In[]:=
[◼]
EnumerateBooleanExpressions
[2,Take[{a,b,c,d},1]]/.{Equal->Equivalent,OverBar->Not,Wedge->And,Vee->Or}
Out[]=
{a⧦!a}
"MathFieldColors"->{"axioms"->Hue[0.26,0.67,0.76],"set theory"->Hue[0.02,0.68,0.9400000000000001],"logic"->Hue[0.07,0.9,1.],"numbers"->Hue[0.12,0.86,1.],"algebra"->Hue[0.44,0.5,0.72],"analysis"->Hue[0.56,0.5,0.78],"geometry & topology"->Hue[0.77,0.36,0.75],"abstract structures"->Hue[0.89,0.51,0.79]}

pythag

In[]:=
partRules=<|"CLASSICAL FIRST-ORDER LOGIC WITH EQUALITY""logic","ZF (ZERMELO-FRAENKEL) SET THEORY""set theory","SUPPLEMENTARY MATERIAL (USER'S MATHBOXES)""infrastructure","ZFC (ZERMELO-FRAENKEL WITH CHOICE) SET THEORY""set theory","TG (TARSKI-GROTHENDIECK) SET THEORY""set theory","REAL AND COMPLEX NUMBERS""numbers","ELEMENTARY NUMBER THEORY""numbers","BASIC STRUCTURES""algebra","BASIC CATEGORY THEORY""algebra","BASIC ORDER THEORY""algebra","BASIC ALGEBRAIC STRUCTURES""algebra","BASIC LINEAR ALGEBRA""algebra","BASIC TOPOLOGY""geometry & topology","BASIC REAL AND COMPLEX ANALYSIS""analysis","BASIC REAL AND COMPLEX FUNCTIONS""analysis","ELEMENTARY GEOMETRY""geometry & topology","GRAPH THEORY""abstract structures","GUIDES AND MISCELLANEA""infrastructure","COMPLEX HILBERT SPACE EXPLORER (DEPRECATED)"->"infrastructure","SUPPLEMENTARY MATERIAL (USER'S MATHBOXES)"->"infrastructure","COMPLEX TOPOLOGICAL VECTOR SPACES (DEPRECATED)"->"infrastructure"|>;
In[]:=
parts={"logic","set theory","numbers","algebra","geometry & topology","analysis","abstract structures"};
In[]:=
metamathInfrastructure={"SUPPLEMENTARY MATERIAL (USER'S MATHBOXES)","GUIDES AND MISCELLANEA",​​"COMPLEX HILBERT SPACE EXPLORER (DEPRECATED)","SUPPLEMENTARY MATERIAL (USER'S MATHBOXES)","COMPLEX TOPOLOGICAL VECTOR SPACES (DEPRECATED)"};
In[]:=
partColors=Association
[◼]
MetamathematicsStyleData
["MathFieldColors"];
In[]:=
mm=
[◼]
MetamathImport
[Uncompress@CloudGet[CloudObject[
https://www.wolframcloud.com/obj/wolframphysics/setmm
]]];//AbsoluteTiming
Out[]=
{47.6683,Null}
In[]:=
metamathGraph=mm["DependencyGraph"];
In[]:=
mmvars=Cases[mm["Statements"],_[label_,{"wff"|"class"|"setvar",__},___]:>label];
In[]:=
setmmReport=ResourceData["Metamath-Report"];
In[]:=
metamathAssoc=ToUpperCase@Association[Rule@@@Normal@Values@setmmReport[All,{"Label","Part"}]];
In[]:=
metamathAssoc["pythi"]=metamathAssoc["pythag"];
In[]:=
dropTheorems=Select[metamathAssoc,MatchQ[Alternatives@@metamathInfrastructure]];
In[]:=
mmgraph=Subgraph[metamathGraph,DeleteCases[VertexList[metamathGraph],​​Alternatives@@Join[mmvars,Keys@dropTheorems]]];
In[]:=
With[{gr=TransitiveReductionGraph[Subgraph[mmgraph,VertexOutComponent[mmgraph,"pythag"],VertexLabelsNone]]},​​Legended[ReverseGraph[gr,GraphLayout"LayeredDigraphEmbedding",AspectRatio1/2,EdgeStyleGrayLevel[0.5,0.5],VertexStyle->((#Enclose[Directive[Hue[#1,#21.4,#3]&@@Hue[#]&@Confirm[partColors[partRules[metamathAssoc[#]]]],EdgeForm[]],Gray&])&/@VertexList[gr]),VertexSize->1.5,ImageSize->{640,Automatic}],Placed[SwatchLegend[Drop[Values[partColors],-1],Style[#,GrayLevel[.4]]&/@Drop[Keys[partColors],-1],LegendLayout->(Row[Map[Row[#,Spacer[0]]&,#],Spacer[8]]&)],Below]]​​]
Out[]=
axioms
set theory
logic
numbers
algebra
analysis
geometry & topology

Not this

In[]:=
With[{gr=Subgraph[mmgraph,VertexOutComponent[mmgraph,"pythag"],VertexLabelsNone]},​​Legended[ReverseGraph[gr,GraphLayout"LayeredDigraphEmbedding",AspectRatio1/2,EdgeStyleGrayLevel[0.5,0.5],VertexStyle->((#Enclose[Directive[Hue[#1,#21.4,#3]&@@Hue[#]&@Confirm[partColors[partRules[metamathAssoc[#]]]],EdgeForm[]],Gray&])&/@VertexList[gr]),VertexSize->1.5],Placed[SwatchLegend[Drop[Values[partColors],-1],Style[#,GrayLevel[.4]]&/@Drop[Keys[partColors],-1]],After]]​​]