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

(x | x) | (x | x) = x
x | (y | (y | y)) = x | x
(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.

(x | x) | (y | x) = x
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.

Several 2-bases are presented in [4].
Several more 2-bases are presented in [5], including, for example,
1. (x | y) | (x | (y | z)) = x
2. x | y = y | x,
which is system 26 (Equations 26a and 26b) from the candidate set. This basis is especially simple in that it has a total of only 6 applications of the Sheffer stroke operator. In terms of length, the basis has a total length of 18 (i.e., has a combined total of 18 variable and operator symbols). Furthermore, the basis is shortest in that no 2-basis has fewer than 6 applications of the Sheffer stroke operator and unique up to applications of commutativity. That is, this basis and its commutative variants are the only shortest 2-bases for Boolean algebra in terms of the Sheffer stroke.
A single axiom of length 105 is presented in [6].
The length 15 equation, ((x|z)|y)|((x|(x|y))|x)=y, is proved to be a single axiom in [7]. This equation is the "mirror image" of Equation 10 from the candidate set, where the mirror image is found by applying commutativity to each occurrence of the Sheffer stroke operator.
Since the mirror image of any single axiom is a single axiom, it follows that Equation 10 itself, (x|((y|x)|x))|(y|(z|x))=y, also is a single axiom.
Equation 10 is called Sh-1 in [8]. Here is the Otter proof from the paper.
(Sh-1.in, Sh-1.proof)

Here is a Prover9 proof.
(in, out, pf, xml)

The Prover9 proof consists of strictly-forward, demodulation-free derivations of the 3 axioms of the known system proved in the paper.
Equation ((x|y)|z)|(x|((x|z)|x))=z (Equation 14 from the candidate set) is proved to be a single axiom in [8]. It follows that the mirror image, ((x|(z|x))|x)|(z|(y|x))=z, also is a single axiom.
The mirror image of Equation 14 is called Sh-2 in [8]. Here is the Otter proof from the paper.
(Sh-2.in, Sh-2.proof)

Here is a Prover9 proof.
(in, out, pf, xml)

The Prover9 proof consists of strictly-forward, demodulation-free derivations of the 3 axioms of the known system proved in the paper.
[8] includes proofs that these single axioms are among the shortest possible. It also includes several short single axioms for Boolean algebra in terms of the operators or and not.
[9] is mostly a rehashing of the material in [5], but it includes proofs that the short Sheffer 2-basis mentioned previously is indeed shortest and that it is unique up to applications of commutativity.
Here are lists of clauses that help reconcile the naming conventions used in the original candidate list and the JAR paper ([8]).

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