Sheffer stroke
The Sheffer stroke, denoted by the vertical bar symbol "|", is a binary logical connective in propositional logic that represents the NAND (not both) operation, yielding true unless both inputs are true.[1] It is defined such that for propositions p and q, p | q is equivalent to \neg (p \land q).[2] This connective is functionally complete on its own, allowing the expression of all other Boolean connectives, including negation, conjunction, and disjunction, through compositions of itself.[1] Its truth table is as follows: | p | q | p | q | |---------|---------|----------| | True | True | False | | True | False | True | | False | True | True | | False | False | True |[1] Introduced by American logician Henry Maurice Sheffer in 1913, the stroke was proposed as a primitive operation in Boolean algebra to simplify axiomatic systems.[3] In his seminal paper, Sheffer demonstrated that a set of five independent postulates using the stroke could define Boolean algebras fully, reducing the need for multiple primitive connectives like negation and inclusive disjunction.[2] This work influenced major texts, including the second edition of Principia Mathematica by Alfred North Whitehead and Bertrand Russell, who adopted it to streamline their logical framework.[1] The Sheffer stroke's significance extends to digital electronics and computer science, where the NAND gate—its hardware implementation—serves as a universal logic gate capable of realizing any Boolean function.[1] All modern digital circuits, from simple processors to complex integrated systems, can be constructed using only NAND gates, underscoring its foundational role in computing technology.[3] Sheffer, born in 1882 in Odessa (then Russia) and later a Harvard professor, contributed this insight amid early 20th-century advances in symbolic logic, though he produced limited further publications.[3]Definition
Truth Table
The Sheffer stroke, denoted as p \mid q, is a binary logical connective that evaluates to true unless both inputs are true.[4] Its truth table, which lists all possible combinations of truth values for the propositions p and q, is as follows:| p | q | p \mid q |
|---|---|---|
| T | T | F |
| T | F | T |
| F | T | T |
| F | F | T |
Logical Equivalences
The Sheffer stroke operation, denoted as p \mid q, is logically equivalent to the negation of the conjunction of p and q, that is, p \mid q \equiv \neg (p \land q).[5] This equivalence holds because the truth table for the Sheffer stroke matches exactly that of the NAND (not both) operation in Boolean logic.[5] A key self-referential equivalence is that applying the Sheffer stroke to a variable with itself yields negation: p \mid p \equiv \neg p. This can be derived from the truth table as follows:| p | p \mid p | \neg p |
|---|---|---|
| T | F | F |
| F | T | T |
| p | q | p \land q | p \mid q | (p \mid q) \mid (p \mid q) |
|---|---|---|---|---|
| T | T | T | F | T |
| T | F | F | T | F |
| F | T | F | T | F |
| F | F | F | T | F |
Notation and Terminology
Alternative Symbols
The Sheffer stroke operation is primarily denoted by the vertical bar symbol |, as p | q, which was introduced by Henry M. Sheffer in his 1913 paper on Boolean algebras.[5] This notation reflects Sheffer's original conceptualization of the stroke as a fundamental connective, later standardized for the NAND function in propositional logic.[1] Common alternative symbols include the upward arrow ↑, as in p ↑ q, which appears in various modern logic texts to distinguish it from other vertical bar usages. Another option is the dedicated Unicode character ⊼ (U+22BC), employed in formal mathematical contexts for precise rendering of the NAND operation.[6] The vertical bar | predominated in early 20th-century logic literature, including Alfred North Whitehead and Bertrand Russell's Principia Mathematica (1925–1927 edition), where it was explicitly termed the "Sheffer stroke."[5] In contrast, the upward arrow ↑ and ⊼ gained traction in mid- to late-20th-century works on symbolic logic and computer science, particularly where clarity in printed or digital formats was prioritized.[1] Symbol selection has evolved primarily due to typesetting constraints in early publications, which limited access to specialized glyphs, and to mitigate potential confusion with the vertical bar's roles in other mathematical notations, such as set membership or conditional statements.[5]Names and Synonyms
The Sheffer stroke is named in honor of the American philosopher and logician Henry M. Sheffer, who formalized its role in propositional logic in his 1913 paper.[5] Logically, it is synonymous with NAND, an abbreviation for "NOT AND," which negates the conjunction of its two inputs, yielding true unless both are true.[1] In philosophical and logical contexts, it is also termed alternative denial, as it asserts that at least one of the propositions is false.[7] The operation has been called joint denial in some early treatments, reflecting its denial of simultaneous truth, though this name is more standardly applied to its dual, the NOR connective. Additionally, the Peirce arrow—named for Charles Sanders Peirce, who sketched related ideas in the late 19th century—has been linked to the Sheffer stroke in historical discussions, though its application remains debated and is typically reserved for the NOR operation.[5] In computing and digital electronics, it is commonly designated as the NAND gate, a fundamental building block for logic circuits.[1] Within Boolean algebra, the connective is often specified as Sheffer's operation, emphasizing its functional completeness.[8]Historical Development
Invention
Henry Maurice Sheffer, an American logician and mathematician, introduced the operation now associated with the Sheffer stroke in his 1913 paper titled "A Set of Five Independent Postulates for Boolean Algebras, with Application to Logical Constants," published in the Transactions of the American Mathematical Society.[9] In this work, Sheffer sought to simplify the axiomatization of Boolean algebras by reducing the number of primitive ideas and propositions required, motivated by the desire to streamline logical systems while preserving their expressive power.[9] Sheffer defined the operation, denoted by the vertical stroke symbol "|", as a binary connective representing "rejection." Specifically, for propositions p and q, p | q is interpreted as the proposition "neither p nor q," which corresponds to the negation of their disjunction, \neg (p \lor q).[9] This definition aligns with the logical constant "neither-nor," and its truth table is true only when both inputs are false (NOR operation).[9] The key innovation in Sheffer's paper was his proof that this single binary operation, combined with the class of elements K, suffices to define all Boolean functions through a set of five independent postulates.[9] By demonstrating that traditional primitives like negation and disjunction could be derived from rejection alone—via theorems showing, for instance, that p | p yields the negation of p and other expressions produce disjunction—Sheffer established the potential for a minimal primitive basis in Boolean algebra, anticipating the concept of functional completeness.[9] This approach predated similar reductions in other mathematical and logical domains by emphasizing the sufficiency of one connective for comprehensive expressiveness.[9]Recognition and Influence
Following Henry M. Sheffer's publication of his findings in 1913, the Sheffer stroke received limited immediate attention within the logical community, as his work appeared in a specialized mathematical journal and was not widely disseminated at the time.[5] It was not until the early 1920s that the operation gained broader recognition, particularly through analyses by logicians such as Jean Nicod, who in 1917–1919 explored axiomatizations using a similar stroke operation equivalent to NAND (not both), and Emil L. Post, who in 1921 provided a systematic treatment of functional completeness in propositional logic, demonstrating that binary connectives like the Sheffer stroke could generate all truth functions.[10] Post's work in his dissertation "Introduction to a General Theory of Elementary Propositions" highlighted the stroke's role in simplifying logical systems, marking a key milestone in the development of truth-functional completeness theorems.[5] The operation's prominence surged with its formal naming as the "Sheffer stroke" by Alfred North Whitehead and Bertrand Russell in the second edition of Principia Mathematica (1925–1927), where they incorporated the vertical bar "|" as the sole primitive connective for propositional logic, but defined it as the NAND operation (\neg (p \land q), "not both") rather than Sheffer's original NOR.[3][5] This endorsement by Russell and Whitehead, who described it as a significant advance in mathematical logic, integrated the stroke into foundational efforts like Hilbert's program for the formalization of mathematics, where efficient axiomatizations of Boolean algebra were essential for consistency proofs in arithmetic and beyond.[11] Ludwig Wittgenstein also acknowledged its philosophical implications in his Tractatus Logico-Philosophicus (1922), using it to illustrate the expressive power of elementary logical forms.[5] In the mid-20th century, the Sheffer stroke—as the NAND operation—influenced the foundations of switching theory and early computer design, notably through Claude E. Shannon's 1938 thesis "A Symbolic Analysis of Relay and Switching Circuits," which applied Boolean algebra—including connectives equivalent to the stroke—to electrical engineering, enabling the logical design of complex circuits with minimal components. This connection clarified the stroke's practical utility in realizing functional completeness with a single operation, paving the way for efficient gate implementations in digital systems. Post's later 1941 elaboration on hereditary properties further solidified its theoretical impact, emphasizing why the stroke avoids preserving certain logical classes like monotonicity or linearity, thus distinguishing it in completeness criteria.[5] Although Charles Sanders Peirce sketched ideas resembling the stroke's functional completeness in an 1880 manuscript (MS 378), using an operator for "not-A and not-B" (NOR), Sheffer's 1913 proof provided the definitive formal demonstration of its sufficiency as a sole connective, resolving earlier informal anticipations and establishing his contribution as the pivotal advancement.[10]Properties
Functional Completeness
Functional completeness refers to the property of a logical connective that allows it to serve as the sole primitive operation for expressing every possible truth function in propositional logic. In the case of the Sheffer stroke (denoted ↓, equivalent to the NAND operation), this means it can generate a functionally complete set such as {¬, ∧} or {¬, ∨}, from which all Boolean functions can be derived via composition.[12][5] The proof of this universality proceeds by explicitly constructing the standard basis connectives using only ↓. First, negation is obtained as\neg p \equiv p \downarrow p,
since p \downarrow p = \neg(p \wedge p) = \neg p.[12][13] Next, conjunction is expressed as
p \wedge q \equiv (p \downarrow q) \downarrow (p \downarrow q),
which simplifies to \neg(\neg(p \wedge q) \wedge \neg(p \wedge q)) = \neg\neg(p \wedge q) = p \wedge q.[13][5] Disjunction follows using De Morgan's law:
p \vee q \equiv (p \downarrow p) \downarrow (q \downarrow q),
since \neg p \downarrow \neg q = \neg(\neg p \wedge \neg q) = p \vee q.[12] Material implication is constructed as
p \to q \equiv (p \downarrow q) \downarrow p,
which equals \neg(\neg(p \wedge q) \wedge p) = (p \wedge q) \vee \neg p = \neg p \vee q.[5] Alternatively, it can be written as p \downarrow (q \downarrow q) = \neg(p \wedge \neg q) = \neg p \vee q.[5] These constructions establish that {↓} is functionally complete, as {¬, ∧, ∨} (or equivalents) suffice for all Boolean functions.[12] Henry M. Sheffer provided the first explicit demonstration of this single-primitive basis in his 1913 paper on Boolean algebra postulates.[2]