Relation between models and reference frames
Relation between models and reference frames
Reference frame is way of foliating the multiway graph
Reference frame is way of foliating the multiway graph
Model is a way of coloring pieces of the multiway graph that are equivalent
Model is a way of coloring pieces of the multiway graph that are equivalent
Consider the non-accumulative case
Consider the non-accumulative case
In[]:=
MultiwayRulesNestGraph[x_∘y_<->(y_∘x_)∘y_,(a∘b)∘a,3,AspectRatio->1/2]
Out[]=
A model tells us which are equal:
A model tells us which are equal:
In[]:=
symbolifyPatterns[x_∘y_<->(y_∘x_)∘y_]/.TwoWayRule->Equal
Out[]=
x∘y(y∘x)∘y
In[]:=
ResourceFunction["FindFiniteModels"][x∘y(y∘x)∘y,2]
Out[]=
{0}SmallCircle{{0,0},{0,0}},{1}SmallCircle{{0,0},{0,1}},{5}SmallCircle{{0,1},{0,1}},{7}SmallCircle{{0,1},{1,1}},{10}SmallCircle{{1,0},{1,0}},{15}SmallCircle{{1,1},{1,1}}
In[]:=
VertexList[%1410]
Out[]=
{(a∘b)∘a,b∘a,(a∘(a∘b))∘a,((b∘a)∘b)∘a,(a∘(a∘(a∘b)))∘a,(a∘((b∘a)∘b))∘a,(((a∘b)∘a)∘(a∘b))∘a,((b∘(b∘a))∘b)∘a,(((a∘b)∘a)∘b)∘a,(a∘(a∘(a∘(a∘b))))∘a,(a∘(a∘((b∘a)∘b)))∘a,(a∘(((a∘b)∘a)∘(a∘b)))∘a,(((a∘(a∘b))∘a)∘(a∘(a∘b)))∘a,(a∘((b∘(b∘a))∘b))∘a,(a∘(((a∘b)∘a)∘b))∘a,((((b∘a)∘b)∘a)∘((b∘a)∘b))∘a,((b∘(b∘(b∘a)))∘b)∘a,((b∘((a∘b)∘a))∘b)∘a,((((b∘a)∘b)∘(b∘a))∘b)∘a,(((a∘(a∘b))∘a)∘b)∘a,((((b∘a)∘b)∘a)∘b)∘a,((b∘a)∘(a∘b))∘a,(((a∘b)∘a)∘((b∘a)∘b))∘a,(((a∘b)∘((a∘b)∘a))∘(a∘b))∘a,(((a∘(a∘b))∘a)∘(a∘b))∘a,((((b∘a)∘b)∘a)∘(a∘b))∘a}
In[]:=
ApplyFiniteModel[#,SmallCircle{{0,1},{1,1}},{a,b}]&/@VertexList[%1410]
Out[]=
{{{0,1},{1,1}},{{0,1},{1,1}},{{0,1},{1,1}},{{0,1},{1,1}},{{0,1},{1,1}},{{0,1},{1,1}},{{0,1},{1,1}},{{0,1},{1,1}},{{0,1},{1,1}},{{0,1},{1,1}},{{0,1},{1,1}},{{0,1},{1,1}},{{0,1},{1,1}},{{0,1},{1,1}},{{0,1},{1,1}},{{0,1},{1,1}},{{0,1},{1,1}},{{0,1},{1,1}},{{0,1},{1,1}},{{0,1},{1,1}},{{0,1},{1,1}},{{0,1},{1,1}},{{0,1},{1,1}},{{0,1},{1,1}},{{0,1},{1,1}},{{0,1},{1,1}}}
In[]:=
ApplyFiniteModel[#,SmallCircle{{1,0},{0,0}},{a,b}]&/@VertexList[%1410]
Out[]=
{{{0,1},{0,0}},{{1,0},{0,0}},{{1,0},{0,0}},{{1,1},{0,0}},{{0,1},{0,0}},{{0,0},{0,0}},{{1,1},{0,0}},{{0,1},{0,0}},{{0,1},{0,0}},{{1,0},{0,0}},{{1,1},{0,0}},{{0,0},{0,0}},{{1,1},{0,0}},{{1,0},{0,0}},{{1,0},{0,0}},{{1,1},{0,0}},{{1,1},{0,0}},{{1,1},{0,0}},{{0,1},{0,0}},{{1,1},{0,0}},{{1,1},{0,0}},{{1,0},{0,0}},{{0,1},{0,0}},{{1,0},{0,0}},{{1,0},{0,0}},{{1,1},{0,0}}}
In[]:=
With[{g=EdgeList[MultiwayRulesNestGraph[x_∘y_<->(y_∘x_)∘y_,(a∘b)∘a,3,AspectRatio->1/2]]},Graph[g,VertexStyle->(#->Hue[FromDigits[Flatten[ApplyFiniteModel[#,SmallCircle{{1,0},{0,0}},{a,b}]],2]/20]&/@VertexList[g]),GraphLayout->"LayeredDigraphEmbedding"]]
Out[]=
In[]:=
With[{g=EdgeList[MultiwayRulesNestGraph[x_∘y_<->(y_∘x_)∘y_,(a∘b)∘a,3,AspectRatio->1/2]]},Graph[g,VertexStyle->(#->Hue[FromDigits[Flatten[ApplyFiniteModel[#,SmallCircle{{0,1},{1,1}},{a,b}]],2]/20]&/@VertexList[g]),GraphLayout->"LayeredDigraphEmbedding"]]
Out[]=
In[]:=
Function[mat,With[{g=EdgeList[MultiwayRulesNestGraph[x_∘y_<->(y_∘x_)∘y_,(a∘b)∘a,2,AspectRatio->1]]},Graph[g,AspectRatio->1,VertexSize->.2,VertexStyle->(#->Hue[FromDigits[Flatten[ApplyFiniteModel[#,SmallCirclemat,{a,b}]],2]/20]&/@VertexList[g]),GraphLayout->"LayeredDigraphEmbedding"]]]/@Tuples[{1,0},{2,2}]
Out[]=
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
In[]:=
ParallelMap[Function[mat,With[{g=EdgeList[MultiwayRulesNestGraph[x_∘y_<->(y_∘x_)∘y_,(a∘b)∘a,3,AspectRatio->1]]},Graph[g,AspectRatio->1,VertexSize->1,VertexStyle->(#->Hue[FromDigits[Flatten[ApplyFiniteModel[#,SmallCirclemat,{a,b}]],2]/20]&/@VertexList[g]),GraphLayout->"LayeredDigraphEmbedding"]]],Tuples[{1,0},{2,2}]]
Reference frames: foliations that determine what we do first in the entailment graph
Reference frames: foliations that determine what we do first in the entailment graph
E.g. make a foliation where one gets to small theorems fast
E.g. make a foliation where one gets to small theorems fast
E.g. imagine a foliation where you’re always looking at larger expressions :: this doesn’t satisfy partial order
E.g. imagine a foliation where you’re always looking at larger expressions :: this doesn’t satisfy partial order
The observer is e.g. merely saying what color things are ... that is their coarse graining
The observer is e.g. merely saying what color things are ... that is their coarse graining
The observer approximates the structure by a model, then wants to make an effective theory based on the model.
If the model is a slam dunk, then the effective theory is trivial.
If the model isn’t completely there, then the observer might still be able to make an effective theory.... [[ e.g. describe the dynamics as transitions between colors ]]
If the model is a slam dunk, then the effective theory is trivial.
If the model isn’t completely there, then the observer might still be able to make an effective theory.... [[ e.g. describe the dynamics as transitions between colors ]]
Models vs. proofs:
Models vs. proofs:
To verify a model with arity a one needs k^k^a cases [[[ one can imagine a “faithful model” that is a perfect “classification” ... all expressions that are equal have equal values and vice versa ]]]
Proof: only follow the proof path
In the expression equality case, everything is two-way
In the expression equality case, everything is two-way
Accumulative case
Accumulative case
In the accumulative case, there is a definite flow
In the accumulative case, there is a definite flow
We should draw the accumulative entailment cone ... then for a given model this cone will be colored in variegated way
Any correct model will confirm that an entailed theorem is correct....
This is an actual model....
To make a reference frame, you need a monotone function.....
To make a reference frame, you need a monotone function.....
E.g. from an expression, get a function that always increases for an entailment......
Imagine a model that maps expressions to integers
Imagine a model that maps expressions to integers
Say ∘ is Plus; say every variable is 1
Say ∘ is Plus; say every variable is 1
In this case, FWIW every integer can eventually be generated.....
[[[ Relation to CH ? ]]]
A monotonic model would be a reference frame.....
A monotonic model would be a reference frame.....
E.g. A AA