[FOM] 629: Boolean Algebra/Simplicity

[Harvey Friedman]

Nice! It does show that it is possible to carry out such research, at
least in some contexts, as we hoped for in
http://www.cs.nyu.edu/pipermail/fom/2012-March/016357.html

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
http://www.cs.nyu.edu/pipermail/fom/2012-March/016357.html Of course,
I can imagine a rationale, say involving circuits and other
considerations, where one may get interested in the Wolfram/Veroff
formulation.

I also see from http://www.cs.unm.edu/~veroff/BA that there is
subsequent work on short axiomatizations of BA, still with a primary
focus on single axioms.

Of course, a small set of small axioms is much more readable.

INFORMAL QUESTION. What is the most readable axiomatization of BA in
0,1,and,or,not?

Here one can put a very stringent condition, say just size, on each
axiom, and a stringent condition on the number of axioms.

Harvey Friedman

On Sat, Oct 3, 2015 at 10:41 PM, Matthew Szudzik <mszudzik at szudzik.com> wrote:
> 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
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom