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.

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

- (x | x) | (x | x) = x
- x | (y | (y | y)) = x | x
- (x | (y | z)) | (x | (y | z)) = ((y | y) | x) | ((z | z) | x)

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

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

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.

[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)