| Description: Define incompatibility,
or alternative denial ("not-and" or "nand"). See
dfnan2 1494 for an alternative. This is also called the
Sheffer stroke,
represented by a vertical bar, but we use a different symbol to avoid
ambiguity with other uses of the vertical bar. In the second edition of
Principia Mathematica (1927), Russell and Whitehead used the Sheffer
stroke and suggested it as a replacement for the "or" and
"not" operations
of the first edition. However, in practice, "or" and
"not" are more
widely used. After we define the constant true ⊤ (df-tru 1543) and
the constant false ⊥ (df-fal 1553), we will be able to prove these
truth table values: ((⊤ ⊼ ⊤) ↔
⊥) (trunantru 1581),
((⊤ ⊼ ⊥) ↔ ⊤) (trunanfal 1582), ((⊥ ⊼ ⊤)
↔ ⊤)
(falnantru 1583), and ((⊥ ⊼
⊥) ↔ ⊤) (falnanfal 1584).
Contrast with ∧ (df-an 396), ∨ (df-or 849), → (wi 4), and
⊻ (df-xor 1512). (Contributed by Jeff Hoffman,
19-Nov-2007.) |