In[]:=
With[{tab=BooleanTable[#,{p,q,r}]},Grid[Map[TraditionalForm,ParallelMap[Function[ops,{First/@ops,First[SortBy[Catch[Do[If[#=!={},Throw[#],#]&[Select[Catenate[Groupings[#,ops]&/@Tuples[{p,q,r},n]],BooleanTable[#,{p,q,r}]==tab&]],{n,7}]],LeafCount]]}],{{And->2,Or->2,Not->1},{And->2,Not->1},{Or->2,Not->1},{Implies->2,Not->1},{Xor->2,Implies->2},{Nand->2,Not->1},{Nand->2},{Nor->2}}],{2}],Frame->All]]&/@{p||q,Nand[p,q],p||(q&&r),Xor[p,q]}
Out[]=
,
,
,
{And,Or,Not} | p∨q |
{And,Not} | ¬(¬p∧¬(q∧q)) |
{Or,Not} | p∨q |
{Implies,Not} | ¬pq |
{Xor,Implies} | (pq)q |
{Nand,Not} | ¬p⊼¬q |
{Nand} | (p⊼p)⊼(q⊼q) |
{Nor} | (p⊽q)⊽(p⊽q) |
{And,Or,Not} | ¬(p∧q) |
{And,Not} | ¬(p∧q) |
{Or,Not} | ¬p∨¬q |
{Implies,Not} | p¬q |
{Xor,Implies} | pp⊻q |
{Nand,Not} | p⊼q |
{Nand} | p⊼q |
{Nor} | (p⊽(p⊽p))⊽((p⊽p)⊽(q⊽q)) |
{And,Or,Not} | p∨(q∧r) |
{And,Not} | ¬(¬p∧¬(q∧r)) |
{Or,Not} | p∨¬(¬q∨¬r) |
{Implies,Not} | (q¬r)p |
{Xor,Implies} | (q(rp))p |
{Nand,Not} | (q⊼r)⊼¬p |
{Nand} | (p⊼p)⊼(q⊼r) |
{Nor} | (p⊽q)⊽(p⊽r) |
{And,Or,Not} | ¬(p∧q)∧(p∨q) |
{And,Not} | ¬(p∧q)∧¬(¬p∧¬q) |
{Or,Not} | ¬(p∨¬q)∨¬(q∨¬p) |
{Implies,Not} | (pq)¬(qp) |
{Xor,Implies} | p⊻q |
{Nand,Not} | (p⊼¬q)⊼(q⊼¬p) |
{Nand} | (p⊼(p⊼q))⊼(q⊼(p⊼p)) |
{Nor} | (p⊽q)⊽((p⊽p)⊽(q⊽q)) |
Implies[Implies[p,q],r]
In[]:=
FindLogicFormula[expr_,vars_,ops_,steps_:7]:=With[{tab=BooleanTable[expr,vars]},First[SortBy[Catch[Do[If[#=!={},Throw[#],#]&[Select[Catenate[Groupings[#,ops]&/@Tuples[vars,n]],BooleanTable[#,vars]==tab&]],{n,steps}]],LeafCount]]]
Take an expression using something non-functionally-complete ... e.g. Implies on its own, or And on its own....
Take an expression using something non-functionally-complete ... e.g. Implies on its own, or And on its own....
Two paths: 1. Convert to Nands and compute with that; 2. Use only Implies
Two paths: 1. Convert to Nands and compute with that; 2. Use only Implies
Simplify expression using Nands; not obvious you can go backwards to Implies
Simplify expression using Nands; not obvious you can go backwards to Implies
(x_⊼(x_⊼y_)):>imp[x,y]
In[]:=
FindLogicFormula[Implies[Implies[p,q],Implies[p,r]],{p,q,r},{Nand->2}]
Out[]=
p⊼(p⊼(q⊼(p⊼r)))
In[]:=
%//.(x_⊼(x_⊼y_)):>Implies[x,y]
Out[]=
pq⊼(p⊼r)
In[]:=
Groupings[{p,q,r},Implies->2]
Out[]=
{(pq)r,p(qr)}
In[]:=
FindLogicFormula[#,{p,q,r},{Nand->2}]&/@%64
Out[]=
{(p⊼(p⊼q))⊼(r⊼r),p⊼(p⊼(q⊼(p⊼r)))}
In[]:=
%//.(x_⊼(x_⊼y_)):>Implies[x,y]
Out[]=
{(pq)⊼(r⊼r),pq⊼(p⊼r)}
In[]:=
FindLogicFormula[#,{p,q,r},{Implies->2}]&/@%64
Out[]=
{(pq)r,p(qr)}
In[]:=
Groupings[{p,q,r,p,q},Implies->2]
Out[]=
{(((pq)r)p)q,p(((qr)p)q),(p((qr)p))q,p(q((rp)q)),((p(qr))p)q,p((q(rp))q),(p(q(rp)))q,p(q(r(pq))),((pq)(rp))q,p((qr)(pq)),((pq)r)(pq),(pq)((rp)q),(p(qr))(pq),(pq)(r(pq))}
In[]:=
FindLogicFormula[#,{p,q,r},{Implies->2}]&/@%
Out[]=
{(rp)q,pq,q,True,pq,pq,q,True,(rp)q,pq,pq,(pq)((qr)r),pq,True}
Purely in terms of Implies (((pq)r)p)q simplifies to (rp)q
In[]:=
ParallelMap[FindLogicFormula[#,{p,q,r},{Nand->2}]&,%69]
(kernel 13)
SortBy::normal:Nonatomic expression expected at position 1 in SortBy[Null,LeafCount].
Out[]=
{(q⊼q)⊼(r⊼(p⊼p)),p⊼(p⊼q),q,p⊼(p⊼p),p⊼(p⊼q),p⊼(p⊼q),q,p⊼(p⊼p),(q⊼q)⊼(r⊼(p⊼p)),p⊼(p⊼q),p⊼(p⊼q),Null,p⊼(p⊼q),p⊼(p⊼p)}
In[]:=
%//.(x_⊼(x_⊼y_)):>Implies[x,y]
Out[]=
{(q⊼q)⊼(r⊼(p⊼p)),pq,q,True,pq,pq,q,True,(q⊼q)⊼(r⊼(p⊼p)),pq,pq,Null,pq,True}
Imagine we define a higher-level math concept in terms of something lower level...
If we compute at the lower level, can we describe what happened purely in terms of the higher level?
Imagine we define a higher-level math concept in terms of something lower level...
If we compute at the lower level, can we describe what happened purely in terms of the higher level?
If we compute at the lower level, can we describe what happened purely in terms of the higher level?
Case 1:
Case 1:
p(((qr)p)q)
can be simplified to
pq
either directly, or by converting it to Nand
In[]:=
p(((qr)p)q)//.Implies[x_,y_]:>(x⊼(x⊼y))
Out[]=
p⊼(p⊼(((q⊼(q⊼r))⊼((q⊼(q⊼r))⊼p))⊼(((q⊼(q⊼r))⊼((q⊼(q⊼r))⊼p))⊼q)))
Now simplify it in Nands
In[]:=
FindLogicFormula[p⊼(p⊼(((q⊼(q⊼r))⊼((q⊼(q⊼r))⊼p))⊼(((q⊼(q⊼r))⊼((q⊼(q⊼r))⊼p))⊼q))),{p,q,r},{Nand->2}]
Out[]=
p⊼(p⊼q)
which can be converted to
In[]:=
p⊼(p⊼q)//.(x_⊼(x_⊼y_)):>Implies[x,y]
Out[]=
pq
Case 2:
Case 2:
(((pq)r)p)q
can be simplified to
(rp)q
but converting to Nand:
In[]:=
(((pq)r)p)q//.Implies[x_,y_]:>(x⊼(x⊼y))
Out[]=
(((p⊼(p⊼q))⊼((p⊼(p⊼q))⊼r))⊼(((p⊼(p⊼q))⊼((p⊼(p⊼q))⊼r))⊼p))⊼((((p⊼(p⊼q))⊼((p⊼(p⊼q))⊼r))⊼(((p⊼(p⊼q))⊼((p⊼(p⊼q))⊼r))⊼p))⊼q)
In[]:=
FindLogicFormula[%,{p,q,r},{Nand->2}]
Out[]=
(q⊼q)⊼(r⊼(p⊼p))
In[]:=
%//.(x_⊼(x_⊼y_)):>Implies[x,y]
Out[]=
(q⊼q)⊼(r⊼(p⊼p))
In[]:=
FindLogicFormula[(q⊼q)⊼(r⊼(p⊼p)),{p,q,r},{Implies->2}]
Out[]=
(rp)q
Does the definition you have capture all relevant mathematical structures/processes?
Does the definition you have capture all relevant mathematical structures/processes?
Use a definition to “compile down” to something lower level. The compiled structure could be recognizable “floating around” at the lower level. Or it could be shredded there
Use a definition to “compile down” to something lower level. The compiled structure could be recognizable “floating around” at the lower level. Or it could be shredded there
If the observer is merely looking for template at the lower level, they won’t find them in this case....
Xor case
Xor case
In[]:=
FindLogicFormula[Xor[p,q],{p,q},{Nand->2}]
Out[]=
(p⊼(p⊼q))⊼(q⊼(p⊼p))
In[]:=
Clear[LogicLoop]
This is wrong, because of the associativity of And:
Will work for Implies because it is not associative....
Will work for Implies because it is not associative....