With the right definitions, one is effectively reducing computational work
With the right definitions, one is effectively reducing computational work
The definitions could be “violated” by the existence of axioms that “break out of the definitions”
If you resolve all definitions, you have “axiomatic machine code”
If you resolve all definitions, you have “axiomatic machine code”
~ Grothendieck’s avocado
~ Grothendieck’s avocado
E.g. in logic ... compile from And, Or to Nand .... then at the end try to go back.....
E.g. in logic ... compile from And, Or to Nand .... then at the end try to go back.....
Consider expressions in terms of Implies alone.... [Implicational calculus.. ]
There are theorems of implicational calculus ...
There are theorems of implicational calculus ...
In[]:=
With[{tab=BooleanTable[Implies[p,q],{p,q}]},First[SortBy[Catch[Do[If[#=!={},Throw[#],#]&[Select[Catenate[Groupings[#,{Nand->2}]&/@Tuples[{p,q},n]],BooleanTable[#,{p,q}]==tab&]],{n,7}]],LeafCount]]]
Out[]=
p⊼(p⊼q)
In[]:=
Implies[Implies[p,q],Implies[p,r]]//.Implies[p_,q_]:>p⊼(p⊼q)
Out[]=
(p⊼(p⊼q))⊼((p⊼(p⊼q))⊼(p⊼(p⊼r)))
In[]:=
BooleanTable[(p⊼(p⊼q))⊼((p⊼(p⊼q))⊼(p⊼(p⊼r))),{p,q,r}]
Out[]=
{True,False,True,True,True,True,True,True}
In[]:=
BooleanTable[Implies[Implies[p,q],Implies[p,r]],{p,q,r}]
Out[]=
{True,False,True,True,True,True,True,True}
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]]]
In[]:=
FindLogicFormula[Implies[p,q],{p,q},{Nand->2}]
Out[]=
p⊼(p⊼q)
In[]:=
FindLogicFormula[Implies[Implies[p,q],Implies[p,r]],{p,q,r},{Nand->2}]
Out[]=
p⊼(p⊼(q⊼(p⊼r)))
In[]:=
ExpressionTree[p⊼(p⊼q)]
Out[]=
In[]:=
ExpressionTree[p⊼(p⊼(q⊼(p⊼r)))]
Out[]=
In[]:=
(x_⊼(x_⊼y_)):>imp[x,y]
Out[]=
x_⊼(x_⊼y_)imp[x,y]
In[]:=
p⊼(p⊼(q⊼(p⊼r)))//.(x_⊼(x_⊼y_)):>imp[x,y]
Out[]=
imp[p,q⊼(p⊼r)]
By distinguishing definitions and evolution by wff vs. ⊢ one can avoid this, by cocooning the defined objects.... [like different combinators]
By distinguishing definitions and evolution by wff vs. ⊢ one can avoid this, by cocooning the defined objects.... [like different combinators]
When is coarse-graining consistent?
When is coarse-graining consistent?
If the “reference frame leaks” it doesn’t matter if all you’re looking at is large-scale fluid mechanics...
If the “reference frame leaks” it doesn’t matter if all you’re looking at is large-scale fluid mechanics...
There may be leaks in corner cases, but it doesn’t matter to ordinary math
“Most of the code works ... except in a corner case” [Is the hole big enough to fit a counterexample through?] [ Is the space tunnel big enough to fit a photon through? ]
If you insist on writing verifiable code, what can you program?
Analogy : conservation laws
Analogy : conservation laws
To have a perfect definition, you need a conservation law .... otherwise things will turn into heat....