You are using a browser not supported by the Wolfram Cloud
Supported browsers include recent versions of Chrome, Edge, Firefox and Safari.
I understand and wish to continue anyway »
WOLFRAM NOTEBOOK
(1,1) fabric: 1 iteration for axioms; 1 iteration for “propositions”
(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?]
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
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
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
Bisubstitution
Note: reduced leaf count cutoff