## One-way derivations of equality

One-way derivations of equality

## Propositions with inference

Propositions with inference

#### Propositions can have a top-level Equal, which has its own rules associated with it

Propositions can have a top-level Equal, which has its own rules associated with it

#### Propositions can be logic statements

Propositions can be logic statements

## Two-way conversion

Two-way conversion

### Extensionality : A B and B A means A = B

Extensionality : A B and B A means A = B

Undirected multiway system is equivalent to a two-way directed

## Generation vs. theorem proving

Generation vs. theorem proving

## Minimal theorem proving

Minimal theorem proving

Equational multiway system

[ Proving left inverse ]

In[]:=

EquationalMultiwaySystem[{ForAll[{a,b,c},g[a,g[b,c]]g[g[a,b],c]],ForAll[a,g[a,e]a],ForAll[a,g[a,inv[a]]e]},{ForAll[a,g[inv[a],a]e]},1,"AllStatesList"]

Out[]=

{{Equal[g[inv[a], a], e]},{Equal[g[g[inv[a], a], e], e],Equal[g[g[inv[a], e], a], e],Equal[g[inv[a], a], g[e, e]],Equal[g[inv[a], a], g[$5384, inv[$5384]]],Equal[g[inv[a], g[a, e]], e],Equal[g[inv[g[a, e]], a], e],g[Equal[g[inv[a], a], e], e]}}

In[]:=

EquationalMultiwaySystem[{ForAll[{a,b,c},g[a,g[b,c]]g[g[a,b],c]],ForAll[a,g[a,e]a],ForAll[a,g[a,inv[a]]e]},{ForAll[a,g[inv[a],a]e]},1,"StatesGraph"]

Out[]=

In[]:=

EquationalMultiwaySystem[{ForAll[{a,b,c},g[a,g[b,c]]g[g[a,b],c]],ForAll[a,g[a,e]a],ForAll[a,g[a,inv[a]]e]},{ForAll[a,g[inv[a],a]e]},2,"StatesGraph"]

Out[]=

In[]:=

EquationalMultiwaySystem[ForAll[{x,y},f[x,y]f[y,x]],f[f[a,b],f[c,d]]f[f[d,c],f[b,a]],1,"StatesGraph",GraphLayout"SpringElectricalEmbedding"]

Out[]=

In[]:=

EquationalMultiwaySystem[ForAll[{x,y},f[x,y]f[y,x]],f[f[a,b],f[c,d]]f[f[d,c],f[b,a]],2,"StatesGraph",GraphLayout"SpringElectricalEmbedding"]

Out[]=

In[]:=

EquationalMultiwaySystem[ForAll[{x,y},f[x,y]f[y,x]],f[f[a,b],f[c,d]]f[f[d,c],f[b,a]],3,"StatesGraph",GraphLayout"SpringElectricalEmbedding"]

Out[]=

In[]:=

FindShortestPath[%929,ToString[FullForm[f[f[a,b],f[c,d]]f[f[d,c],f[b,a]]]],ToString[True]]

Out[]=

{Equal[f[f[a, b], f[c, d]], f[f[d, c], f[b, a]]],Equal[f[f[a, b], f[c, d]], f[f[b, a], f[d, c]]],Equal[f[f[a, b], f[c, d]], f[f[a, b], f[d, c]]],True}

In[]:=

HighlightGraph

,Style[PathGraph[{"Equal[f[f[a, b], f[c, d]], f[f[d, c], f[b, a]]]","Equal[f[f[a, b], f[c, d]], f[f[b, a], f[d, c]]]","Equal[f[f[a, b], f[c, d]], f[f[a, b], f[d, c]]]","True"},DirectedEdgesTrue],Red,Thick]

If you reach causal invariance , then you inevitably get to the True normal form

Energy ~ mathematical difficulty : counting the number of paths...

More claims...

## Homogeneity allows the possibility of completions

Homogeneity allows the possibility of completions

Disconnected branchial graphs

If a completion can be done without adding more branch pairs, then it implies that the branchial graphs can be equivalentized, i.e. methods from one area of math can be transported to another

I.e. there is a functor that goes from one category to another

Morphisms are like what is happening within a single connected piece of the multiway system; functors are like what associate different parts.

Homogeneity of mm space is what makes category theory useful: i.e. allows functorial maps to be defined.

I.e. multiway edges are like morphisms and/or like substitution lemmas

completions are like critical pair lemma and functors

completions are like critical pair lemma and functors

Sequence of completions (“patching the patch”) are like higher-order functors

Completions also map one proof to another

A category with two morphisms:

Claim: substitution lemmas are associativity of morphisms

Substitution lemmas shorten proofs ... same way that there is transitivity of morphisms

Reflexivity : a :> a [ both equality and implication satisfy this ... ]

Maybe: functors correspond to completions

## The coming world of spatial metamathematics.........

The coming world of spatial metamathematics.........

“Easy to state but difficult to prove”

Lack of correlation between spatial and branchial distances [ “failure of holography” ]

< Holography requires expressions whose structure is a bit like the multiway system >

## [ More ]

[ More ]

### Multiway system: dynamic way of studying ensembles

E.g. simulated annealing

Multiway system: dynamic way of studying ensembles

E.g. simulated annealing

E.g. simulated annealing