WOLFRAM NOTEBOOK

[[ See also Metamathematics-25 ]]

a==ba

In[]:=
ResourceFunction["FindFiniteModels"][a==ba,2]
Out[]=
{5}SmallCircle{{0,1},{0,1}}
In[]:=
ResourceFunction["FindFiniteModels"][a==ba,3]
Out[]=
{3785}SmallCircle{{0,1,2},{0,1,2},{0,1,2}}
In[]:=
ResourceFunction["FindFiniteModels"][a==ba,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(cd)),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[ed,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(cd))==ed
In[]:=
AccumulativeTokenEventGraph[a_<->b_a_,1,"S"]
Out[]=
In[]:=
VertexList[AccumulativeTokenEventGraph[a_<->b_a_,1,"S"],_TwoWayRule]/.p_Pattern:>First[p]
Out[]=
{aba,aa,ab(ca),a(bc)a,abcb}
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[]=
{aba,aa,ab(ca),a(bc)a,abcb,ab(c(da)),ab(c(d(ea))),ab(c((de)a)),ab((cd)a),ab((cd)(ea)),ab((c(de))a),ab(((cd)e)a),a(bc)(da),a(bc)(d(ea)),a(bc)((de)a),a(b(cd))a,a(b(cd))(ea),a(b(c(de)))a,a(b((cd)e))a,a((bc)d)a,a((bc)d)(ea),a((bc)(de))a,a((b(cd))e)a,a(((bc)d)e)a,bab,ca(bc),c(ab)c,abc(db),abc(d(eb)),abc((de)b),ab(cd)b,ab(cd)(eb),ab(c(de))b,ab((cd)e)b,a(bc)dc,a(bc)d(ec),a(bc)(de)c,a(b(cd))ed,a((bc)d)ed,dc(ab)c,d(ec)(ab)c,ed(ab)(cd),ed(a(bc))d,ed((ab)c)d,(ab)c(de)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(bc)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[]=
(ab)c
a(bc)
(ac)b
a(cb)
(ba)c
b(ac)
(bc)a
b(ca)
(ca)b
c(ab)
(cb)a
c(ba)
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{(ab)c,a(bc),(ba)c,b(ac)},51{(ac)b,a(cb),(ca)b,c(ab)},15{(bc)a,b(ca),(cb)a,c(ba)}
In[]:=
DeleteCases[Flatten[Outer[Equal,#,#]],True]&/@%699
Out[]=
85{(ab)ca(bc),(ab)c(ba)c,(ab)cb(ac),a(bc)(ab)c,a(bc)(ba)c,a(bc)b(ac),(ba)c(ab)c,(ba)ca(bc),(ba)cb(ac),b(ac)(ab)c,b(ac)a(bc),b(ac)(ba)c},51{(ac)ba(cb),(ac)b(ca)b,(ac)bc(ab),a(cb)(ac)b,a(cb)(ca)b,a(cb)c(ab),(ca)b(ac)b,(ca)ba(cb),(ca)bc(ab),c(ab)(ac)b,c(ab)a(cb),c(ab)(ca)b},15{(bc)ab(ca),(bc)a(cb)a,(bc)ac(ba),b(ca)(bc)a,b(ca)(cb)a,b(ca)c(ba),(cb)a(bc)a,(cb)ab(ca),(cb)ac(ba),c(ba)(bc)a,c(ba)b(ca),c(ba)(cb)a}
In[]:=
First[%]
Out[]=
{(ab)ca(bc),(ab)c(ba)c,(ab)cb(ac),a(bc)(ab)c,a(bc)(ba)c,a(bc)b(ac),(ba)c(ab)c,(ba)ca(bc),(ba)cb(ac),b(ac)(ab)c,b(ac)a(bc),b(ac)(ba)c}
In[]:=
Map[If[Head[#]===Failure,Infinity,#["ProofLength"]]&,ParallelMap[FindEquationalProof[#,ForAll[{a,b},a==ba]]&,#]]&/@%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==ba]]&,#]]&/@(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==ba]]&,#]]&/@(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==ba]]&,#]]&/@(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==(yx)y

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