ResourceFunction["MultiwaySystem"][{"A""AB","BB""A"},{"A"},7,"StatesGraph"]
In[]:=
Out[]=
With[{g=ResourceFunction["MultiwaySystem"][{"A""AB","BB""A"},{"A"},7,"StatesGraph"]},HighlightGraph[g,Subgraph[g,PathGraph[FindShortestPath[g,"A","AABA"]]]]]
In[]:=
Out[]=
With[{g=ResourceFunction["MultiwaySystem"][{"A""AB","BB""A","AB""A","A""BB"},{"A"},7,"StatesGraph"]},HighlightGraph[g,Subgraph[g,PathGraph[FindShortestPath[g,"A","AABA"],DirectedEdgesTrue]]]]//LayeredGraphPlot
In[]:=
Out[]=
With[{g=ResourceFunction["FindStringProof"][{"A""AABA"},{"A""AB","BB""A"}]["ProofGraph"]},Graph[g,VertexLabels(#[[1]]#[[2,1,2,1,2]]&/@Options[g,"AnnotationRules"][[1,2]])]]
In[]:=
Out[]=
Every substitution X = Y has an evolution edge and a causal edge
After transitive closure, the causal edges in the proof graph are the same as in the MW graph
TransitiveClosureGraph[ResourceFunction["MultiwaySystem"][{"A""AB","BB""A"},{"A"},3,"StatesGraph"]]
In[]:=
Out[]=
ResourceFunction["MultiwaySystem"][{"A""AB","BB""A","A""AAB"},{"A"},4,"StatesGraph"]//LayeredGraphPlot
In[]:=
Out[]=
[ semantic entailment ]
[ rules of inference ]
proposition: a = b
​
Case 1: every node is a proposition; a true theorem is a path from a proposition node to the True node
Case 2: every node is a word, and theorems are paths between “equivalent” words

Generational states ↔ theorems “in the bag”

A jump ahead event is causally connected to all its component events. [Though in the proof graph, only one causal edge is shown here] [ Because the proof graph is essentially a transitive reduction ]
Looking at centrality of lemmas:

Multiway to Equational

Can have unidirectional string case ... but involves lots of infrastructure

Causal edges: making use of previous expr, and also previous jump-ahead theorem

Inevitably “positive mass”, because previous results just increase number of different paths.

Critical fact: you put the whole proof in the bag, and use it as a one-step theorem [univalence]

Assumption : metamath is explored on geodesics ; therefore you don’t get to see all the theorems of this axiom system

Dynamical theory of epistemology

To be “about something” is to make everything deterministic; i.e. a total order

Transportability of category theory : uniformity of metamathematical space

Expansion of MM universe: all the computer experiments you could do

Expansion of rulial space : NKS is necessary; math can’t reach far enough [ NKS : quantum computer ; math : classical computer ]