Sheffer stroke
|
|
NAND.jpg
The Sheffer stroke, |, also called joint denial and in Boolean algebra and digital circuitry known as the NAND (Not AND) operation, is a logical operator which is the negation of the conjunction operator. It can be used by itself, without any other logical operator, to constitute a logical formal system. It is named for Henry M. Sheffer, who proved that all the usual operators of logical calculus (not, and, or, implies) could be expressed in terms of it.
| Contents |
NAND
A common means of writing p NAND q is <math>\overline{p \cdot q}<math>, where the symbol <math>\cdot<math> signifies AND and the line over the expression signifies not, the logical negation of that expression.
The two-input logical NAND operator is commonly described by a truth table, describing the output state for all possible input combinations:
| A | B | A nand B |
|---|---|---|
| F | F | T |
| F | T | T |
| T | F | T |
| T | T | F |
Expressed in terms of NAND, the usual operators of propositional calculus are:
| "not p" is equivalent to "p NAND p" | <math>\overline{p} \equiv \overline{p \cdot p}<math> |
| "p and q" is equivalent to "(p NAND q) NAND (p NAND q)" | <math>p \cdot q \equiv \overline{\overline{(p \cdot q)} \cdot \overline{(p \cdot q)}}<math> |
| "p or q" is equivalent to "(p NAND p) NAND (q NAND q)" | <math>p + q \equiv \overline{\overline{(p \cdot p)} \cdot \overline{(q \cdot q)}}<math> |
| "p implies q" is equivalent to "(p NAND q) NAND p" | <math>p \rightarrow q \equiv \overline{\overline{(p \cdot q)} \cdot p}<math> |
This leads to an alternative axiom system for boolean algebras that needs only one operation.
Digital systems that require use of certain logic circuits take advantage of this property. In complicated logical expressions, normally written in terms of other logic functions such as AND, OR, and NOT, writing these in terms of NAND allows for cheaper construction because in many schemes for implementing such circuits, the NAND gate is more compact than these other gates.
There is another logical operator which is sufficient to express all the others: NOR.
Sheffer stroke
Using the stroke notation, |, the Sheffer stroke is equivalent to the negation of conjunction:
- <math> A | B = \neg (A \wedge B). <math>
Its operation can be defined semantically by the following table:
| <math>|<math> | F | T |
|---|---|---|
| F | T | T |
| T | T | F |
The Sheffer stroke is commutative but not associative. The other logical operators can be defined in terms of it, like so:
- <math> \neg A = A | A, <math>
- <math> A \wedge B = (A | B) | (A | B), <math>
- <math> A \vee B = (A | A) | (B | B), <math>
- <math> A \rightarrow B = A | (B | B) = A | (A | B). <math>
Formal system based on the Sheffer stroke
The following is an example of a formal system based entirely on the Sheffer stroke, but which has the functional expressiveness of propositional calculus:
1. Symbols
A B C D E F G '
( | )
2. Grammar
The letters A, B, C, D, E, F and G are atoms.
Any of these letters primed once or several times is also an atom (e.g. A', B′′, C′′′, D′′′′ are atoms).
Construction Rule I: An atom is a well-formed formula.
Construction Rule II: If X and Y are well-formed formulae, then (X|Y) is a well-formed formula.
Closure Rule: Any formulae which cannot be constructed by means of the first two Construction Rules is not a well-formed formula.
A decision procedure for determining whether a formula is a well-formed formula is the following: "deconstruct" the formula by applying the Construction Rules backwards, thereby breaking the formula into smaller subformulae. Then repeat this recursive deconstruction process to each of the subformulae. Eventually the formula should be reduced to its atoms, but if some subformula cannot be so reduced, then the formula is not a well-formed formula.
3. Axiom
(Letters U, V, X are metavariables which stand for well-formed formulae, and the following wff′s are axiom schemata which become axioms when all their metavariables have been replaced by wff′s.)
THEN-1: (U|(U|(V|(U|U))))
4. Inference Rules
(In the following inference rules, letters U, V, X, Y are metavariables which stand for well-formed formulae. Also, an equation means that if one side of the equation is part of a theorem, and if this side is replaced by the other side of the equation, the resulting formula is also a theorem.)
Commutativity: (X|Y) = (Y|X)
Duality: If strings of the forms X and (X|X) both show up in a theorem, then if these two strings are swapped wherever they appear in the theorem, then the result will also be a theorem.
Double Negation: ((X|X)|(X|X)) = X
Mimesis: (U|(X|X)) = (U|(U|X))
THEN-3: (U|(U|(V|(V|X)))) = (V|(V|(U|(U|X))))
MP-1: U, (U|(V|X)) |- V
MP-2: U, (U|(V|X)) |- X
Note: MP-1 and MP-2 are the analogues of modus ponens. The formula (U|(V|X)) can be interpreted as meaning U→V∧X. MP-1 and MP-2 correspond exactly to MP when V and X are identical.
Simplification
Since the only connective of this logic is the disjoint union, the symbol | could be discarded altogether (being replaced by spaces), leaving only the parentheses to group the letters. A restriction on the grouping with parentheses is that a pair of parentheses must always enclose a pair of wffs. Examples of a theorems in this simplified notation are
- (A (A (B (B ((A B) (A B)))))),
- (A (A ((B B) (A A)))),
which are seen to have a LISP-like appearance.
Reference
- 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.