[FOM] 629: Boolean Algebra/Simplicity

[Harvey Friedman]

There are many axiomatizations of Boolean Algebras, using various sets
of primitives.

I want to focus only on the purely equational axiomatizations.

Recall my posting on Simplicity
http://www.cs.nyu.edu/pipermail/fom/2012-March/016357.html

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 =.

I found the following relevant comments in the Wiki entry
https://en.wikipedia.org/wiki/Boolean_algebra#Basic_operations

"In 1933 Edward Huntington showed that if the basic operations are
taken to be x∨y and ¬x, with x∧y considered a derived operation (e.g.
via De Morgan's law in the form x∧y = ¬(¬x∨¬y)), then the equation
¬(¬x∨¬y)∨¬(¬x∨y) = x along with the two equations expressing
associativity and commutativity of ∨ completely axiomatized Boolean
algebra. When the only basic operation is the binary NAND operation
¬(x∧y), Stephen Wolfram has proposed in his book A New Kind of Science
the single axiom (((xy)z)(x((xz)x))) = z as a one-equation
axiomatization of Boolean algebra, where for convenience here xy
denotes the NAND rather than the AND of x and y."

Incidentally, all of the axiomatizations of BA that I have seen use
three variables. Must be a classic result that you can't get away with
2 variables? And also, are we going to gain any simplicity (low #) by
using more variables?

Of course, the same study can be done for Heyting Algebra.

So realistically, how are we going to start using a computer for this
kind of study?

I would start by proving that there is no axiomatization of BA with
complexity k, in the above mentioned complexity measure #. Start with
k = 1, and move up, and see how far you can get. I can even handle k =
1, and so start with k = 2 (smile).

**********************************************************
My website is at https://u.osu.edu/friedman.8/ and my youtube site is at
https://www.youtube.com/channel/UCdRdeExwKiWndBl4YOxBTEQ
This is the 629th in a series of self contained numbered
postings to FOM covering a wide range of topics in f.o.m. The list of
previous numbered postings #1-599 can be found at the FOM posting
http://www.cs.nyu.edu/pipermail/fom/2015-August/018887.html

600: Removing Deep Pathology 1  8/15/15  10:37PM
601: Finite Emulation Theory 1/perfect?  8/22/15  1:17AM
602: Removing Deep Pathology 2  8/23/15  6:35PM
603: Removing Deep Pathology 3  8/25/15  10:24AM
604: Finite Emulation Theory 2  8/26/15  2:54PM
605: Integer and Real Functions  8/27/15  1:50PM
606: Simple Theory of Types  8/29/15  6:30PM
607: Hindman's Theorem  8/30/15  3:58PM
608: Integer and Real Functions 2  9/1/15  6:40AM
609. Finite Continuation Theory 17  9/315  1:17PM
610: Function Continuation Theory 1  9/4/15  3:40PM
611: Function Emulation/Continuation Theory 2  9/8/15  12:58AM
612: Binary Operation Emulation and Continuation 1  9/7/15  4:35PM
613: Optimal Function Theory 1  9/13/15  11:30AM
614: Adventures in Formalization 1  9/14/15  1:43PM
615: Adventures in Formalization 2  9/14/15  1:44PM
616: Adventures in Formalization 3  9/14/15  1:45PM
617: Removing Connectives 1  9/115/15  7:47AM
618: Adventures in Formalization 4  9/15/15  3:07PM
619: Nonstandardism 1  9/17/15  9:57AM
620: Nonstandardism 2  9/18/15  2:12AM
621: Adventures in Formalization  5  9/18/15  12:54PM
622: Adventures in Formalization 6  9/29/15  3:33AM
623: Optimal Function Theory 2  9/22/15  12:02AM
624: Optimal Function Theory 3  9/22/15  11:18AM
625: Optimal Function Theory 4  9/23/15  10:16PM
626: Optimal Function Theory 5  9/2515  10:26PM
627: Optimal Function Theory 6  9/29/15  2:21AM
628: Optimal Function Theory 7  10/2/15  6:23PM

Harvey Friedman