Boolean Algebra Results
Boolean Algebra Results
In[]:=
data53
Out[]=
In[]:=
Flatten[Groupings[#,{Wedge->2,Vee->2,Square->1}]&/@Catenate[Table[Tuples[{a,b},n],{n,3}]]]
Out[]=
In[]:=
AllTheorems[{a,b},3]
Out[]=
In[]:=
ResourceFunction["DepthLeafCountSort"][%]
Out[]=
In[]:=
%===%%
Out[]=
False
In[]:=
FindPermutation[%158,%157]
Out[]=
Cycles[{{6,22,17,12,7,23,18,13,8,24,19,14,9,41,37,33,59,53,61,55,50,46,64,57,51,47,43,60,54,49,45,40,36,63,62,56,65,58,52,48,44,39,35,32,30,28,26,21,16,11},{10,42,38,34,31,29,27,25,20,15},{69,82,91,96,110,97,100,102,114,127,73,85,93,108,116,128,99,112,118,122,124,77,74,72,84,92,107,106,79,89},{70,83,78,88,94,98,111,117,129,119,123,131,134,121,103,104,105,115,120,130,133,139,141,138,137,101,113,126,132,135,136,140,75,86,80,76,87,81,90,95,109,71}}]
In[]:=
PermutationList[%]
Out[]=
{1,2,3,4,5,22,23,24,41,42,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,25,26,27,28,29,30,59,31,32,63,33,34,35,36,37,38,60,39,40,64,43,44,45,46,47,48,61,49,50,65,51,52,53,54,55,56,62,57,58,66,67,68,82,83,70,84,85,72,86,87,74,88,89,76,90,91,78,92,93,80,81,94,69,95,96,107,108,98,109,110,100,111,112,102,113,114,104,105,115,79,106,116,71,97,117,118,126,127,120,128,129,122,123,130,103,124,131,77,125,132,73,99,119,133,134,135,139,121,136,140,101,137,141,75,138}
In[]:=
ListLinePlot[%]
Out[]=
Grid[Flatten/@Table[{Length@FindAllAON[p,n],Style[Length@FindAONTheorems[p,n],Background->LightBlue]},{p,5},{n,4}],Frame->All,FrameStyle->LightGray,AlignmentRight]
In[]:=
FindAllAON[3,2]
Out[]=
{ab,aa,ba,ab,bb,ab,aa⋀a,ba⋀a,aa⋀a,ba⋀a,aa⋁a,ba⋁a,aa⋁a,ba⋁a,a⋀aa⋁a,aa⋀b,ba⋀b,aa⋀b,ba⋀b,a⋀aa⋀b,a⋁aa⋀b,aa⋁b,ba⋁b,aa⋁b,ba⋁b,a⋀aa⋁b,a⋁aa⋁b,a⋀ba⋁b,ab⋀a,bb⋀a,ab⋀a,bb⋀a,a⋀ab⋀a,a⋁ab⋀a,a⋀bb⋀a,a⋁bb⋀a,ab⋁a,bb⋁a,ab⋁a,bb⋁a,a⋀ab⋁a,a⋁ab⋁a,a⋀bb⋁a,a⋁bb⋁a,b⋀ab⋁a,ab⋀b,bb⋀b,ab⋀b,bb⋀b,a⋀ab⋀b,a⋁ab⋀b,a⋀bb⋀b,a⋁bb⋀b,b⋀ab⋀b,b⋁ab⋀b,ab⋁b,bb⋁b,ab⋁b,bb⋁b,a⋀ab⋁b,a⋁ab⋁b,a⋀bb⋁b,a⋁bb⋁b,b⋀ab⋁b,b⋁ab⋁b,b⋀bb⋁b,aa,ba,aa,ba,a⋀aa,a⋁aa,a⋀ba,a⋁ba,b⋀aa,b⋁aa,b⋀ba,b⋁ba,ab,bb,ab,bb,a⋀ab,a⋁ab,a⋀bb,a⋁bb,b⋀ab,b⋁ab,b⋀bb,b⋁bb,ab}
In[]:=
LeafCount/@%
Out[]=
{3,4,4,4,4,5,5,5,6,6,5,5,6,6,7,5,5,6,6,7,7,5,5,6,6,7,7,7,5,5,6,6,7,7,7,7,5,5,6,6,7,7,7,7,7,5,5,6,6,7,7,7,7,7,7,5,5,6,6,7,7,7,7,7,7,7,5,5,6,6,7,7,7,7,7,7,7,7,5,5,6,6,7,7,7,7,7,7,7,7,7}
In[]:=
Grid[Prepend[MapIndexed[Prepend[#,First[#2]]&,Flatten/@Table[{Length@FindAllAON[p,n],Style[Length@FindAONTheorems[p,n],Background->LightBlue]},{p,5},{n,4}]],Prepend[Catenate[Table[{Row[{"≤",n}],},{n,4}]],""]],Frame->All,Dividers->{Table[n->Black,{n,2,10,2}]},FrameStyle->LightGray,AlignmentRight]
Out[]=
≤1 | ≤2 | ≤3 | ≤4 | |||||
1 | 0 | 1 | 1 | 2 | 3 | 3 | 6 | 4 |
2 | 1 | 2 | 6 | 4 | 15 | 6 | 28 | 8 |
3 | 10 | 2 | 91 | 6 | 351 | 12 | 946 | 20 |
4 | 66 | 4 | 780 | 14 | 3486 | 32 | 10296 | 58 |
5 | 528 | 4 | 11781 | 14 | 84255 | 40 | 362526 | 90 |
In[]:=
Prepend[Table[Row[{"≤",n,}],{n,4}],""]
Out[]=
{,≤1,≤2,≤3,≤4}
In[]:=
TautologyQ[Equivalent[And[a,b],And[b,a]]]
Out[]=
True
In[]:=
And[a,b]==And[b,a]
Out[]=
(a&&b)(b&&a)
In[]:=
Counts[TautologyQ/@(data53/.{Equal->Equivalent,Square->Not,Vee->Or,Wedge->And})]
Out[]=
True914
In[]:=
Take[data53,10]
Out[]=
{aa⋀a,aa⋁a,a⋀aa⋁a,a⋀bb⋀a,a⋁bb⋁a,aa,a⋀aa,a⋁aa,a⋀aa⋀a,a⋁aa⋁a}
In[]:=
FindAllAON[3,2]
Out[]=
{ab,aa,ba,ab,bb,ab,aa⋀a,ba⋀a,aa⋀a,ba⋀a,aa⋁a,ba⋁a,aa⋁a,ba⋁a,a⋀aa⋁a,aa⋀b,ba⋀b,aa⋀b,ba⋀b,a⋀aa⋀b,a⋁aa⋀b,aa⋁b,ba⋁b,aa⋁b,ba⋁b,a⋀aa⋁b,a⋁aa⋁b,a⋀ba⋁b,ab⋀a,bb⋀a,ab⋀a,bb⋀a,a⋀ab⋀a,a⋁ab⋀a,a⋀bb⋀a,a⋁bb⋀a,ab⋁a,bb⋁a,ab⋁a,bb⋁a,a⋀ab⋁a,a⋁ab⋁a,a⋀bb⋁a,a⋁bb⋁a,b⋀ab⋁a,ab⋀b,bb⋀b,ab⋀b,bb⋀b,a⋀ab⋀b,a⋁ab⋀b,a⋀bb⋀b,a⋁bb⋀b,b⋀ab⋀b,b⋁ab⋀b,ab⋁b,bb⋁b,ab⋁b,bb⋁b,a⋀ab⋁b,a⋁ab⋁b,a⋀bb⋁b,a⋁bb⋁b,b⋀ab⋁b,b⋁ab⋁b,b⋀bb⋁b,aa,ba,aa,ba,a⋀aa,a⋁aa,a⋀ba,a⋁ba,b⋀aa,b⋁aa,b⋀ba,b⋁ba,ab,bb,ab,bb,a⋀ab,a⋁ab,a⋀bb,a⋁bb,b⋀ab,b⋁ab,b⋀bb,b⋁bb,ab}
In[]:=
Counts[TautologyQ/@(%/.{Equal->Equivalent,Square->Not,Vee->Or,Wedge->And})]
Out[]=
False77,True14
In[]:=
Table[Counts[TautologyQ/@(FindAllAON[p,n]/.{Equal->Equivalent,Square->Not,Vee->Or,Wedge->And})],{p,4},{n,4}]
Out[]=
{{,False1,False3,False6},{False1,False6,False15,False28},{False4,True6,False77,True14,False327,True24,False910,True36},{False52,True14,False736,True44,False3396,True90,False10144,True152}}
In[]:=
Map[{Total[#],Lookup[#,True,0]}&,%197,{2}]
Out[]=
{{{0,0},{1,0},{3,0},{6,0}},{{1,0},{6,0},{15,0},{28,0}},{{10,6},{91,14},{351,24},{946,36}},{{66,14},{780,44},{3486,90},{10296,152}}}
Metamath Database
Metamath Database
In[]:=
metamathGraph=CloudGet["https://wolfr.am/PLbmdhRv"];
In[]:=
metamathAssoc=CloudGet["https://wolfr.am/PLborw8R"];
In[]:=
metamathDomains=Union[Values[metamathAssoc]];
In[]:=
metamathInfrastructure={"SUPPLEMENTARY MATERIAL (USER'S MATHBOXES)","GUIDES AND MISCELLANEA"};
In[]:=
VertexCount[metamathGraph]
Out[]=
35241
metamathGraph is the dependency graph of theorems .... where its nodes are “generalized substitution” taking in some set of theorems, and generating a new one
[each node is a proof of one named theorem from others]
[the “raw material” may include “definitions”, which have the same form as axioms]
[each node is a proof of one named theorem from others]
[the “raw material” may include “definitions”, which have the same form as axioms]
Base of everything is named operator-like constructs
Dependency graph is coarse-grained to the level of just talking about named theorems, eliding away unnamed lemmas
MM database defines 35241 things that were named....
Of which XXX are definitions, XXX are axioms .... and XXX are derived theorems
Definitions define syntax forms but don’t have truth value
Definitions: http://us.metamath.org/mpeuni/mmdefinitions.html
Definitions: http://us.metamath.org/mpeuni/mmdefinitions.html
For a definition, only going one way
What’s worth defining?
What’s worth defining?
Perfect numbers? DivisorSigma ?? [power vs. iterated multiplication] << Directly analogous to language design >>
In language design, resolving definitions can be nontrivial computation;
here definitions are essentially trivial macros
here definitions are essentially trivial macros
Deducing equivalences vs. running the evaluator
Definitions
Definitions
Of all possible low-level sequences of symbols, which ones are given names via definitions?
emeplasm
Level 1: what definitions are worth making
Level 2: what theorems are worth talking about [given definitions]
Level 2: what theorems are worth talking about [given definitions]
[[ There is a configuration of pixels on the screen; ultimately we are the ones who might consider it meaningful ]]
Graph of Definitions in MM
Graph of Definitions in MM
The things without links are “pure emes”
On http://us.metamath.org/mpeuni/mmdefinitions.html df-* is a definition; other things are pure notation
The pure notation would be implemented at a lower level as emes
The pure notation would be implemented at a lower level as emes
Find all entries that are df-* named
Then look at what these depend on
Pure “atomic” stuff
Then look at what these depend on
Pure “atomic” stuff
In Boolean algebra, an analogy would be defining xnor and writing theorems in terms of it
In Boolean algebra, an analogy would be defining xnor and writing theorems in terms of it
In the case of logic, we have certain constructs that we usually talk about....
In the case of logic, we have certain constructs that we usually talk about....
Make the mapping
Make the mapping
ASCII conventions: http://us.metamath.org/mpegif/mmascii.html
ASCII conventions: http://us.metamath.org/mpegif/mmascii.html
NOTE: definitions are more subtle in the way they are set up
NOTE: definitions are more subtle in the way they are set up