Posted on the Web July 8, 2000. Last updated on August 27, 2021 by Bob Veroff.

Update (2016-feb-16): We posted Prover9 proofs that candidates C2 and C5 are single axioms.

Update (2021-aug-27): We added links on this page to Otter and Prover9 proofs that Sh-1 and Sh-2 are single axioms.

Simple Axiom Systems for Boolean Algebra

This page (still under development) will summarize our work in identifying and verifying simple axiom systems for Boolean algebra. For now, the focus will be primarily on equational systems in terms of the Sheffer stroke operator, |. Bill McCune maintains related pages here and here.

Collaborators on this project include Andrew Feist, Branden Fitelson, Ken Harris, Bill McCune, Bob Veroff, and Larry Wos.

Sheffer Stroke

In 1913, Henry Sheffer presented the following 3-axiom equational basis (3-basis) for Boolean Algebra [1].
  1. (x | x) | (x | x) = x
  2. x | (y | (y | y)) = x | x
  3. (x | (y | z)) | (x | (y | z)) = ((y | y) | x) | ((z | z) | x)
Note: In Sheffer's paper, the | operator, which is now commonly called the Sheffer stroke, is interpreted as "NOR" (x | y = x' * y'). It also is common to interpret it instead as the dual "NAND" (x | y = x' + y').

More recently, a number of simplifications ("abridgements") of Sheffer's system have been published. These include, for example, five systems presented by Meredith [2]. The simplest of these five systems is as follows.

  1. (x | x) | (y | x) = x
  2. x | (y | (x | z)) = ((z | y) | y) | x

We were introduced to this problem in February 2000 via some e-mail exchanges with Dana Scott, Stephen Wolfram, and David Hillman. In particular, Stephen Wolfram proposed a study of 27 candidate axiom systems consisting of 25 single equations and 2 pairs of equations. Wolfram's interest in these equations arose from his research project, A New Kind of Science.

We have used the automated reasoning program Otter [3] to prove several bases. The following is a very brief summary.

Other Operators

A number of single axioms in terms of operators other than the Sheffer stroke are presented in [6]. These are in addition to the length 105 Sheffer equation already mentioned.

Bill McCune is developing a Web page, Short Single Axioms for Boolean Algebra with {OR, NOT}.

Comments

It is known that no Sheffer equation of length less than 15 can be a single axiom, so some of the single axioms identified above are indeed among the shortest possible. We'll eventually include some discussion on this topic.

Some work not yet reported here is the use of model generation techniques to eliminate candidate axiom systems from consideration. Some of this work has relied on the use of the program SEM.

We'll eventually include a sampling of input files and proofs.

References

[1] Sheffer, H., "A set of five independent postulates for Boolean algebras, with application to logical constants," Trans. American Mathematical Society, vol. 14 (1913), pp. 481-488.

[2] Meredith, C., "Equational postulates for the Sheffer stroke," Notre Dame Journal of Formal Logic, vol. 10 (1969), pp. 266-270.

[3] McCune, W., OTTER 3.0 Reference Manual and Guide, Technical Report ANL-94/6, Argonne National Laboratory, Argonne, Illinois, 1994.

[4] Veroff, R., Axiom Systems for Boolean Algebra Using the Sheffer Stroke, Technical Report TR-CS-2000-15, Computer Science Department, University of New Mexico, Albuquerque, New Mexico, 2000. (gzipped postscript)

[5] Veroff, R., Short 2-Bases for Boolean Algebra in Terms of the Sheffer Stroke, Technical Report TR-CS-2000-25, Computer Science Department, University of New Mexico, Albuquerque, New Mexico, 2000. (gzipped postscript)

[6] McCune, W., Single Axioms for Boolean Algebra, Technical Memo ANL/MCS-TM-243, Argonne National Laboratory, Argonne, Illinois, 2000. (pdf)

[7] Veroff, R. and McCune, W., A Short Sheffer Axiom for Boolean Algebra, Technical Report TR-CS-2000-26, Computer Science Department, University of New Mexico, Albuquerque, New Mexico, 2000. (gzipped postscript)

[8] McCune, W., Veroff, R., Fitelson, B., Harris, K., Feist, A., and Wos, L., "Short Single Axioms for Boolean Algebra," Journal of Automated Reasoning, vol. 29, no. 1, (2002), pp. 1-16. (pdf)

[9] Veroff, R., "A Shortest 2-Basis for Boolean Algebra in Terms of the Sheffer Stroke," Journal of Automated Reasoning, to appear. (pdf)


The University of New Mexico

School of Engineering

Computer Science Department