[FOM] 629: Boolean Algebra/Simplicity

Matthew Szudzik mszudzik at szudzik.com
Sat Oct 3 22:41:26 EDT 2015

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


has more details.

Matthew Szudzik

More information about the FOM mailing list