In logic, the Sheffer's stroke, also called joint denial, is a logical operator analogous to a NAND logic gate which can be used by itself, without any other logical operator, to constitute a logical formal system. It is the negation of conjunction:
Its truth table is
Sheffer's stroke is commutative but not associative. Other logical operators can be defined in terms of it, like so:
Formal system based on Sheffer's stroke
The following is an example of a formal system based entirely on the Sheffer's 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 Summary
(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.)
SH1: (U|(U|(V|(U|U))))
SH2:
((U|(U|(V|(X|X))))|((U|(U|(V|(X|X))))|((U|(U|V))|((U|(X|X))|(U|(X|X))))))
4. Inference Rules
(In the following inference rules, letters U, V, X, Y are metavariables which stand for well-formed formulae.)
Commutativity: If a string of the form (X|Y) shows up in a theorem, then if this string is replaced by the string (Y|X), then the result will also be a theorem.
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: If the string ((X|X)|(X|X)) shows up in a theorem, and if this string is replaced by the string X, then the result will also be a theorem. Likewise, if the string X shows up in a theorem, and if this string is replaced by the string ((X|X)|(X|X)), then the result will also be a theorem.
Mimesis: If a string of the form (U|(X|X)) shows up in a theorem, then if this string is replaced by the string (U|(U|X)), then the result will also be a theorem. Likewise, if the string (U|(U|X)) shows up in a theorem, and if this string is replaced by the string (U|(X|X)), then the result will also be a theorem.
MP: U, (U|(V|V)) |- V
MP Dual: U, (U|V) |- (V|V)
Simplification
Since the only connective of this logic is the disjoint union, the symbol | can 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.
