[FOM] 629: Boolean Algebra/Simplicity
Harvey Friedman
hmflogic at gmail.com
Sun Oct 4 01:08:57 EDT 2015
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
More information about the FOM
mailing list