Description: Define incompatibility,
or alternative denial ('not-and' or 'nand'). 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 1325) and the constant false (df-fal 1326), we will be
able to prove these truth table values: 
(trunantru 1360), 
(trunanfal 1361),

(falnantru 1362), and

(falnanfal 1363). Contrast with
(df-an 361), (df-or 360), (wi 4), and
(df-xor 1311) . (Contributed by Jeff Hoffman,
19-Nov-2007.) |