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"],DirectedEdgesTrue]]]]//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”
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
Multiway to Equational
Can have unidirectional string case ... but involves lots of infrastructure
Can have unidirectional string case ... but involves lots of infrastructure
Causal edges: making use of previous expr, and also previous jump-ahead theorem
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]
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
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
To be “about something” is to make everything deterministic; i.e. a total order
Transportability of category theory : uniformity of metamathematical space
Transportability of category theory : uniformity of metamathematical space
Expansion of MM universe: all the computer experiments you could do
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 ]
Expansion of rulial space : NKS is necessary; math can’t reach far enough [ NKS : quantum computer ; math : classical computer ]