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