Short Single Axioms for Boolean Algebra

William McCune, Robert Veroff, Branden Fitelson, Kenneth Harris, Andrew Feist, Larry Wos

June 2000 (Revised December 2002)

This web page contains material in support of a paper of the same name in the Journal of Automated Reasoning 29 (1), pages 1--16, 2002. Here is a preprint of the paper.

Here are the links that correspond to the "pseudo-links" in the paper.

1. Background and Introduction

2. A Basis for Disjunction and Negation

3. A Basis for the Sheffer Stroke

4. (Sh_1) is a Shortest 1-Basis for the Sheffer Stroke

5. An Exhaustive List of Possible 15-Symbol Single Axioms

open-16 (the 16 open candidates of length 15)
- Update (August 2003): Thomas Hillenbrand has written (by e-mail) that C_2 and C_5 are, in fact, single axioms. Waldmeister proved the theorems, given specialized definitions, and (for C_5) multiple searches, restarting with lemmas.
- Update (November 2003): A counterexample to C_9 has been found.
  - Mace4 input (needs version mace4-2003-C)
  - Mace4 output

6. Automated Deduction Methods

DN-filter.interps
DN-search.in, DN-search.proof
DN-20615.in, DN-20615.proof (same as above)
Sh-1-comm.in, Sh-1-comm.proof
DN-1.in, DN-1.proof (same as above)
Sh-1.in, Sh-1.proof (same as above)
Sh-2.in, Sh-2.proof (same as above)
circle-1.in, circle-1.proof
circle-2.in, circle-2.proof
circle-3.in, circle-3.proof
circle-4.in, circle-4.proof

7. Summary and Questions

Additional Material

In a footnote on the third page of the paper we write:

Wolfram's 25 candidates are precisely the set of Sheffer identities of length <= 15 (excluding mirror images) that have no noncommutative models of size <=4.

Here is how one can use MACE 2.0 to derive the 25 candidates.

Consider Sheffer-mgi-without-mirrors (356 members). This is the set of Sheffer stroke identities of length <= 15, excluding mirror images, and is straightforward to generate.
The simple Perl program commute4_filter takes a stream of Sheffer identities and filters out those with noncommutative models of size up through 4. For each identity, the Perl program calls MACE 2.0 (here's a Linux binary of MACE 2) to determine if any noncommutative models of size <=4 exist.
Running the command
```
        commute4_filter < Sheffer-mgi-without-mirrors
```
gives us the 25 candidates in a minute or so.