In[]:=
FindHigherOrderLogicProof[Exists[r,between[2,r,4]],{HoldForm[ForAll[{alpha,beta,y,z},Implies[Exists[x,Implies[And[alpha[y],beta[z]],between[x,y,z]]],Exists[u,Implies[And[alpha[y],beta[z]],between[y,u,z]]]]]],And[mid[2],end[4]],ForAll[{v,w},Exists[q,Implies[And[mid[v],end[w]],between[q,v,w]]]]}]
»
{alphaend,alphamid,betaend,betamid}
»
{}
»
{}
»
((end[y]&&end[z]between[x,y,z])(end[y]&&end[z]between[y,u,z])),mid[2]&&end[4],(mid[v]&&end[w]between[q,v,w])
∀
{y,z}
∃
x
∃
u
∀
{v,w}
∃
q
Out[]=
$Aborted
In[]:=
ResourceFunction["MultiwayOperatorSystem"][{a_Module[{b=Unique[]},CircleTimes[a,b]],CircleTimes[a_,b_]a},1,3,"CausalInvariantQ"]
Out[]=
False
In[]:=
ResourceFunction["MultiwayOperatorSystem"][{a_Module[{b=Unique[]},CircleTimes[a,b]],CircleTimes[a_,b_]a},1,2,"StatesGraph"]
Out[]=
In[]:=
Cases[0,a_,{0,Infinity},HeadsTrue]
Out[]=
{0}
In[]:=
ResourceFunction["MultiwayOperatorSystem"][{a_Module[{b},CircleTimes[a,b]]},CircleTimes[1,2],1,"StatesGraph"]
Out[]=
In[]:=
ResourceFunction["MultiwayOperatorSystem"][{a_Module[{b=Unique[]},CircleTimes[a,b]],CircleTimes[a_,b_]a},CircleTimes[1,2],1,"StatesGraph"]
Out[]=
Merging Strategies:
- Don’t merge
- Merge by (global) isomorphism (i.e. canonicalize trees)
- Merge by isomorphism with additional equations (i.e. define additional equivalences between (sub)trees) - the completion case
- Don’t merge
- Merge by (global) isomorphism (i.e. canonicalize trees)
- Merge by isomorphism with additional equations (i.e. define additional equivalences between (sub)trees) - the completion case
If edges are reversible, and hence define an equivalence relation, then completion is uncontroversial (i.e. is just a computational reduction).
(Theorem: Knuth-Bendix completion over equational rewrite systems preserves deductive closure, i.e. paths exist in the completed system if and only if they exist in the uncompleted system)
(Theorem: Knuth-Bendix completion over equational rewrite systems preserves deductive closure, i.e. paths exist in the completed system if and only if they exist in the uncompleted system)
In the non-reversible case, we can use univalence to treat the edges as though they were reversible (i.e. topos structure -> groupoid structure).
Physical interpretation: Coarse-graining (causal invariance in the eye of the beholder...)
Physical interpretation: Coarse-graining (causal invariance in the eye of the beholder...)
Hierarchy:
- Causal invariant
- Finitely completable via mathematical identities
- Finitely completable via other stuff
- Not finitely completable
- Causal invariant
- Finitely completable via mathematical identities
- Finitely completable via other stuff
- Not finitely completable
In[]:=
ResourceFunction["MultiwayOperatorSystem"][a_Module[{b=Unique[]},CircleTimes[a,b]],1,2,"EvolutionGraphStructure"]
Out[]=