WOLFRAM NOTEBOOK

One-way derivations of equality

Propositions with inference

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

Propositions can be logic statements

Two-way conversion

Extensionality : A B and B A means A = B

Undirected multiway system is equivalent to a two-way directed

Generation vs. 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]
Out[]=
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

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
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.........

“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 ]

Multiway system: dynamic way of studying ensembles
E.g. simulated annealing

Wolfram Cloud

You are using a browser not supported by the Wolfram Cloud

Supported browsers include recent versions of Chrome, Edge, Firefox and Safari.


I understand and wish to continue anyway »

You are using a browser not supported by the Wolfram Cloud. Supported browsers include recent versions of Chrome, Edge, Firefox and Safari.