## Minimal Models

Minimal Models

Possible distinction:

### Type 1: axioms are outside the system

Type 1: axioms are outside the system

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

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

vertices are expressions

expr1<->expr2

Proof graph: 1many

#### Case 2: propositions are vertices

Case 2: propositions are vertices

Apply an axiom to one proposition to get another

Proof graph: 1many

### Type 2: axioms are inside the system

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

Type 3: the rulial limit

All possible entailments are considered

## Minimal Model of a Type 2 Entailment

Minimal Model of a Type 2 Entailment

#### Known types:

substitutions

critical pair lemmas

? resolution

[inference rules]

Known types:

substitutions

critical pair lemmas

? resolution

[inference rules]

substitutions

critical pair lemmas

? resolution

[inference rules]

#### They take multiple hyperedges and produce hyperedges

They take multiple hyperedges and produce hyperedges

#### Is there a string version? Probably not

Is there a string version? Probably not

Minimal entailment:

StringJoin[XXX]

## String Entailments

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?

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

Knitting in the WM Case

## TEG Entailment Models

TEG Entailment Models

#### Strings [ tokens are characters ]

Numbers ?

Hypergraphs [tokens are sequences of symbols]

Expression hypergraphs [tokens are trees of symbols]

Strings [ tokens are characters ]

Numbers ?

Hypergraphs [tokens are sequences of symbols]

Expression hypergraphs [tokens are trees of symbols]

Numbers ?

Hypergraphs [tokens are sequences of symbols]

Expression hypergraphs [tokens are trees of symbols]

## Tree-Edged Hypergraphs

Tree-Edged Hypergraphs

#### Arborograph

Arborograph

#### Dendrograph

Dendrograph

#### Expression hypergraph

Expression hypergraph

#### Interexpression graph

Interexpression graph

[ shared common subexpression hypergraph ]