Both the philosopher Charles Sanders Peirce in 1880 and the American logician H. M. Sheffer in 1913 realized that the truth-functions of elementary logic could all be defined from a single operation. The Sheffer stroke, also known as the NAND operation, is a logical operator with the following meaning: p NAND q is true if and only if not both p and q are true. It is named for Henry M. Sheffer, who proved that all the usual operators of Boolean algebra (not, and, or, implies) could be expressed in terms of NAND*. There is another logical operator which is able to express all the others: NOR* [ A set of five independent postulates for Boolean algebras, with application to logical constants. Transactions of the American Mathematical Soc. 14 (1913), pp. 481-488]. In 1933, Edward Huntington proposed an alternative set of axioms for Boolean algebra, consisting of associativity and commutativity plus Huntington’s axiom:!( !x [Or] y) [Or] ( !( !x [Or] !y ) = x
Huntington showed that the three axioms together imply the axioms of Boolean algebra. Sometime after, Herbert Ellis Robbins also found a single axiom:!( !( x [Or] y) [Or] ( y [Or] !x )) = x that he conjectured (when taken  together with associativity and commutativity) implied that of Huntington, so that Robbins algebras are equivalent to Boolean algebras.The proof was finally delivered in 1996 by William McCune, using his theorem prover EQP.*,*** Gina Kolata, Computer Math Proof Shows Reasoning Power, The New York Times, 1996. ** Tutorial on Automatic Reasoning and Theorem Proving related to the course MAT 504, Topics in Logic, for the Spring term of 1997 from prof. Edward Nelson A single axiom that is satisfied only by NAND or NOR must be in equational form since otherwise constant functions would satisfy the equation. As Stephen Wolfram has proved, with up to six NANDs and two variables, none of the 16896 possible axiom systems of this kind work even up to 3-value operators. But with 6 NANDS and 3 variables, 296 of the 288684 possible axiom systems work up to 3-value operators, and 100 work up to 4-value operators (Wolfram 2002, p. 809). Of the 25 of these that are not trivially equivalent, it then turns out that only the Wolfram axiom:(((x [Nand] y) [Nand] z) [Nand] (x [Nand] ((x [Nand] z) [Nand] x))) = z. is equivalent to the axioms of Boolean algebra (Wolfram 2002, pp. 808-811 and 1174). Wolfram, who also proved that there were no smaller candidates, found the simplest equational axiom system for Boolean algebra by using the methods contained in his A New Kind of Science. He has also pointed out that around 1949 Carew Meredith found the axiom system:f[f[a, f[b, c]], f[a, f[b, c]]] = f[f[f[c, a], a],f[f[b, a], a]]f[f[a, a], f[b, a]] ==a. In 1967 George Spencer Brown found (NKS page 1173)f[f[a, a], f[f[b, b], b]] ==af[a, f[b, c]] = f[f[f[f[c, c], a], f[f[b, b], a]], f[f[f[c, c], a], f[f[b, b], a]]] and in 1969 Meredith also found the systemf[a, f[b, f[a, c]]] = f[a, f[b, f[b, c]]]f[f[a, a], f[b, a]] = af[a, b] == f[b, a]
Carew Meredith spent a long time studying somewhat similar forms (e.g. http://www.wolframscience.com/nksonline/page-1175a-text). Meredith’s interest in short axioms came originally from Lukasiewicz.

More online references:
- NKS explanation on the use of axioms.
- Simple Axiom Systems for Boolean Algebra.
- A Summary of New Results in Mathematics Obtained with Argonne’s Automated Deduction Software.- Group Theory Single Axioms Survey.
- Axiomatizations of Some Sentential Logics.

More bibliographical references (Meredith and Prior 1968 and Meredith 1969b are the main ones on equational logic, and Meredith 1951 contains the six-character single axiom that Prior described as ’sensational’):

- Meredith, C.A. 1951. ‘On an Extended System of the Propositional Calculus’. Proceedings of the Royal Irish Academy, vol. 54 Sect. A, 37-47.
- Meredith, C.A. 1953a. ‘Single Axioms for the Systems (C,N), (C, 0), and (A, N) of the Two-Valued Propositional Calculus’. Journal of Computing Systems, vol. 1, 155-164.
- Meredith, C.A. 1953b. ‘A Single Axiom of Positive Logic’. Journal of Computing Systems, vol. 1, 169-170.
- Meredith, C.A. 1958. ‘The Dependence of an Axiom of Lukasiewicz’. Transactions of the American Mathematical Society, vol. 87, 54.
- Meredith, C.A. 1966. ‘Postulates for Implicational Calculi’. Journal of Symbolic Logic, vol. 31, 7-9.
- Meredith, C.A. 1969b. ‘Equational Postulates for the Sheffer Stroke’. Notre Dame Journal of Formal Logic, vol. 10, 266-270.
- Meredith, C.A., Prior, A.N. 1963. ‘Notes on the Axiomatics of the Propositional Calculus’. Notre Dame Journal of Formal Logic, vol. 4, 171-187.
- Meredith, C.A., Prior, A.N. 1968. ‘Equational Logic’. Notre Dame Journal of Formal Logic, vol. 9, 212-226.

Last Modified : May 15th, 2008 Filed under : Foundations of Math, Mathematical Logic Navigate : Previous post / Next post