(1,1) fabric: 1 iteration for axioms; 1 iteration for “propositions”

Make entailment cones for the axioms ; make them for the propositions
Do these entailment cones overlap? [i.e. are the propositions theorems in this axiom system?]
The “atoms” of axiomatic mathematics (i.e. statements) are somewhat human readable [as opposed to atoms of space]

Sample string-based entailment fabric

In[]:=
CombinedFabricTagged[rules_,t_,opts___]:=Graph[Flatten[MapIndexed[Function[{a,b},With[{rc=Blend[{ResourceFunction["WolframPhysicsProjectStyleData"]["BranchialGraph"]["EdgeStyle"],Hue[FractionalPart[GoldenRatioFirst[b]]]},.3]},Style[Append[#,First[b]],rc]&/@EdgeList[removeEvents@ResourceFunction["TokenEventGraph"][{{r1_,r2_}:>StringApply[r1,r2]},a,t,"TokenMultiplicity"->Automatic,"EventDeduplication"->True,"TokenLabeling"->False]]]],rules]],opts]
In[]:=
CombinedFabricTagged[{"A""AAAA","AA""AAA","AA""AAAA","AAA"<->"AAAA"},2,VertexLabels->Automatic,VertexStyle->ResourceFunction["WolframPhysicsProjectStyleData"]["BranchialGraph"]["VertexStyle"],VertexSize->.15]
Out[]=

True expression entailment fabric

In[]:=
TokenEventSubstitutionGraph[{#},1]&/@(AxiomaticTheoryTWP[AxiomaticTheory["BooleanAxioms"]]/.{CircleTimes->Wedge,CirclePlus->Vee})
Out[]=

,
,
,
,
,

In[]:=
Graph[Flatten[MapIndexed[Function[{a,b},With[{rc=Blend[{ResourceFunction["WolframPhysicsProjectStyleData"]["BranchialGraph"]["EdgeStyle"],Hue[FractionalPart[GoldenRatioFirst[b]]]},.3]},Style[Append[#,First[b]],rc]&/@EdgeList[removeEvents@(TokenEventSubstitutionGraph[{a},1])]]],AxiomaticTheoryTWP[AxiomaticTheory["BooleanAxioms"]]/.{CircleTimes->Wedge,CirclePlus->Vee}]],VertexLabels->(v_:>symbolifyPatterns[v])]
Out[]=
In[]:=
Graph[Flatten[MapIndexed[Function[{a,b},With[{rc=Blend[{ResourceFunction["WolframPhysicsProjectStyleData"]["BranchialGraph"]["EdgeStyle"],Hue[FractionalPart[GoldenRatioFirst[b]]]},.3]},Style[Append[#,First[b]],rc]&/@EdgeList[removeEvents@(TokenEventSubstitutionGraph[{a},2])]]],AxiomaticTheoryTWP[AxiomaticTheory["BooleanAxioms"]]/.{CircleTimes->Wedge,CirclePlus->Vee}]]]
Out[]=

Bisubstitution

Note: reduced leaf count cutoff