Minimal Models

Possible distinction:

Type 1: axioms are outside the system

Case 1: propositions are edges [in the proof graph]

vertices are expressions
expr1<->expr2
Proof graph: 1many

Case 2: propositions are vertices

Apply an axiom to one proposition to get another
Proof graph: 1many

Type 2: axioms are inside the system

There is a big vat of propositions
The propositions are combined through entailments
Propositions are like hyperedges ; entailments are just like WM rules [which consume certain hyperedges and generate new ones]

Type 3: the rulial limit

All possible entailments are considered

Minimal Model of a Type 2 Entailment

Known types:
substitutions
critical pair lemmas
? resolution
[inference rules]

They take multiple hyperedges and produce hyperedges

Is there a string version? Probably not

Minimal entailment:
StringJoin[XXX]

String Entailments

"ABBBA","BBBA"
In[]:=
ResourceFunction["TokenEventGraph"][{x_,y_}:>{Join[x,y],Join[y,x]},{{1,0},{0,1}},3,"TokenRenderingFunction"->Row]
Out[]=
In[]:=
ResourceFunction["TokenEventGraph"][{x_,y_}:>{Join[x,y],Join[y,x]},{{1,0},{0,1}},3,"TokenRenderingFunction"->Row,"TokenDeduplication"->False]
Out[]=
This axiom system can prove ? any sequence with an even number of 1s
In[]:=
VertexList[ResourceFunction["TokenEventGraph"][{x_,y_}:>{Join[x,y],Join[y,x]},{{1,0},{0,1}},3]]
Out[]=
{{1,0},{0,1},{0,1,1,0},{1,0,0,1},{0,1,1,0,1,0,0,1},{1,0,0,1,0,1,1,0},{0,1,1,0,1,0,0,1,1,0,0,1,0,1,1,0},{1,0,0,1,0,1,1,0,0,1,1,0,1,0,0,1},{Event,1,1},{Event,1,2},{Event,1,3}}
In[]:=
ResourceFunction["TokenEventGraph"][{x_,y_}:>{Join[x,y],Join[y,x],x,y},{{1,0},{0,1}},3,"TokenRenderingFunction"->Row,"TokenLabeling"->None,VertexLabels->Placed["Name",Tooltip]]
Out[]=
In[]:=
Select[VertexList[%],AllTrue[IntegerQ]]
Out[]=
In[]:=
FromDigits[#,2]&/@%
Out[]=
{2,1,6,9,22,25,26,37,38,41,105,150,86,89,90,101,102,106,149,153,154,165,166,169,358,361,406,409,410,421,422,425,598,601,602,613,614,617,662,665,1433,1434,1445,1446,1449,1622,1626,1637,1638,1641,1686,1689,1701,1702,1705,2390,2393,2394,2406,2409,2454,2457,2458,2469,2473,2646,2649,2650,2661,2662,5737,5782,6505,6550,6742,6745,6746,6757,6758,6761,6806,9577,9622,9625,9626,9637,9638,9641,9833,9878,10601,10646,27030,38505}
In[]:=
Total/@%191
Out[]=
{1,1,2,2,3,3,3,3,3,3,4,4,4,4,4,4,4,4,4,4,4,4,4,4,5,5,5,5,5,5,5,5,5,5,5,5,5,5,5,5,6,6,6,6,6,6,6,6,6,6,6,6,6,6,6,6,6,6,6,6,6,6,6,6,6,6,6,6,6,6,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,8,8}
In[]:=
ResourceFunction["TokenEventGraph"][{x_,y_}:>{Join[x,y],Join[y,x],x,y},{{1,0},{0,1}},2,"TokenRenderingFunction"->Row]
Out[]=
In[]:=
UndirectedGraph[%195,GraphLayout"SpringElectricalEmbedding"]
Out[]=
We must only get sequences with the same number of 0s and 1s

How to make a global multiway system?

The states are orderless sets of the tokens [ foliation would pick out particular sequences of sets ]
At each step, from the set of tokens, we’re picking up pairs ... and then making triples of tokens from these....
Is it a problem that the generated nodes don’t contain all history?
Including the set itself...

Knitting in the WM Case

TEG Entailment Models

Strings [ tokens are characters ]
Numbers ?
Hypergraphs [tokens are sequences of symbols]
Expression hypergraphs [tokens are trees of symbols]

Tree-Edged Hypergraphs

Arborograph

Dendrograph

Expression hypergraph

Interexpression graph

[ shared common subexpression hypergraph ]