[[ See also Metamathematics-25 ]]
[[ See also Metamathematics-25 ]]
a==b∘a
a==b∘a
In[]:=
ResourceFunction["FindFiniteModels"][a==b∘a,2]
Out[]=
{5}SmallCircle{{0,1},{0,1}}
In[]:=
ResourceFunction["FindFiniteModels"][a==b∘a,3]
Out[]=
{3785}SmallCircle{{0,1,2},{0,1,2},{0,1,2}}
In[]:=
ResourceFunction["FindFiniteModels"][a==b∘a,4]
Out[]=
{454761243}SmallCircle{{0,1,2,3},{0,1,2,3},{0,1,2,3},{0,1,2,3}}
In[]:=
ApplyFiniteModel[expr_,op_->model_,vars_]:=Table[expr/.(op->(model[[#1+1,#2+1]]&)),##]&@@({#,0,Length[model]-1}&/@vars)
In[]:=
ApplyFiniteModel[a∘(b∘(c∘d)),SmallCircle->{{0,1},{0,1}},{a,b,c,d,e}]
Out[]=
{{{{{0,0},{1,1}},{{0,0},{1,1}}},{{{0,0},{1,1}},{{0,0},{1,1}}}},{{{{0,0},{1,1}},{{0,0},{1,1}}},{{{0,0},{1,1}},{{0,0},{1,1}}}}}
In[]:=
ApplyFiniteModel[e∘d,SmallCircle->{{0,1},{0,1}},{a,b,c,d,e}]
Out[]=
{{{{{0,0},{1,1}},{{0,0},{1,1}}},{{{0,0},{1,1}},{{0,0},{1,1}}}},{{{{0,0},{1,1}},{{0,0},{1,1}}},{{{0,0},{1,1}},{{0,0},{1,1}}}}}
a∘(b∘(c∘d))==e∘d
In[]:=
AccumulativeTokenEventGraph[a_<->b_∘a_,1,"S"]
Out[]=
In[]:=
VertexList[AccumulativeTokenEventGraph[a_<->b_∘a_,1,"S"],_TwoWayRule]/.p_Pattern:>First[p]
Out[]=
{ab∘a,aa,ab∘(c∘a),a(b∘c)∘a,a∘bc∘b}
In[]:=
AccumulativeTokenEventGraph[a_<->b_∘a_,2,"S",AspectRatio->1/2]
Out[]=
In[]:=
VertexList[%,_TwoWayRule]
Out[]=
{a_b_∘a_,a_a_,a_b_∘(c_∘a_),a_(b_∘c_)∘a_,a_∘b_c_∘b_,a_b_∘(c_∘(d_∘a_)),a_b_∘(c_∘(d_∘(e_∘a_))),a_b_∘(c_∘((d_∘e_)∘a_)),a_b_∘((c_∘d_)∘a_),a_b_∘((c_∘d_)∘(e_∘a_)),a_b_∘((c_∘(d_∘e_))∘a_),a_b_∘(((c_∘d_)∘e_)∘a_),a_(b_∘c_)∘(d_∘a_),a_(b_∘c_)∘(d_∘(e_∘a_)),a_(b_∘c_)∘((d_∘e_)∘a_),a_(b_∘(c_∘d_))∘a_,a_(b_∘(c_∘d_))∘(e_∘a_),a_(b_∘(c_∘(d_∘e_)))∘a_,a_(b_∘((c_∘d_)∘e_))∘a_,a_((b_∘c_)∘d_)∘a_,a_((b_∘c_)∘d_)∘(e_∘a_),a_((b_∘c_)∘(d_∘e_))∘a_,a_((b_∘(c_∘d_))∘e_)∘a_,a_(((b_∘c_)∘d_)∘e_)∘a_,b_a_∘b_,c_a_∘(b_∘c_),c_(a_∘b_)∘c_,a_∘b_c_∘(d_∘b_),a_∘b_c_∘(d_∘(e_∘b_)),a_∘b_c_∘((d_∘e_)∘b_),a_∘b_(c_∘d_)∘b_,a_∘b_(c_∘d_)∘(e_∘b_),a_∘b_(c_∘(d_∘e_))∘b_,a_∘b_((c_∘d_)∘e_)∘b_,a_∘(b_∘c_)d_∘c_,a_∘(b_∘c_)d_∘(e_∘c_),a_∘(b_∘c_)(d_∘e_)∘c_,a_∘(b_∘(c_∘d_))e_∘d_,a_∘((b_∘c_)∘d_)e_∘d_,d_∘c_(a_∘b_)∘c_,d_∘(e_∘c_)(a_∘b_)∘c_,e_∘d_(a_∘b_)∘(c_∘d_),e_∘d_(a_∘(b_∘c_))∘d_,e_∘d_((a_∘b_)∘c_)∘d_,(a_∘b_)∘c_(d_∘e_)∘c_}
In[]:=
%/.p_Pattern:>First[p]
Out[]=
{ab∘a,aa,ab∘(c∘a),a(b∘c)∘a,a∘bc∘b,ab∘(c∘(d∘a)),ab∘(c∘(d∘(e∘a))),ab∘(c∘((d∘e)∘a)),ab∘((c∘d)∘a),ab∘((c∘d)∘(e∘a)),ab∘((c∘(d∘e))∘a),ab∘(((c∘d)∘e)∘a),a(b∘c)∘(d∘a),a(b∘c)∘(d∘(e∘a)),a(b∘c)∘((d∘e)∘a),a(b∘(c∘d))∘a,a(b∘(c∘d))∘(e∘a),a(b∘(c∘(d∘e)))∘a,a(b∘((c∘d)∘e))∘a,a((b∘c)∘d)∘a,a((b∘c)∘d)∘(e∘a),a((b∘c)∘(d∘e))∘a,a((b∘(c∘d))∘e)∘a,a(((b∘c)∘d)∘e)∘a,ba∘b,ca∘(b∘c),c(a∘b)∘c,a∘bc∘(d∘b),a∘bc∘(d∘(e∘b)),a∘bc∘((d∘e)∘b),a∘b(c∘d)∘b,a∘b(c∘d)∘(e∘b),a∘b(c∘(d∘e))∘b,a∘b((c∘d)∘e)∘b,a∘(b∘c)d∘c,a∘(b∘c)d∘(e∘c),a∘(b∘c)(d∘e)∘c,a∘(b∘(c∘d))e∘d,a∘((b∘c)∘d)e∘d,d∘c(a∘b)∘c,d∘(e∘c)(a∘b)∘c,e∘d(a∘b)∘(c∘d),e∘d(a∘(b∘c))∘d,e∘d((a∘b)∘c)∘d,(a∘b)∘c(d∘e)∘c}
In[]:=
Map[ApplyFiniteModel[#,SmallCircle->{{0,1},{0,1}},{a,b,c,d,e}]&,%680,{2}]/.TwoWayRule->Equal
Out[]=
{True,True,True,True,True,True,True,True,True,True,True,True,True,True,True,True,True,True,True,True,True,True,True,True,True,True,True,True,True,True,True,True,True,True,True,True,True,True,True,True,True,True,True,True,True}
In[]:=
Map[ApplyFiniteModel[#,SmallCircle->{{0,1},{1,1}},{a,b,c,d,e}]&,%680,{2}]/.TwoWayRule->Equal
Out[]=
{False,True,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False}
In[]:=
ApplyFiniteModel[#,SmallCircle->{{0,1},{0,1}},{a,b,c}]&/@(a(b∘c)∘a)
Out[]=
{{{0,0},{0,0}},{{1,1},{1,1}}}{{{0,0},{0,0}},{{1,1},{1,1}}}
In[]:=
Grid[Transpose[{#,FromDigits[Flatten[ApplyFiniteModel[#,SmallCircle->{{0,1},{0,1}},{a,b,c}]],2]}&/@Flatten[Groupings[#,SmallCircle->2]&/@Permutations[{a,b,c}]]],Frame->All]
Out[]=
(a∘b)∘c | a∘(b∘c) | (a∘c)∘b | a∘(c∘b) | (b∘a)∘c | b∘(a∘c) | (b∘c)∘a | b∘(c∘a) | (c∘a)∘b | c∘(a∘b) | (c∘b)∘a | c∘(b∘a) |
85 | 85 | 51 | 51 | 85 | 85 | 15 | 15 | 51 | 51 | 15 | 15 |
In[]:=
Map[First/@#&,GroupBy[{#,FromDigits[Flatten[ApplyFiniteModel[#,SmallCircle->{{0,1},{0,1}},{a,b,c}]],2]}&/@Flatten[Groupings[#,SmallCircle->2]&/@Permutations[{a,b,c}]],Last]]
Out[]=
85{(a∘b)∘c,a∘(b∘c),(b∘a)∘c,b∘(a∘c)},51{(a∘c)∘b,a∘(c∘b),(c∘a)∘b,c∘(a∘b)},15{(b∘c)∘a,b∘(c∘a),(c∘b)∘a,c∘(b∘a)}
In[]:=
DeleteCases[Flatten[Outer[Equal,#,#]],True]&/@%699
Out[]=
85{(a∘b)∘ca∘(b∘c),(a∘b)∘c(b∘a)∘c,(a∘b)∘cb∘(a∘c),a∘(b∘c)(a∘b)∘c,a∘(b∘c)(b∘a)∘c,a∘(b∘c)b∘(a∘c),(b∘a)∘c(a∘b)∘c,(b∘a)∘ca∘(b∘c),(b∘a)∘cb∘(a∘c),b∘(a∘c)(a∘b)∘c,b∘(a∘c)a∘(b∘c),b∘(a∘c)(b∘a)∘c},51{(a∘c)∘ba∘(c∘b),(a∘c)∘b(c∘a)∘b,(a∘c)∘bc∘(a∘b),a∘(c∘b)(a∘c)∘b,a∘(c∘b)(c∘a)∘b,a∘(c∘b)c∘(a∘b),(c∘a)∘b(a∘c)∘b,(c∘a)∘ba∘(c∘b),(c∘a)∘bc∘(a∘b),c∘(a∘b)(a∘c)∘b,c∘(a∘b)a∘(c∘b),c∘(a∘b)(c∘a)∘b},15{(b∘c)∘ab∘(c∘a),(b∘c)∘a(c∘b)∘a,(b∘c)∘ac∘(b∘a),b∘(c∘a)(b∘c)∘a,b∘(c∘a)(c∘b)∘a,b∘(c∘a)c∘(b∘a),(c∘b)∘a(b∘c)∘a,(c∘b)∘ab∘(c∘a),(c∘b)∘ac∘(b∘a),c∘(b∘a)(b∘c)∘a,c∘(b∘a)b∘(c∘a),c∘(b∘a)(c∘b)∘a}
In[]:=
First[%]
Out[]=
{(a∘b)∘ca∘(b∘c),(a∘b)∘c(b∘a)∘c,(a∘b)∘cb∘(a∘c),a∘(b∘c)(a∘b)∘c,a∘(b∘c)(b∘a)∘c,a∘(b∘c)b∘(a∘c),(b∘a)∘c(a∘b)∘c,(b∘a)∘ca∘(b∘c),(b∘a)∘cb∘(a∘c),b∘(a∘c)(a∘b)∘c,b∘(a∘c)a∘(b∘c),b∘(a∘c)(b∘a)∘c}
In[]:=
Map[If[Head[#]===Failure,Infinity,#["ProofLength"]]&,ParallelMap[FindEquationalProof[#,ForAll[{a,b},a==b∘a]]&,#]]&/@%702
Out[]=
85{4,4,4,4,4,4,4,4,4,4,4,4},51{4,4,4,4,4,4,4,4,4,4,4,4},15{4,4,4,4,4,4,4,4,4,4,4,4}
In[]:=
Map[If[Head[#]===Failure,Infinity,#["ProofLength"]]&,ParallelMap[FindEquationalProof[#,ForAll[{a,b},a==b∘a]]&,#]]&/@(DeleteCases[Flatten[Outer[Equal,#,#]],True]&/@Map[First/@#&,GroupBy[{#,FromDigits[Flatten[ApplyFiniteModel[#,SmallCircle->{{0,1},{0,1}},{a,b,c}]],2]}&/@Flatten[Groupings[#,SmallCircle->2]&/@Permutations[{a,b,c,a}]],Last]])
Out[]=
In[]:=
Map[If[Head[#]===Failure,Infinity,#["ProofLength"]]&,ParallelMap[FindEquationalProof[#,ForAll[{a,b},a==b∘a]]&,#]]&/@(DeleteCases[Flatten[Outer[Equal,#,#]],True]&/@Map[First/@#&,GroupBy[{#,FromDigits[Flatten[ApplyFiniteModel[#,SmallCircle->{{0,1},{0,1}},{a,b}]],2]}&/@AllExprs[{a,b},3],Last]])
Out[]=
3{3,3,3,4,3,4,3,4,3,4,3,4,4,3,4,3,4,3,4,5,3,4,4,5,4,3,4,3,4,3,3,4,4,4,4,4,4,4,4,5,4,3,5,4,5,4,4,4,5,6,3,4,4,4,5,4,4,4,4,4,4,3,3,4,4,4,4,4,4,4,3,4,4,4,4,4,4,4,4,5,4,3,3,4,4,4,4,4,4,4,3,4,4,4,5,4,4,4,4,4,4,5,3,5,6,4,4,5,4,4},5{3,3,3,4,3,4,3,4,3,4,3,4,4,3,4,3,4,3,4,5,3,4,4,5,4,3,4,3,4,3,3,4,4,4,4,4,4,4,4,5,4,3,5,4,5,4,4,4,5,6,3,4,4,4,5,4,4,4,4,4,4,3,3,4,4,4,4,4,4,4,3,4,4,4,4,4,4,4,4,5,4,3,3,4,4,4,4,4,4,4,3,4,4,4,5,4,4,4,4,4,4,5,3,5,6,4,4,5,4,4}
In[]:=
Map[If[Head[#]===Failure,Infinity,#["ProofLength"]]&,ParallelMap[FindEquationalProof[#,ForAll[{a,b},a==b∘a]]&,#]]&/@(DeleteCases[Flatten[Outer[Equal,#,#]],True]&/@Map[First/@#&,GroupBy[{#,FromDigits[Flatten[ApplyFiniteModel[#,SmallCircle->{{0,1},{0,1}},{a,b}]],2]}&/@AllExprs[{a,b},4],Last]])
x∘ y==(y∘x)∘y
x∘ y==(y∘x)∘y
Looking for non-proof-agreeing models
Looking for non-proof-agreeing models
In NKS https://www.wolframscience.com/nks/notes-12-9--searching-for-logic-axioms/ given axiom systems, which models satisfy them.
Wanted: a case where all models [up to a certain size] agree on what expressions should be equivalent, but some of the expressions actually aren’t proof-theoretically equivalent