[FOM] 629: Boolean Algebra/Simplicity

[Matthew Szudzik]

On Sat, Oct 03, 2015 at 09:41:32AM -0400, Harvey Friedman wrote:
> 
> Here with BA, I am thinking that with the imaginative help from
> computer technology, it may be possible to determine good lower and
> upper bounds on the "simplest" axiomatization of BA.
> 
> Take the following specific formulation. Use the particularly natural
> language 0,1,and,or,not. All axioms must be equations.
> 
> We count the total number # of signs used, excluding parentheses and =.
> 

This is almost exactly what Stephen Wolfram did in 2000.  (I was one of
his research assistants at the time, but I wasn't involved in this
particular project.)  By doing an exhaustive search, Wolfram was able to
eliminate all candidate axioms that are smaller than the single axiom
for Boolean algebra that now appears on Wikipedia.  But Wolfram was not
able to prove that the single axiom was, in fact, an axiom for Boolean
algebra.  Instead, that was done by Bob Veroff.  Veroff's webpage

 http://www.cs.unm.edu/~veroff/BA

has more details.

Matthew Szudzik