From: A New Kind of Science, by Stephen Wolfram © 2002 Stephen Wolfram, LLC

The Principle of Computational Equivalence

The Validity of the Principle

({{Page 729 · Continuum and cardinality,  (page 1127)}})

Rest[FoldList[Plus,1,ContinuedFraction[x]]]

With[{x=11/13},Rest[FoldList[Plus,1,ContinuedFraction[x]]]]

With[{x=Sqrt[2]},Rest[FoldList[Plus,1,ContinuedFraction[x]]]]

Table[With[{x=Sqrt[n]},
Rest[FoldList[Plus,1,ContinuedFraction[x]]]]//Last//Length,{n,1,100}]

Position[%,0]

({{Emulating discrete systems,  (page 1129)}})

Mod[x,3]⟷1+2/3 (Cos[2/3 π (x-2)]-Cos[2 π x/3])

Table[1+2/3 (Cos[2/3 π (x-2)]-Cos[2 π x/3]),{x,0,10}]

Mod[x,4]⟷(3-2 Cos[π x/2]-Cos[π x]-2 Sin[π x/2])/2

Table[(3-2 Cos[π x/2]-Cos[π x]-2 Sin[π x/2])/2,{x,0,10}]

Mod[x,n]⟷Sum[j Product[(((Sin[π (x-i-j)/n]/Sin[π i/n]))^(  2)),{i,n-1}],{j,n-1}]

With[{n=7},Table[Sum[j Product[(((Sin[π (x-i-j)/n]/Sin[π i/n]))^(  2)),{i,n-1}],{j,n-1}],{x,0,12}]]//FullSimplify

Computational Irreducibility

({{Page 744 · Reducible systems,  (page 1134)}})

Flatten[With[{w=Max[Ceiling[Log[2,{t,x}]]]},{2 Reverse[IntegerDigits[t,2,w]]+1,5,2 IntegerDigits[x,2,w]+2}]]

With[{t=49,x=33},Flatten[With[{w=Max[Ceiling[Log[2,{t,x}]]]},{2 Reverse[IntegerDigits[t,2,w]]+1,5,2 IntegerDigits[x,2,w]+2}]]]

{{a:(1|3),1|3,_}->a,{_,2|4,a:(2|4)}->a,{3,5|10,2}->6,{1,5|7,4}->0,{3,5,4}->7,{1,6,2}->10,{1,6|11,4}->8,{3,6|8|10|11,4}->9,{3,7|9,2}->11,{1,8|11,2}->9,{3,11,2}->8,{1,9|10,4}->11,{_,a_/;a>4,_}->a,{_,_,_}->0}

CAEvolveList[rule_,init_List,t_Integer]:=NestList[CAStep[rule,#]&,init,t]
CAStep[GeneralCARule[rule_,r_Integer:1],a_List]:=Partition[a,2 r+1,1,r+1]/.rule

With[{t=49,x=33},CAEvolveList[GeneralCARule[{{a:(1|3),1|3,_}->a,{_,2|4,a:(2|4)}->a,{3,5|10,2}->6,{1,5|7,4}->0,{3,5,4}->7,{1,6,2}->10,{1,6|11,4}->8,{3,6|8|10|11,4}->9,{3,7|9,2}->11,{1,8|11,2}->9,{3,11,2}->8,{1,9|10,4}->11,{_,a_/;a>4,_}->a,{_,_,_}->0}],Flatten[With[{w=Max[Ceiling[Log[2,{t,x}]]]},{2 Reverse[IntegerDigits[t,2,w]]+1,5,2 IntegerDigits[x,2,w]+2}]],10]]

{{a:(1|3),1|3,_}->a,{_,2|4,a:(2|4)}->a,{1,5,4}->0,{_,5,_}->5,{_,_,_}->0}

CAEvolveList[rule_,init_List,t_Integer]:=NestList[CAStep[rule,#]&,init,t]
CAStep[GeneralCARule[rule_,r_Integer:1],a_List]:=Partition[a,2 r+1,1,r+1]/.rule

With[{t=49,x=33},CAEvolveList[GeneralCARule[{{a:(1|3),1|3,_}->a,{_,2|4,a:(2|4)}->a,{1,5,4}->0,{_,5,_}->5,{_,_,_}->0}],Flatten[With[{w=Max[Ceiling[Log[2,{t,x}]]]},{2 Reverse[IntegerDigits[t,2,w]]+1,5,2 IntegerDigits[x,2,w]+2}]],10]]

Undecidability and Intractability

({{Page 757 · Correspondence systems,  (page 1139)}})

StringJoin[u[[s]]]==StringJoin[v[[s]]]

Block[{u,v,s={2,3,2,2,3,2,1,1}},{u,v}=Transpose[{{"ABB","B"},{"B","BA"},{"A","B"}}];{StringJoin[u[[s]]],StringJoin[v[[s]]]}]

TSToPCP[{n_,rule_},s_]:=Map[Flatten[IntegerDigits[#,2,2]]&,Module[{f},f[u_]:=Flatten[Map[{1,#}&,3 u]];Join[Map[{f[Last[#]],RotateLeft[f[First[#]]]}&,rule],{{f[s],{1}}},Flatten[Table[{{1,2},Append[RotateLeft[f[IntegerDigits[j,2,i]]],2]},{i,0,n-1},{j,0,(2^(  i))-1}],1]]],{2}]

TSToPCP[{n_,rule_},s_]:=Map[Flatten[IntegerDigits[#,2,2]]&,Module[{f},f[u_]:=Flatten[Map[{1,#}&,3 u]];Join[Map[{f[Last[#]],RotateLeft[f[First[#]]]}&,rule],{{f[s],{1}}},Flatten[Table[{{1,2},Append[RotateLeft[f[IntegerDigits[j,2,i]]],2]},{i,0,n-1},{j,0,(2^(  i))-1}],1]]],{2}]

TSToPCP[{2,{{0,0}->{1,1},{1,0}->{},{0,1}->{1,0},{1,1}->{0,0,0}}},{0,1,1}]

Apply[Append[#2,s___]->Prepend[#1,s]&,p,{1}]

With[{p={{{0,1,1,1,0,1,1,1},{0,0,0,1,0,0,0,1}},{{},{1,1,0,1,0,0,0,1}},{{0,1,1,1,0,1,0,0},{0,0,0,1,1,1,0,1}},{{0,1,0,0,0,1,0,0,0,1,0,0},{1,1,0,1,1,1,0,1}},{{0,1,0,0,0,1,1,1,0,1,1,1},{0,1}},{{0,1,1,0},{1,0}},{{0,1,1,0},{0,0,0,1,1,0}},{{0,1,1,0},{1,1,0,1,1,0}}}},
Apply[Append[#2,s___]->Prepend[#1,s]&,p,{1}]]

({{Multiway tag systems,  (page 1141)}})

{{1,1,s___}->{s,1,0},{1,s___}->{s,1,0,1}}

MWTSEvolve[rule_,list_,t_]:=Nest[Flatten[Map[ReplaceList[#,rule]&,#],1]&,list,t]

MWTSEvolve[rule_,list_,t_]:=Nest[Flatten[Map[ReplaceList[#,rule]&,#],1]&,list,t]

MWTSEvolve[{{1,1,s___}->{s,1,0},{1,s___}->{s,1,0,1}},{{1,1}},2]

({{Word problems,  (page 1141)}})

{"CCBB"↔"BBCC","BCCCBB"↔"CBBBCC","ACCBB"↔"BBA","ABCCCBB"↔"CBBA","BBCCBBBBCC"↔"BBCCBBBBCCA"}

({{Sequence equations,  (page 1141)}})

Flatten[{x,0,x,0,y}]==Flatten[{y,x,0,y,1,0,1,0,0}]

With[{x= {1,0,1,0,0,1,0,1,0,0,1,0,1,0},y= {1,0,1,0,0,1,0,1,0,0}},Flatten[{x,0,x,0,y}]==Flatten[{y,x,0,y,1,0,1,0,0}]]

({{Fast algorithms,  (page 1141)}})

First[f[IntegerDigits[x,2,n],IntegerDigits[y,2,n],n/2]]

f[x_,y_,n_]:=If[n<1,x y,g[Partition[x,n],Partition[y,n],n]]

g[{x1_,x0_},{y1_,y0_},n_]:=With[{z1=f[x1,y1,n/2],z0=f[x0,y0,n/2]},z1 (2^(  2 n))+(f[x0+x1,y0+y1,n/2]-z1-z0) (2^(  n))+z0]

f[x_,y_,n_]:=If[n<1,x y,g[Partition[x,n],Partition[y,n],n]]
g[{x1_,x0_},{y1_,y0_},n_]:=With[{z1=f[x1,y1,n/2],z0=f[x0,y0,n/2]},z1 (2^(  2 n))+(f[x0+x1,y0+y1,n/2]-z1-z0) (2^(  n))+z0]

With[{x=1324,y=4233,n=2^4},First[f[IntegerDigits[x,2,n],IntegerDigits[y,2,n],n/2]]]

1324*4233

({{Sorting networks,  (page 1142)}})

Fold[PairSort,list,pairs]

PairSort[a_,p:{_,_}]:=Block[{t=a},t[[p]]=Sort[t[[p]]];t]

Flatten[Reverse[Flatten[With[{m=Ceiling[Log[2,n]]-1},Table[With[{d=If[i==m,(2^(  t)),(2^(  i+1))-(2^(  t))]},Map[{0,d}+#&,Select[Range[n-d],BitAnd[#-1,(2^(  t))]==If[i==m,0,(2^(  t))]&]]],{t,0,m},{i,t,m}]],1]],1]

PairSort[a_,p:{_,_}]:=Block[{t=a},t[[p]]=Sort[t[[p]]];t]

With[{n=10},Flatten[Reverse[Flatten[With[{m=Ceiling[Log[2,n]]-1},Table[With[{d=If[i==m,(2^(  t)),(2^(  i+1))-(2^(  t))]},Map[{0,d}+#&,Select[Range[n-d],BitAnd[#-1,(2^(  t))]==If[i==m,0,(2^(  t))]&]]],{t,0,m},{i,t,m}]],1]],1]]

Block[{list={1,3,2,4,1,8,3,2,4,0},n,pairs},n=Length[list]; pairs=Flatten[Reverse[Flatten[With[{m=Ceiling[Log[2,n]]-1},Table[With[{d=If[i==m,(2^(  t)),(2^(  i+1))-(2^(  t))]},Map[{0,d}+#&,Select[Range[n-d],BitAnd[#-1,(2^(  t))]==If[i==m,0,(2^(  t))]&]]],{t,0,m},{i,t,m}]],1]],1];Fold[PairSort,list,pairs]]

Sort[{1,3,2,4,1,8,3,2,4,0}]

({{Turing machines,  (page 1143)}})

Module[{s=1,a,i=1,d},a[_]=0;MapIndexed[a[#2[[1]]]=#1&,Reverse[IntegerDigits[x,2]]];Do[{s,a[i],d}={s,a[i]}/.rule;i-=d;If[i==0,Return[t]],{t,tmax}]]

With[{x=11,rule={{1,1}->{2,1,-1},{1,0}->{1,0,-1},{2,1}->{2,0,1},{2,0}->{1,0,-1}},tmax=10000},Module[{s=1,a,i=1,d},a[_]=0;MapIndexed[a[#2[[1]]]=#1&,Reverse[IntegerDigits[x,2]]];Do[{s,a[i],d}={s,a[i]}/.rule;i-=d;If[i==0,Return[t]],{t,tmax}]]]

({{Machine 1507,  (page 1144)}})

u[{Reverse[IntegerDigits[x,2]],0}]

u[list_]:=v[Split[Flatten[list]]]

v[{a_,b_:{},c_:{},d_:{},e_:{},f_:{},g___}]:=Which[a=={1}||First[a]==0,True,c=={},False,EvenQ[Length[b]],u[{a,1-b,c,d,e,f,g}],EvenQ[Length[c]],u[{a,1-b,c,1,Rest[d],e,f,g,0}],e=={}||Length[d]≥Length[b]+Length[a]-2,True,EvenQ[Length[e]],u[{a,b,c,d,f,g}],True,u[{a,1-b,c,1-d,e,1,Rest[f],g,0}]]

u[list_]:=v[Split[Flatten[list]]]
v[{a_,b_:{},c_:{},d_:{},e_:{},f_:{},g___}]:=Which[a=={1}||First[a]==0,True,c=={},False,EvenQ[Length[b]],u[{a,1-b,c,d,e,f,g}],EvenQ[Length[c]],u[{a,1-b,c,1,Rest[d],e,f,g,0}],e=={}||Length[d]≥Length[b]+Length[a]-2,True,EvenQ[Length[e]],u[{a,b,c,d,f,g}],True,u[{a,1-b,c,1-d,e,1,Rest[f],g,0}]]

With[{x=13},u[{Reverse[IntegerDigits[x,2]],0}]]

({{Machine 600720,  (page 1145)}})

{5,159,161,1021,5419,315391,1978213883,1978213885,3018415453261}

2^{3,23,24,63,148,1148,91148,91149,3560523}-1

u=Nest[(13+(6 #+8) (5/2)^IntegerExponent[6 #+8,2])/6&,1,s+1]

With[{s=3},Nest[(13+(6 #+8) (5/2)^IntegerExponent[6 #+8,2])/6&,1,s+1]]

h[{i_,j_}]:=With[{e=IntegerExponent[3 i+4,2]},{13/6+(i+4/3) (((5/2))^(  e+1)),((((154+75 (i+4/3) (((5/2))^(  e))))^(  2))-16321-7860 i-900 (i^(  2))+3360 e)/3780+j}]

h[{i_,j_}]:=With[{e=IntegerExponent[3 i+4,2]},{13/6+(i+4/3) (((5/2))^(  e+1)),((((154+75 (i+4/3) (((5/2))^(  e))))^(  2))-16321-7860 i-900 (i^(  2))+3360 e)/3780+j}]

Table[Last[Nest[h,{8,4s+24},s]]-1,{s,1,3}]

2^(b[Join[{1,1},#],Length[#]]&)[IntegerDigits[x,2]]-1

a[{l_,_},r_]:=({l+(5 r-3 #)/2,#}&)[Mod[r,2]]

a[{l_,0},0]:={l+1,0}

a[{l_,1},0]:=({(13+# (5/2)^IntegerExponent[#,2])/6,0}&)[6 l+2]

b[list_,i_]:=First[Fold[a,{Apply[Plus,Drop[list,-i]],0},Apply[Plus,Split[Take[list,-i],#1==#2≠0&],1]]]

a[{l_,_},r_]:=({l+(5 r-3 #)/2,#}&)[Mod[r,2]]
a[{l_,0},0]:={l+1,0}
a[{l_,1},0]:=({(13+# (5/2)^IntegerExponent[#,2])/6,0}&)[6 l+2]
b[list_,i_]:=First[Fold[a,{Apply[Plus,Drop[list,-i]],0},Apply[Plus,Split[Take[list,-i],#1==#2≠0&],1]]]

With[{x=FromDigits[{1,0,1,1,0,1},2]},{x,2^(b[Join[{1,1},#],Length[#]]&)[IntegerDigits[x,2]]-1}]

f[4 s]=4 s+3

f[4 s+1]=2 f[2 s]+1

f[(2^(  s))-1]=(2^(  (10 s+5+3 (((-1))^(  s)))/4))-1

({{Non-deterministic Turing machines,  (page 1146)}})

NTMEvolve[rule_,inits_,t_Integer]:=Nest[Union[Flatten[Map[NTMStep[rule,#]&,#],1]]&,inits,t]

NTMStep[rule_List,{s_,a_,n_}]/;1≤n≤Length[a]:=Apply[{#1,ReplacePart[a,#2,n],n+#3}&,Replace[{s,a[[n]]},rule],{1}]

NTMEvolve[rule_,inits_,t_Integer]:=Nest[Union[Flatten[Map[NTMStep[rule,#]&,#],1]]&,inits,t]

NTMStep[rule_List,{s_,a_,n_}]/;1≤n≤Length[a]:=Apply[{#1,ReplacePart[a,#2,n],n+#3}&,Replace[{s,a[[n]]},rule],{1}]

NTMEvolve[{{2,1}->{{2,1,1}},{2,0}->{{1,0,1},{2,1,-1}},{1,1}->{{2,1,1}},{1,0}->{{2,0,-1}}},{{1,{0,0,0,0,0,0,0,0},4}},4]

({{Page 767 · Implementation,  (page 1146)}})

NDTMToCA[tm_]:=Flatten[{{_,h,_}->h,{s,_c,_}->e,{s,_,_}->s,{_,s,c[i_]}->s[i],{_,s,x_}->x,{a[_,_],_s,_}->s,{_,a[x_,y_],s[i_]}->a[x,y,i],{x_,_s,_}->x,{_,_,s[i_]}->s[i],Map[Table[With[{b=(#[[Min[Length[#],z]]]&)[{x,#}/.tm]},If[Last[b]==-1,{{a[_],a[x,#,z],e}->h,{a[_],a[x,#,z],s}->a[x,#,z],{a[_],a[x,#,z],_}->a[b[[2]]],{a[x,#,z],a[w_],_}->a[b[[1]],w],{_,a[w_],a[x,#,z]}->a[w]},{{a[_],a[x,#,z],_}->a[b[[2]]],{a[x,#,z],a[w_],_}->a[w],{_,a[w_],a[x,#,z]}->a[b[[1]],w]}]],{x,Max[Map[#[[1,1]]&,tm]]},{z,Max[Map[Length[#[[2]]]&,tm]]}]&,Union[Map[#[[1,2]]&,tm]]],{_,x_,_}->x}]

NDTMToCA[tm_]:=Flatten[{{_,h,_}->h,{s,_c,_}->e,{s,_,_}->s,{_,s,c[i_]}->s[i],{_,s,x_}->x,{a[_,_],_s,_}->s,{_,a[x_,y_],s[i_]}->a[x,y,i],{x_,_s,_}->x,{_,_,s[i_]}->s[i],Map[Table[With[{b=(#[[Min[Length[#],z]]]&)[{x,#}/.tm]},If[Last[b]==-1,{{a[_],a[x,#,z],e}->h,{a[_],a[x,#,z],s}->a[x,#,z],{a[_],a[x,#,z],_}->a[b[[2]]],{a[x,#,z],a[w_],_}->a[b[[1]],w],{_,a[w_],a[x,#,z]}->a[w]},{{a[_],a[x,#,z],_}->a[b[[2]]],{a[x,#,z],a[w_],_}->a[w],{_,a[w_],a[x,#,z]}->a[b[[1]],w]}]],{x,Max[Map[#[[1,1]]&,tm]]},{z,Max[Map[Length[#[[2]]]&,tm]]}]&,Union[Map[#[[1,2]]&,tm]]],{_,x_,_}->x}]

NDTMToCA[{{2,1}->{{2,1,1}},{2,0}->{{1,0,1},{2,1,-1}},{1,1}->{{2,1,1}},{1,0}->{{2,0,-1}}}]

({{Page 768 · Satisfiability,  (page 1146)}})

NDTMToCNF[rules_,{s_,a_,n_},t_]:={Table[Apply[Or,Table[𝕤[i,j],{j,stot}]],{i,t-1}],Table[!𝕤[i,j]||!𝕤[i,k],{i,0,t-1},{j,stot},{k,j+1,stot}],Table[Apply[Or,Table[𝕟[i,j],{j,n+i,Max[0,n-i],-2}]],{i,0,t}],Table[!𝕟[i,j]||!𝕟[i,k],{i,0,t},{j,n+i,Max[0,n-i],-2},{k,j+2,n+i}],Table[Apply[Or,Table[𝕒[i,j,k],{k,0,ktot-1}]],{i,0,t-1},{j,Max[1,n-i],n+i}],Table[!𝕒[i,j,k]||!𝕒[i,j,m],{i,0,t-1},{j,Max[1,n-i],n+i},{k,0,ktot-1},{m,k+1,ktot-1}],𝕤[0,s],Cases[MapIndexed[𝕒[Abs[n-First[#2]],First[#2],#1]&,a],𝕒[x_,_,_]/;x<t],Table[𝕒[Abs[n-i],i,0],{i,Length[a]+1,n+t-1}],Table[!𝕒[i,j,k]||If[EvenQ[n+i-j],𝕟[i,j],False]||𝕒[i+1,j,k],{i,0,t-2},{j,Max[1,n-i],n+i},{k,0,ktot-1}],Table[Map[Function[z,Outer[!𝕟[i,j]||!𝕤[i,z[[1,1]]]||!𝕒[i,j,z[[1,2]]]||##&,Apply[Sequence,Map[If[i<t-1,{𝕤[i+1,#[[1]]],𝕟[i+1,j-#[[3]]],𝕒[i+1,j,#[[2]]]},{𝕟[i+1,j-#[[3]]]}]&,z[[2]]]]]],rules],{i,0,t-1},{j,n+i,Max[1,n-i],-2}],Apply[Or,Table[𝕟[i,0],{i,n,t,2}]]}/.List->And

NDTMToCNF[rules_,{s_,a_,n_},t_]:={Table[Apply[Or,Table[𝕤[i,j],{j,stot}]],{i,t-1}],Table[!𝕤[i,j]||!𝕤[i,k],{i,0,t-1},{j,stot},{k,j+1,stot}],Table[Apply[Or,Table[𝕟[i,j],{j,n+i,Max[0,n-i],-2}]],{i,0,t}],Table[!𝕟[i,j]||!𝕟[i,k],{i,0,t},{j,n+i,Max[0,n-i],-2},{k,j+2,n+i}],Table[Apply[Or,Table[𝕒[i,j,k],{k,0,ktot-1}]],{i,0,t-1},{j,Max[1,n-i],n+i}],Table[!𝕒[i,j,k]||!𝕒[i,j,m],{i,0,t-1},{j,Max[1,n-i],n+i},{k,0,ktot-1},{m,k+1,ktot-1}],𝕤[0,s],Cases[MapIndexed[𝕒[Abs[n-First[#2]],First[#2],#1]&,a],𝕒[x_,_,_]/;x<t],Table[𝕒[Abs[n-i],i,0],{i,Length[a]+1,n+t-1}],Table[!𝕒[i,j,k]||If[EvenQ[n+i-j],𝕟[i,j],False]||𝕒[i+1,j,k],{i,0,t-2},{j,Max[1,n-i],n+i},{k,0,ktot-1}],Table[Map[Function[z,Outer[!𝕟[i,j]||!𝕤[i,z[[1,1]]]||!𝕒[i,j,z[[1,2]]]||##&,Apply[Sequence,Map[If[i<t-1,{𝕤[i+1,#[[1]]],𝕟[i+1,j-#[[3]]],𝕒[i+1,j,#[[2]]]},{𝕟[i+1,j-#[[3]]]}]&,z[[2]]]]]],rules],{i,0,t-1},{j,n+i,Max[1,n-i],-2}],Apply[Or,Table[𝕟[i,0],{i,n,t,2}]]}/.List->And

Block[{stot=2, ktot=2},NDTMToCNF[{{1,0}->{{2,0,1},{1,0,-1}},{2,0}->{{1,0,-1}},{1,1}->{{2,0,-1}},{2,1}->{{2,1,1}}},{1,{1},1},1]]

({{Page 770 · Rule 30 inversion,  (page 1147)}})

{1,2,2,3,3,6,6,10,16,31,52,99,165,260}

{2,5,8,14,23,40,66,111,182,316,540,921,1530,2543,4122}

Implications for Mathematics and Its Foundations

({{Basic logic,  (page 1151)}})

{(¬¬a)==a,(a∨¬(b∨¬b))==a,(¬(¬(a∨¬b)∨¬(a∨¬c)))==(a∨¬(b∨c))}

{a=>(b=>a),(a=>(b=>c))=>((a=>b)=>(a=>c)),(a=>(b=>c))=>(b=>(a=>c)),(a=>b)=>((¬b)=>(¬a)),(¬¬a)=>a,a=>(¬¬a)}

{((a=>(b=>a))=>((((¬c)=>(d=>(¬e)))=>((c=>(d=>f))=>((e=>d)=>(e=>f))))=>g))=>(h=>g)}

{((¬a)=>(b=>(¬c)))=>((a=>(b=>d))=>((c=>b)=>(c=>d))),a=>(b=>a)}

Module[{a},Join[Thread[axioms==a=>a],{((a=>a)=>b)==b,((a=>b)=>b)==(b=>a)=>a}]]

With[{axioms={((¬a)\[Implies](b\[Implies](¬c)))\[Implies]((a\[Implies](b\[Implies]d))\[Implies]((c\[Implies]b)\[Implies](c\[Implies]d))),a\[Implies](b\[Implies]a)}},Module[{a},Join[Thread[axioms==a\[Implies]a],{((a\[Implies]a)\[Implies]b)==b,((a\[Implies]b)\[Implies]b)==(b\[Implies]a)\[Implies]a}]]]//TraditionalForm

{(a⊼(b⊼c))⊼((e⊼(e⊼e))⊼((d⊼b)⊼((a⊼d)⊼(a⊼d))))}

{(a⊼(b⊼c))⊼(((d⊼c)⊼((a⊼d)⊼(a⊼d)))⊼(a⊼(a⊼b)))}

Module[{a},With[{t=a⊼(a⊼a),i=#1⊼(#2⊼#2)&},Join[Thread[axioms==t],{i[t⊼(b⊼c),c]==t,i[t,b]==b,i[i[a,b],b]==i[i[b,a],a]}]]]

With[{axioms={(a⊼(b⊼c))⊼(((d⊼c)⊼((a⊼d)⊼(a⊼d)))⊼(a⊼(a⊼b)))}},Module[{a},With[{t=a⊼(a⊼a),i=#1⊼(#2⊼#2)&},Join[Thread[axioms==t],{i[t⊼(b⊼c),c]==t,i[t,b]==b,i[i[a,b],b]==i[i[b,a],a]}]]]]//TraditionalForm

({{Other algebraic systems,  (page 1153)}})

{a⋀b==b⋀a,a⋁b==b⋁a,(a⋀b)⋀c==a⋀(b⋀c),(a⋁b)⋁c==a⋁(b⋁c),a⋀(a⋁b)==a,a⋁a⋀b==a}

({{Page 775 · Implementation,  (page 1155)}})

s[1]=(a_⊼a_)⊼(a_⊼b_)->a;s[2,x_]:=b_->(b⊼b)⊼(b⊼x);

s[3]=a_⊼(a_⊼b_)->a⊼(b⊼b);s[4]=a_⊼(b_⊼b_)->a⊼(a⊼b);

s[5]=a_⊼(a_⊼(b_⊼c_))->b⊼(b⊼(a⊼c));

{{s[2,b],{2}},{s[4],{}},{s[2,(b⊼b)⊼((a⊼a)⊼(b⊼b))],{2,2}},{s[1],{2,2,1}},{s[2,b⊼b],{2,2,2,2,2,2}},{s[5],{2,2,2}},{s[2,b⊼b],{2,2,2,2,2,1}},{s[1],{2,2,2,2,2}},{s[3],{2,2,2}},{s[1],{2,2,2,2}},{s[4],{2,2,2}},{s[5],{}},{s[2,a],{2,2,1}},{s[1],{2,2}},{s[3],{}},{s[1],{2}}}

FoldList[Function[{u,v},MapAt[Replace[#,v[[1]]]&,u,{v[[2]]}]],a⊼b,proof]

s[1]=(a_⊼a_)⊼(a_⊼b_)->a;s[2,x_]:=b_->(b⊼b)⊼(b⊼x);
s[3]=a_⊼(a_⊼b_)->a⊼(b⊼b);s[4]=a_⊼(b_⊼b_)->a⊼(a⊼b);
s[5]=a_⊼(a_⊼(b_⊼c_))->b⊼(b⊼(a⊼c));

With[{proof={{s[2,b],{2}},{s[4],{}},{s[2,(b⊼b)⊼((a⊼a)⊼(b⊼b))],{2,2}},{s[1],{2,2,1}},{s[2,b⊼b],{2,2,2,2,2,2}},{s[5],{2,2,2}},{s[2,b⊼b],{2,2,2,2,2,1}},{s[1],{2,2,2,2,2}},{s[3],{2,2,2}},{s[1],{2,2,2,2}},{s[4],{2,2,2}},{s[5],{}},{s[2,a],{2,2,1}},{s[1],{2,2}},{s[3],{}},{s[1],{2}}}},
FoldList[Function[{u,v},MapAt[Replace[#,v[[1]]]&,u,{v[[2]]}]],a⊼b,proof]]

({{Page 776 · Proof structures,  (page 1155)}})

(a⊼(a⊼(b⊼((a⊼a)⊼c))))==(b⊼a)

({{Page 781 · Nand tautologies,  (page 1157)}})

Nest[(#⊼#)⊼(#⊼(Subscript[p, t]))&,p⊼(p⊼p),t-1]

With[{t=3},Nest[(#⊼#)⊼(#⊼(Subscript[p, t]))&,p⊼(p⊼p),t-1]]

Table[LeafCount[Nest[(#⊼#)⊼(#⊼(Subscript[p, t]))&,p⊼(p⊼p),t-1]],{t,13}]

Table[8*(3^(t-1))-3,{t,13}]

({{Page 784 · Algebraic axioms,  (page 1159)}})

a·x==a·y=>(x==y∧(Subscript[∃, z])a·z==x)∧a·x==b·x=>a==b∧(a·b)·x==a·(b·x)

({{Page 784 · Set theory,  (page 1160)}})

Nest[Union[#,{#}]&,{},n]

Replace[s,{(Subscript[∀, a_])b_->(Subscript[∀, a])(a∈ℕ=>b),(Subscript[∃, a_])b_->(Subscript[∃, a])(a∈ℕ∧b)},{0,∞}]

With[{n=4},Nest[Union[#,{#}]&,{},n]]

({{Page 786 · Universal Diophantine equation,  (page 1160)}})

(a==0∨b==0)⟷a b==0

(a==0∧b==0)⟷a+b==0

a<b⟷b==a+c+1

a==Mod[b,c]⟷(b==a+c d∧a<c)

a==Quotient[b,c]⟷(b==a c+d∧d<c)

a==Binomial[b,c]⟷With[{n=(2^(  b))+1},(((n+1))^(  b))==(n^(  c)) (a+d n)+e∧e<(n^(  c))∧a<n]

a==b!⟷a==Quotient[(c^(  b)),Binomial[c,b]]

a==GCD[b,c]⟷(b c>0∧a d==b∧a e==c∧a+c f==b g)

a==Floor[b/c]⟷(a c+d==b∧d<c)

PrimeQ[a]⟷(GCD[(a-1)!,a]==1∧a>1)

a==BitAnd[c,d]∧b==BitOr[c,d]⟷(σ[c,a]∧σ[d,a]∧σ[b,c]∧σ[b,d]∧a+b==c+d)/.σ[x_,y_]->Mod[Binomial[x,y],2]==1

BitXor[a,2 BitOr[a,2 a]]

BitXor[x,y]==BitOr[x,y]-BitAnd[x,y]

BitXor[BitAnd[a,2 a,4 a],BitOr[2 a,4 a]]

{1+(Subscript[x, 4])+(Subscript[x, 12])==(2^(  (1+(Subscript[x, 3])) ((Subscript[x, 1])+2 (Subscript[x, 3])))),(Subscript[x, 2])+(Subscript[x, 13])==(2^(  (Subscript[x, 1]))),1+(Subscript[x, 5])+(Subscript[x, 14])==(2^(  (Subscript[x, 1]))),(2^(  (Subscript[x, 3]))) (Subscript[x, 5])+(2^(  (Subscript[x, 1])+2 (Subscript[x, 3]))) (Subscript[x, 6])+(2^(  (Subscript[x, 1])+(Subscript[x, 3]))) (Subscript[x, 15])+(Subscript[x, 16])==(Subscript[x, 4]),1+(Subscript[x, 15])+(Subscript[x, 17])==(2^(  (Subscript[x, 3]))),1+(Subscript[x, 16])+(Subscript[x, 18])==(2^(  (Subscript[x, 3]))),(2^(  1+(Subscript[x, 3]) (1+(Subscript[x, 1])+2 (Subscript[x, 3])))) (-1+(Subscript[x, 2]))-(Subscript[x, 10])+(Subscript[x, 11])==2 (Subscript[x, 4]),(Subscript[x, 7])==BitAnd[(Subscript[x, 6]),2 (Subscript[x, 6])]∧(Subscript[x, 8])==BitOr[(Subscript[x, 6]),2 (Subscript[x, 6])],(Subscript[x, 9])==BitAnd[(Subscript[x, 6]),2 (Subscript[x, 7])]∧(Subscript[x, 19])==BitOr[(Subscript[x, 6]),2 (Subscript[x, 7])],(Subscript[x, 10])==BitAnd[(Subscript[x, 9]),2 (Subscript[x, 8])]∧(Subscript[x, 11])==BitOr[(Subscript[x, 9]),2 (Subscript[x, 8])]}

a==(b^(  c))⟷α[d,4+b e,1+z]∧α[f,e,1+z]∧a==Quotient[d,f]∧α[g,4+b,1+z]∧e==16 g (1+z)

λ[a_,b_,c_]:=Module[{x},2 a+(Subscript[x, 1])==c∧(Mod[b-a,c]==0∨Mod[b+a,c]==0)]

α[a_,b_,c_]:=Module[{x},((Subscript[x, 1])^(  2))-b (Subscript[x, 1]) (Subscript[x, 2])+((Subscript[x, 2])^(  2))==1∧((Subscript[x, 3])^(  2))-b (Subscript[x, 3]) (Subscript[x, 4])+((Subscript[x, 4])^(  2))==1∧1+(Subscript[x, 4])+(Subscript[x, 5])==(Subscript[x, 3])∧Mod[(Subscript[x, 3]),((Subscript[x, 1])^(  2))]==0∧2 (Subscript[x, 4])+(Subscript[x, 7])==b (Subscript[x, 3])∧Mod[-b+(Subscript[x, 8]),(Subscript[x, 7])]==0∧Mod[-2+(Subscript[x, 8]),(Subscript[x, 1])]==0∧(Subscript[x, 8])-(Subscript[x, 11])==3∧((Subscript[x, 12])^(  2))-(Subscript[x, 8]) (Subscript[x, 12]) (Subscript[x, 13])+((Subscript[x, 13])^(  2))==1∧1+2 a+(Subscript[x, 14])==(Subscript[x, 1])∧λ[a,(Subscript[x, 12]),(Subscript[x, 7])]∧λ[c,(Subscript[x, 12]),(Subscript[x, 1])]]

({{Statements in Peano arithmetic,  (page 1162)}})

¬(Subscript[∃, a])((Subscript[∃, b])(b≠0∧a×a==(▲▲0)×(b×b)))

¬(Subscript[∃, n])((Subscript[∀, c])((Subscript[∃, a])((Subscript[∃, b])(n+c)×(n+c)+▲0==(▲▲a)×(▲▲b))))

(Subscript[∀, a])((Subscript[∃, b])((Subscript[∃, c])((▲▲0)×(▲▲a)==b+c∧(Subscript[∀, d])((Subscript[∀, e])((Subscript[∀, f])((f==(▲▲d)×(▲▲e)∨f==▲0)=>(f≠b∧f≠c)))))))

({{Growth rates,  (page 1162)}})

𝒻[1][n_]=2 n;𝒻[s_][n_]:=Nest[𝒻[s-1],1,n]

𝒻[ω][n_]:=𝒻[n][n]

𝒻[ω+s][n_]:=Nest[𝒻[ω+s-1],1,n]

𝒻[1][n_]=2 n;𝒻[s_][n_]:=Nest[𝒻[s-1],1,n]
𝒻[ω][n_]:=𝒻[n][n]
𝒻[ω+s][n_]:=Nest[𝒻[ω+s-1],1,n]

𝒻[1][4]

𝒻[2][4]

𝒻[3][4]

({{Page 787 · Unprovable statements,  (page 1163)}})

g[n_]:=Map[First,NestWhileList[{f[#]-1,Last[#]+1}&,{n,3},First[#]>0&]]

f[{0,_}]=0;

f[{n_,k_}]:=Apply[Plus,MapIndexed[#1 k^f[{#2[[1]]-1,k}]&,Reverse[IntegerDigits[n,k-1]]]]

g[n_]:=Map[First,NestWhileList[{f[#]-1,Last[#]+1}&,{n,3},First[#]>0&]]
f[{0,_}]=0;
f[{n_,k_}]:=Apply[Plus,MapIndexed[#1 k^f[{#2[[1]]-1,k}]&,Reverse[IntegerDigits[n,k-1]]]]

g[1]

g[2]

({{Practical programs,  (page 1168)}})

First[Prepend[p,q]]===q

First[Prepend[p,q]]===q

Join[Join[p,q],r]===Join[p,Join[q,r]]

Join[Join[p,q],r]===Join[p,Join[q,r]]

Partition[Union[p],1]===Split[Union[p]]

Partition[Union[p],1]===Split[Union[p]]

({{Page 801 · Comparison to multiway systems,  (page 1169)}})

Apply[Equal,Map[Fold[#2[#1]&,x,Characters[#]]&,rules,{2}],{1}]

With[{rules={"AAB"↔"BBAA"}},Apply[Equal,Map[Fold[#2[#1]&,x,Characters[#]]&,rules,{2}],{1}]]

Append[Apply[Equal,Map[(Fold[f,First[#],Rest[#]]&)[Characters[#]]&,rules,{2}],{1}],f[f[a,b],c]==f[a,f[b,c]]]

With[{rules={"AAB"↔"BBAA"}},Append[Apply[Equal,Map[(Fold[f,First[#],Rest[#]]&)[Characters[#]]&,rules,{2}],{1}],f[f[a,b],c]==f[a,f[b,c]]]]

({{Page 802 · Operator systems,  (page 1170)}})

With[{m=Length[vars]},FromDigits[Block[{f=Reverse[IntegerDigits[u,k,(k^(  n))]][[FromDigits[{##},k]+1]]&},Apply[Function[Evaluate[vars],expr],Reverse[Array[IntegerDigits[#-1,k,m]&,(k^(  m))]],{1}]],k]]

With[{vars={p,q,r},k=2,n=2,expr=f[p,f[q,r]],u=7},With[{m=Length[vars]},FromDigits[Block[{f=Reverse[IntegerDigits[u,k,(k^(  n))]][[FromDigits[{##},k]+1]]&},Apply[Function[Evaluate[vars],expr],Reverse[Array[IntegerDigits[#-1,k,m]&,(k^(  m))]],{1}]],k]]]

({{Junctional calculus,  (page 1170)}})

Union[Level[expr,{-1}]]

{13203,15633,15663,16401,17139,18063,19539,19569,19599}

With[{expr=f[f[a,b],a]},Union[Level[expr,{-1}]]]

({{Equivalential calculus,  (page 1170)}})

Mod[Map[Count[expr,#,{-1}]&,vars],2]

With[{expr=f[f[a,b],a],vars={a,b}},Mod[Map[Count[expr,#,{-1}]&,vars],2]]

({{Implicational calculus,  (page 1170)}})

{((a∘b)∘c)∘((c∘a)∘(d∘a))==d∘d,(a∘a)∘b==b,(a∘b)∘b==(b∘a)∘a}

({{Page 803 · Operators on sets,  (page 1171)}})

{1116699,169585339,290790239,459258879,1090522958,1309671358,1430343258,1515110058,2184380593,2575151445,2863760025,2986292093}

Distribute[Map[{{},{#}}&,s],List,List,List,Join]

With[{s=Range[4]},Distribute[Map[{{},{#}}&,s],List,List,List,Join]]

({{Page 805 · Implementation,  (page 1171)}})

{f[a,f[a,a]]==a, f[a,b]==f[b,a]}

Module[{c,v},c=Apply[Function,{v=Union[Level[axioms,{-1}]],Apply[And,axioms]}];Select[Range[0,(k^(  (k^(  2))))-1],With[{u=IntegerDigits[#,k,(k^(  2))]},Block[{f},f[x_,y_]:=u[[-1-k x-y]];Array[c,Table[k,{Length[v]}],0,And]]]&]]

BitOp[a_,b_,n_]:=Partition[IntegerDigits[n,2,4],2][[2-a,2-b]]

With[{k=2,axioms={f[a,f[a,a]]==a, f[a,b]==f[b,a]}},Module[{c,v},c=Apply[Function,{v=Union[Level[axioms,{-1}]],Apply[And,axioms]}];Select[Range[0,(k^(  (k^(  2))))-1],With[{u=IntegerDigits[#,k,(k^(  2))]},Block[{f},f[x_,y_]:=u[[-1-k x-y]];Array[c,Table[k,{Length[v]}],0,And]]]&]]]

Block[{f=BitOp[#1,#2,6]&},Table[{f[a,f[a,a]]==a, f[a,b]==f[b,a]},{a,0,1},{b,0,1}]]

({{Page 806 · Algebraic systems,  (page 1171)}})

f[f[a,b,c],d,e]==f[a,f[b,c,d],e]==f[a,b,f[c,d,e]]

({{Page 806 · Groups and semigroups,  (page 1172)}})

Apply[Times,Map[PartitionsP[Last[#]]&,FactorInteger[k]]]

Table[{k,Apply[Times,Map[PartitionsP[Last[#]]&,FactorInteger[k]]]
},{k,1,20}]

({{Page 808 · Searching for logic,  (page 1174)}})

{(b∘(b∘(a∘a)))∘(a∘(b∘c)),(b∘(b∘(a∘a)))∘(a∘(c∘b)),(b∘(b∘(a∘b)))∘(a∘(b∘c)),(b∘(b∘(a∘b)))∘(a∘(c∘b)),(b∘(b∘(a∘c)))∘(a∘(c∘b)),(b∘(b∘(b∘a)))∘(a∘(b∘c)),(b∘(b∘(b∘a)))∘(a∘(c∘b)),(b∘(b∘(c∘a)))∘(a∘(b∘c)),(b∘((a∘b)∘b))∘(a∘(b∘c)),(b∘((a∘b)∘b))∘(a∘(c∘b)),(b∘((a∘c)∘b))∘(a∘(c∘b)),((b∘c)∘a)∘(b∘(b∘(a∘b))),((b∘c)∘a)∘(b∘(b∘(a∘c))),((b∘c)∘a)∘(b∘((a∘a)∘b)),((b∘c)∘a)∘(b∘((a∘b)∘b)),((b∘c)∘a)∘(b∘((a∘c)∘b)),((b∘c)∘a)∘(b∘((b∘a)∘b)),((b∘c)∘a)∘(b∘((c∘a)∘b)),((b∘c)∘a)∘(c∘(c∘(a∘b))),((b∘c)∘a)∘(c∘(c∘(a∘c))),((b∘c)∘a)∘(c∘((a∘a)∘c)),((b∘c)∘a)∘(c∘((a∘b)∘c)),((b∘c)∘a)∘(c∘((a∘c)∘c)),((b∘c)∘a)∘(c∘((b∘a)∘c)),((b∘c)∘a)∘(c∘((c∘a)∘c))}

{(a∘b)∘(a∘(b∘(a∘b))),(a∘b)∘(a∘(b∘(b∘b))),(a∘(b∘b))∘(a∘(b∘(b∘b)))}

1885760537655125429738480884

{(a∘a)∘(b∘(b∘(a∘c))),(a∘b)∘(a∘(b∘(a∘b))),(a∘b)∘(a∘(b∘(a∘c))),(a∘b)∘(a∘(b∘(b∘b))),(a∘b)∘(a∘(b∘(b∘c))),(a∘b)∘(a∘(b∘(c∘c))),(a∘b)∘(a∘(c∘(a∘c))),(a∘b)∘(a∘(c∘(c∘c)))}

({{Page 808 · History,  (page 1175)}})

{(a∘(b∘c))∘(a∘(b∘c))==((c∘a)∘a)∘((b∘a)∘a),(a∘a)∘(b∘a)==a}

{(a∘a)∘((b∘b)∘b)==a,a∘(b∘c)==(((c∘c)∘a)∘((b∘b)∘a))∘(((c∘c)∘a)∘((b∘b)∘a))}

{a∘(b∘(a∘c))==a∘(b∘(b∘c)),(a∘a)∘(b∘a)==a,a∘b==b∘a}

({{Page 814 · Proof lengths in logic,  (page 1175)}})

{(((a⊼a)⊼b)⊼b)==(((a⊼b)⊼a)⊼a),(a⊼(a⊼(a⊼a)))==(a⊼((a⊼b)⊼b)),(((a⊼a)⊼a)⊼a)==(((a⊼a)⊼b)⊼a),(((a⊼a)⊼b)⊼b)==(((a⊼b)⊼a)⊼a),(a⊼((b⊼b)⊼a))==(b⊼((a⊼a)⊼b)),((a⊼a)⊼a)==((b⊼b)⊼b),((a⊼a)⊼a)==((b⊼b)⊼b),((a⊼a)⊼a)==((b⊼b)⊼b)}

({{Page 818 · Nand theorems,  (page 1175)}})

{(p⊼p)⊼p,(((p⊼p)⊼p)⊼p)⊼p,(((p⊼p)⊼p)⊼q)⊼q}

{p,p⊼p,p⊼q,(p⊼p)⊼p,(p⊼q)⊼p,(p⊼p)⊼q}

Intelligence in the Universe

({{Page 832 · Doubling rules,  (page 1185)}})

{{0,2,_}->5,{5,3,_}->5,{5,_,_}->1,{_,5,_}->1,{_,2,_}->3,{_,3,2}->2,{_,1,2}->4,{_,4,_}->3,{4,3,_}->4,{4,0,_}->2,{_,x_,_}->x}

Append[Table[1,{n-1}],2]

CAEvolveList[rule_,init_List,t_Integer]:=NestList[CAStep[rule,#]&,init,t]
CAStep[GeneralCARule[rule_,r_Integer:1],a_List]:=Partition[a,2 r+1,1,r+1]/.rule

With[{n=3},CAEvolveList[GeneralCARule[{{0,2,_}->5,{5,3,_}->5,{5,_,_}->1,{_,5,_}->1,{_,2,_}->3,{_,3,2}->2,{_,1,2}->4,{_,4,_}->3,{4,3,_}->4,{4,0,_}->2,{_,x_,_}->x}],Flatten[{0,Append[Table[1,{n-1}],2],Table[0,{n+1}]}],2(n^2)+n]]//Grid

{{_,2,_}->3,{_,1,2}->2,{3,0,_}->1,{3,_,_}->3,{_,3,_}->1,{_,x_,_}->x}

CAEvolveList[rule_,init_List,t_Integer]:=NestList[CAStep[rule,#]&,init,t]
CAStep[GeneralCARule[rule_,r_Integer:1],a_List]:=Partition[a,2 r+1,1,r+1]/.rule

With[{n=3},CAEvolveList[GeneralCARule[{{_,2,_}->3,{_,1,2}->2,{3,0,_}->1,{3,_,_}->3,{_,3,_}->1,{_,x_,_}->x}],Flatten[{0,Append[Table[1,{n-1}],2],Table[0,{n+1}]}],3n]]//Grid