## Formulating axioms as combinator rules

Formulating axioms as combinator rules

s[k[s]][s[k[s[k[s]]]][k]]

Nest[s[s[k[s]][k]],s[k],n]

{s[x_][y_][z_]->x[z][y[z]],k[x_][y_]->x}

#### Semigroup theory in combinators?

Semigroup theory in combinators?

For some combinator “dot” this would be true for all subtrees a, b, c

dot[a][dot[b][c]]==dot[dot[a][b]][c]

Equality can be thought of in terms of expression paths here....

### The idea of relations is an axiomatic-level idea

The idea of relations is an axiomatic-level idea

is a knitting of expressions which is basically “spatial”

### Two things end up being equivalent if they evolve to the same thing...

Two things end up being equivalent if they evolve to the same thing...

#### Univalence they can be considered equal

Univalence they can be considered equal

### Coarse-graining an evolution graph ⟶ an equivalence statement

Coarse-graining an evolution graph ⟶ an equivalence statement

### Do equivalence statements combine e.g. by substitution inevitably?

Do equivalence statements combine e.g. by substitution inevitably?

In the graph, AA == BAAB

In[]:=

Graph[With[{g=Graph[ResourceFunction["MultiwaySystem"][{"A""AA","A""BAAB"},"A",5,"StatesGraphStructure"],AspectRatio->1.5]},GraphUnion@@(PathGraph[#,DirectedEdgesTrue]&/@FindPath[g,"A","BAABAABAAB",All,All])],VertexLabelsAutomatic]

Out[]=

If AA==BAAB and AA == AAA what follows?

#### How do we derive laws of inference for statements [i.e. entailment for statements]

How do we derive laws of inference for statements [i.e. entailment for statements]

#### Assume that equality/two-way-ruleness is just shared future

Assume that equality/two-way-ruleness is just shared future

The evolutions converge:

e[x]==e[y]

We will write this as: x == y or x y

e[x]==e[y],e[a]==e[b]

e["AA"]==e["BAAB"]

e["AA"]==e["AAA"]

Usually substitution would imply

e["AAA"]==e["BAAB"]

If a and b converge to the same thing, and b and c converge to the same thing, does it follow that a and c must converge to the same thing?