# x+y y +x (and associativity)

x+y y +x (and associativity)

## Applying the axiom to expressions (making a multiway graph)

Applying the axiom to expressions (making a multiway graph)

In[]:=

NestGraph[Flatten[{Values[substitutionLemmas[#,x_⊕y_y_⊕x_]]}]&,(a⊕b)⊕(c⊕d),5,VertexLabelsAutomatic,GraphLayout"LayeredDigraphEmbedding",AspectRatio1]

Out[]=

In[]:=

Graph[ResourceFunction["MultiwayFunctionSystem"][Values[substitutionLemmas[#,x_⊕y_y_⊕x_]]&,(a⊕b)⊕(c⊕d),5,"StatesGraph"],GraphLayout"LayeredDigraphEmbedding",AspectRatio1]

Out[]=

In[]:=

With[{g=NestGraph[Flatten[{Values[substitutionLemmas[#,x_⊕y_y_⊕x_]]}]&,(a⊕b)⊕(c⊕d),5,VertexLabelsAutomatic]},HighlightGraph[g,Style[PathGraph[FindShortestPath[g,(a⊕b)⊕(c⊕d),(d⊕c)⊕(b⊕a)],DirectedEdgesTrue],Red,Thick],GraphLayout"LayeredDigraphEmbedding",AspectRatio1]]

Out[]=

Note that there are multiple proofs of the same result....

In[]:=

With[{g=NestGraph[Flatten[{Values[substitutionLemmas[#,x_⊕y_y_⊕x_]]}]&,(a⊕b)⊕(c⊕d),5,VertexLabelsAutomatic]},FindShortestPath[g,(a⊕b)⊕(c⊕d),(d⊕c)⊕(b⊕a)]]//Column

Out[]=

(a⊕b)⊕(c⊕d) |

(a⊕b)⊕(d⊕c) |

(b⊕a)⊕(d⊕c) |

(d⊕c)⊕(b⊕a) |

In[]:=

Labeled[c,Style[x,Small]]⊕Labeled[d,Style[y,Small]]

Out[]=

x |

y |

[[[[ This is self-applied, so doesn’t work ]]]]

In[]:=

TwoWayMultiReplaceGraphList[{x_⊕y_y_⊕x_},3,"CoSubstitutionLemmas"->False,"Deduplicate"->True,"Canonicalize"->False,"RuleSelectionFunction"->(Tuples[{Range[1],Range@Length@#}]&)]

Out[]=

,

,

,

In[]:=

TwoWayMultiReplaceGraphList[{x_⊕y_y_⊕x_,(a⊕b)⊕(c⊕d)<->True},5,"CoSubstitutionLemmas"->False,"Deduplicate"->True,"Canonicalize"->False,"RuleSelectionFunction"->(Append[DeleteCases[Tuples[{Range[1],Range@Length@#}],{1,1}],{2,2}]&)]

Out[]=

,

,

,

,

,

In[]:=

VertexList

Out[]=

{(a⊕b)⊕(c⊕d)True,TrueTrue,(a⊕b)⊕(c⊕d)(a⊕b)⊕(c⊕d),(b⊕a)⊕(c⊕d)(a⊕b)⊕(c⊕d),x_⊕y_y_⊕x_,(a⊕b)⊕(d⊕c)(a⊕b)⊕(c⊕d),(c⊕d)⊕(a⊕b)(a⊕b)⊕(c⊕d),True(a⊕b)⊕(c⊕d),(c⊕d)⊕(a⊕b)(b⊕a)⊕(c⊕d),(c⊕d)⊕(a⊕b)(a⊕b)⊕(d⊕c),(c⊕d)⊕(a⊕b)True,(d⊕c)⊕(a⊕b)(a⊕b)⊕(c⊕d),(c⊕d)⊕(b⊕a)(a⊕b)⊕(c⊕d),(c⊕d)⊕(a⊕b)(c⊕d)⊕(a⊕b),(b⊕a)⊕(c⊕d)(b⊕a)⊕(c⊕d),(b⊕a)⊕(c⊕d)(a⊕b)⊕(d⊕c),(a⊕b)⊕(c⊕d)(a⊕b)⊕(d⊕c),True(a⊕b)⊕(d⊕c),(d⊕c)⊕(a⊕b)(a⊕b)⊕(d⊕c),(c⊕d)⊕(b⊕a)(a⊕b)⊕(d⊕c),(c⊕d)⊕(a⊕b)(b⊕a)⊕(d⊕c),(c⊕d)⊕(a⊕b)(d⊕c)⊕(a⊕b),(a⊕b)⊕(c⊕d)(c⊕d)⊕(a⊕b),(a⊕b)⊕(d⊕c)(a⊕b)⊕(d⊕c),(a⊕b)⊕(c⊕d)(d⊕c)⊕(a⊕b),(a⊕b)⊕(c⊕d)(c⊕d)⊕(b⊕a),(a⊕b)⊕(c⊕d)(b⊕a)⊕(c⊕d),(a⊕b)⊕(c⊕d)(b⊕a)⊕(d⊕c)}

#### Including associativity

Including associativity

In[]:=

Graph[ResourceFunction["MultiwayFunctionSystem"][Values[substitutionLemmas[#,x_⊕(y_⊕z_)(x_⊕y_)⊕z_]]&,(a⊕b)⊕(c⊕d),5,"StatesGraph"],GraphLayout"LayeredDigraphEmbedding",AspectRatio1]

Out[]=

### Applying to Expressions, but Generating Variables

Applying to Expressions, but Generating Variables

[[ Any time you’re not just rearranging structure, you potentially have to generate variables ]]

[ Similar issue to generating atoms of space ]

[ Similar issue to generating atoms of space ]

This is generating the same literal x_ every time

(it is not a constant because it still matches ... but all instances of x_ have to match the same thing)

(it is not a constant because it still matches ... but all instances of x_ have to match the same thing)

This uses a constant a :

[[ This has both a and a_ ]]

#### [A two-way rule will have the variables-need-to-be-generated issue in a way that one-way rules will not]

[A two-way rule will have the variables-need-to-be-generated issue in a way that one-way rules will not]

### Boolean algebra example

Boolean algebra example

Trying to establish:

## Applying the Axioms to Statements

Applying the Axioms to Statements

This is a code ≠ data situation: the axiom are the code, the statements are the data ... but now the code and data are basically in the same format....

Typical statement:

[ A not very useful statement ]

#### Self-applying to the axiom

Self-applying to the axiom

Canonicalize under pattern/variable renaming:

## Accumulative

Accumulative

[[[ Not very natural without TEGs ... ]]] [ Effectively what one would do is collect every statement into a single state on which to apply a rule that picks up pairs of statements ]

## Purely Self Applying [aka the “Gas of Statements”]

Purely Self Applying [aka the “Gas of Statements”]

#### self-applying == “bootstrapping”

self-applying == “bootstrapping”

(AKA “pool of statements”, “vat of statements”, ...)

These are “actually generated” statements (living in metamathematical space) .... as opposed to statements which are syntactic but which don’t necessarily get generated

#### Start with initial statements, then let them “interact”

Start with initial statements, then let them “interact”

#### The token-event graph is “naturally accumulative”

The token-event graph is “naturally accumulative”

[[ Not such a useful deduplication ]]

In this case, the universe ends........

#### Variable generating case:

Variable generating case:

#### In each case, we can get the pure MW states graph like this:

In each case, we can get the pure MW states graph like this:

[[ Note that a ↔ a is somewhere in the middle ]]

This is too complicated:

#### E.g. Boolean algebra

E.g. Boolean algebra

The following is presumably wrong:

Possibly pure substitution is enough because there is a single variable on one side

#### Ordinary Boolean algebra

Ordinary Boolean algebra

Will pure substitution give all true statements of Boolean algebra?

# Combinator / Machine-Code Level

Combinator / Machine-Code Level

[[ This is below standard axiomatic mathematics ]]

Start from all possible combinator expressions

with a certain “law of application”

with a certain “law of application”

Certain collection of combinator expressions can be “identified as having a meaning/purpose”

(cf recruitment of molecules for life)

(cf recruitment of molecules for life)

#### “Definitional entailment” (AKA “interpretation step”)

“Definitional entailment” (AKA “interpretation step”)

As soon as one finds a “cluster” of combinator expressions that match the LHS ... we can now identify the lumps of combinators with the specified names

How does one piggyback on the raw combinators to make a describable computation?

[cf “How do you make a switch out of magnetic bubbles” ... ]

#### In general, there are many ways to make e.g. Plus at the combinator level

In general, there are many ways to make e.g. Plus at the combinator level

The fact that there many ways to do this (and they’re decently dense in syntactic space) makes this “a robust concept”

#### This is analogous to emergent language design: i.e. if there’s a common cluster of combinators, give it a name

This is analogous to emergent language design: i.e. if there’s a common cluster of combinators, give it a name

#### Probably: syntactic density depends on reference frame

Probably: syntactic density depends on reference frame