In[]:=
ResourceFunction["FindFiniteModels"][x∘y==(y∘x)∘y,2]
Out[]=
{0}SmallCircle{{0,0},{0,0}},{1}SmallCircle{{0,0},{0,1}},{5}SmallCircle{{0,1},{0,1}},{7}SmallCircle{{0,1},{1,1}},{10}SmallCircle{{1,0},{1,0}},{15}SmallCircle{{1,1},{1,1}}
In[]:=
ResourceFunction["FindFiniteModels"][(a∘((b∘a)∘(a∘b)))∘a==b∘a,2]
Out[]=
{0}SmallCircle{{0,0},{0,0}},{1}SmallCircle{{0,0},{0,1}},{5}SmallCircle{{0,1},{0,1}},{7}SmallCircle{{0,1},{1,1}},{10}SmallCircle{{1,0},{1,0}},{15}SmallCircle{{1,1},{1,1}}
For a theorem to be true in a given axiom, it is necessary (but not sufficient) for the theorem to be true for that model
ApplyFiniteModel
In[]:=
Graph[MultiwayRulesNestGraph[x_∘y_<->(y_∘x_)∘y_,(a∘b)∘a,3],VertexShapeFunctionAutomatic,GraphLayout"LayeredDigraphEmbedding"]
Out[]=
In[]:=
Graph[MultiwayRulesNestGraph[x_∘y_<->(y_∘x_)∘y_,(a∘b)∘a,3],VertexShapeFunctionAutomatic,GraphLayout{"LayeredDigraphEmbedding","RootVertex"->(a∘b)∘a}]
Out[]=
In[]:=
Graph[MultiwayRulesNestGraph[x_∘y_<->(y_∘x_)∘y_,(a∘b)∘a,3],GraphLayout"LayeredDigraphEmbedding",AspectRatio1/2]
Out[]=

Here all nodes will have the same “model coloring”

In[]:=
With[{g=Graph[MultiwayRulesNestGraph[x_∘y_<->(y_∘x_)∘y_,(a∘b)∘a,3],GraphLayout"LayeredDigraphEmbedding",VertexShapeFunctionAutomatic,AspectRatio1/2]},Graph[g,VertexLabels->(#->FromDigits[Flatten[ApplyFiniteModel[#,SmallCircle->{{0,1},{0,1}},{a,b,c}]],2]&/@VertexList[g])]]
Out[]=
When the model isn’t a model of the axioms, the results can be different:
In[]:=
With[{g=Graph[MultiwayRulesNestGraph[x_∘y_<->(y_∘x_)∘y_,(a∘b)∘a,3],GraphLayout"LayeredDigraphEmbedding",VertexShapeFunctionAutomatic,AspectRatio1/2]},Graph[g,VertexLabels->(#->FromDigits[Flatten[ApplyFiniteModel[#,SmallCircle->{{1,1},{1,0}},{a,b,c}]],2]&/@VertexList[g])]]
Out[]=
In[]:=
Function[mm,Labeled[With[{g=Graph[MultiwayRulesNestGraph[x_∘y_<->(y_∘x_)∘y_,(a∘b)∘a,3],GraphLayout"LayeredDigraphEmbedding",VertexShapeFunctionAutomatic,AspectRatio1/2]},Graph[g,VertexLabels->(#->FromDigits[Flatten[ApplyFiniteModel[#,SmallCircle->mm,{a,b,c}]],2]&/@VertexList[g])]],FromDigits[Flatten[mm],2]]]/@Tuples[{0,1},{2,2}]
Out[]=

0
,
1
,
2
,
3
,
4
,
5
,
6
,
7
,
8
,
9
,
10
,
11
,
12
,
13
,
14
,
15


In the sea of all possible expressions, those that appear in the entailment cone must have the same model signature......

If two expressions are in the same entailment cone, they must have the same signature wrt a model of a particular size.....

Note this is using transitive closure, so each edge might be a “multistop edge” [that has a waypoint with larger leaf count]

Entailment/proof structure:

“Which expressions are equal [wrt this axiom system] in the sea of all possible expressions”

If we can find a valid global model, then we can use this to guess equalities that might (or might not) later be proved by entailment
The observer combines things which agree according to a model ... even if they are not in fact entailed...
If the observer has the wrong model, this will somehow be discovered/shredded by the entailments......
Invalid model:
An observer puts in a single equivalence class everything with a particular value under their chosen model... But now entailment could show that items in the same observer equivalence class are not connected. I.e. starting from the region of metamathematical space defined by the observer’s model, there could “tubes going to different places” [in the sense that they go to different observer equivalence classes] ... so the observer will see that their model was wrong.......
Make a list of expressions that start as “48s” ... see what model they go to on successive steps.... If the observer has a correct model, nothing will ever go to a different to a value different from the one it started with....
Start with a particular model. Take all initial expressions, and work out their values. Now look at what values those lead to in subsequent steps..... We could make a “value transition graph” where the nodes are values [i.e. are equivalence classes from the observer] As community plot, we should either see all entailment connections being within a single community, or we should see “hopping”

Accumulative case

In the accumulative entailment cone, we can ask what the “model spectrum” is for each node.....
And ... entailment will preserve the model spectrum
These numbers must be non-decreasing:
[[[ NOTE: the only reason this isn’t looking 2-way is because the initial axiom isn’t canonicalized ]]]

All possible axioms:

Starting from a given axiom, things only “fill in”

Entailment fabric

Want to build accumulative entailment cones from different axioms, and see how they overlap...
Any given axiom will have certain models [and a certain entailment code] ... and certain theorems that are true. The entailment fabric knits the cones together by their common theorems. We can color by their “values under a model”
Start from all possible axioms ... and ask what common theorems they make

< Mistake: False should be all white > [ or : just remove axioms without ∘ ]

We should be distinguishing: no models involving a small circles, and no models at all.....

Effectively there is an “energy function”: nondecreasing model signature [due to the transitive-closure-like accumulativity]

[ If there is a loop, everything has to have the same model signature ]

[ Things are timelike separated when they have “increasing model signatures” ]