## On single and shortest axioms for Boolean logic

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. See:

Gina Kolata, Computer Math Proof Shows Reasoning Power, The New York Times, 1996.

As a result of an exhaustive and systematic computer exploration undertaken by Stephen Wolfram looking for the shortest single axiom equivalent to the axioms of Boolean algebra. Wolfram found among 288684 a single formula (up to other equivalent of the same size) with 6 Nands and 3 variables. It then turns out that Wolfram’s axiom:

(((x [Nand] y) [Nand] z) [Nand] (x [Nand] ((x [Nand] z) [Nand] x))) = z

is equivalent to the axioms of Boolean algebra and the shortest (in the number of operators and variables) single axiom equivalent to Boolean algebra (Wolfram 2002, pp. 808-811 and 1174).

In the NKS notes at the end of the book there is an account that around 1949 Carew Meredith found the axiom system (NKS page 1173):

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

And in 1967 George Spencer Brown found:

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 again Meredith in 1969:

f[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. Meredith’s interest in short axioms came originally from Lukasiewicz.

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

If you have an interest in single axioms for systems, you might be interested in Tarsi’s 1930 result, which is that if you have a logic defined by axioms, the rule of Modus Ponens, and the rule of Uniform Substitution, then is MUST have a single axiom basis if it can prove two specific theorems he gave.

Giving names to the theorems for discussion:

I: Cpp p -> p

K: CpCqp p -> (q -> p)

C: CCpCqrCqCpr (p -> (q -> r)) -> (q -> (p -> r))

D: CpCqCCpCqrr p -> (q -> ((p -> (q -> r)) -> r))

E: CpCqCCpCqrCsr p -> (q -> ((p -> (q -> r)) -> (s -> r)))

C*: CpCqCCpCqrr p -> (q -> ((p -> (q -> r)) -> r))

Tarski proved the theorems K + D and the theorems K + E insured the existence of a single axiom for the system.

Since then the provability of the following pairs proved the existence of a single axiom for the system.

K+C, K+C*, I+E

Yes, thanks John, that is very interesting!

Opps… a English reference for Tarski’s claim is:

Alfred Tarski [1956] Logic, Semantics, Metamathematics, Papers from

1923 to 1938 (Translated by J. H. Woodger), Clarendon Press / Oxford UP,

Oxford UK 1956. (A second revised edition has been issued by J. Corcoran

(ed.), at Hackett Pub. Co., Indianapolis IN, in 19832 .)