Until this book, very little work appears to have been done on finding short axioms for logic in terms of Nand .

So for ordinary logic both Nand and Nor work. … For ordinary logic based on Nand it turns out that there are no other finite representations (though there are other infinite ones).

The network of statements that can be proved true using the axiom system for logic from page 775 . p ⊼ (p ⊼ p) is the simplest representation for True when logic is set up using the Nand operator ⊼ .

Nand and Nor are mostly used only in circuit design and in a few foundational studies of logic.

The function Nand[a_, b_] := Not[And[a, b]] used in the main text turns out to be universal for any k .

The operators shown are And , Equal , Implies and Nand .

And the reason is that just the six theorems highlighted already happen to form an axiom system from which any possible theorem about Nands can ultimately be derived.

The "Sheffer version" based on Nand (see page 1173 ) was given by Henry Sheffer in 1913. … In 1948 Jan Łukasiewicz found the single axiom version {((a  (b  a))  (((( ¬ c)  (d  ( ¬ e)))  ((c  (d  f))  ((e  d)  (e  f))))  g))  (h  g)} equivalent for example to {(( ¬ a)  (b  ( ¬ c)))  ((a  (b  d))  ((c  b)  (c  d))), a  (b  a)} It turns out to be possible to convert any axiom system that works with modus ponens (and supports the properties of  ) into a so-called equational one that works with equivalences between expressions by using Module[{a}, Join[Thread[axioms  a  a], {((a  a)  b)  b, ((a  b)  b)  (b  a)  a}]] An analog of modus ponens for Nand is {x, x, ⊼ (y ⊼ z)}  z , and with this Jean Nicod found in 1917 the single axiom {(a ⊼ (b ⊼ c)) ⊼ ((e ⊼ (e ⊼ e)) ⊼ ((d ⊼ b) ⊼ ((a ⊼ d) ⊼ (a ⊼ d))))} which was highlighted in the 1925 edition of Principia Mathematica .

The picture below shows in each of the axiom systems from page 808 the lengths of the shortest proofs found by a version of Waldmeister (see page 1158 ) for all 582 equivalences (see page 818 ) that involve two variables and up to 3 Nand s on either side.

A standard form in terms of Nand can be constructed essentially by direct translation of DNF; other methods can be used for the various other operators shown.