[FOM] 629: Boolean Algebra/Simplicity

[Matthew Szudzik]

On Sun, Oct 04, 2015 at 01:08:57AM -0400, Harvey Friedman wrote:
> 
> In this particular case, I am more interested in the formulation
> allowing multiple axioms, using 0,1,and,or,not,=. This Wolfram/Veroff
> example involves a single axiom with an abbreviation for nand, which I
> consider substantially less attractive for the spirit of

Wolfram also considered equational axiomatizations for Boolean algebra
with And, Or, and Not (but without 0 and 1).  Unfortunately, I don't
think that computers were fast enough in 2000 to search for the shortest
single axiom in that case.

Nevertheless, Wolfram came up with the following interesting result:

 http://wolframscience.com/nksonline/page-817

If one lists the theorems of Boolean algebra in order of syntactic
complexity (based on the height of the parse tree, number of leaves on
the tree, number of distinct variable names, etc.), and if one picks out
those theorems in the list that cannot be derived from earlier theorems,
then those theorems are exactly the standard theorems that are given
names in textbooks (with the exception of the second of the two
distributive laws, which can be derived from theorems earlier in the
list).  This provides a nice formalization for the intuitive notion of
an 'interesting theorem of Boolean algebra'.

Matthew Szudzik