NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  df-nan GIF version

Definition df-nan 1288
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 1319) and the constant false (df-fal 1320), we will be able to prove these truth table values: (( ⊤ ⊤ ) ↔ ⊥ ) (trunantru 1354), (( ⊤ ⊥ ) ↔ ⊤ ) (trunanfal 1355), (( ⊥ ⊤ ) ↔ ⊤ ) (falnantru 1356), and (( ⊥ ⊥ ) ↔ ⊤ ) (falnanfal 1357). Contrast with (df-an 360), (df-or 359), (wi 4), and (df-xor 1305) . (Contributed by Jeff Hoffman, 19-Nov-2007.)
Assertion
Ref Expression
df-nan ((φ ψ) ↔ ¬ (φ ψ))

Detailed syntax breakdown of Definition df-nan
StepHypRef Expression
1 wph . . 3 wff φ
2 wps . . 3 wff ψ
31, 2wnan 1287 . 2 wff (φ ψ)
41, 2wa 358 . . 3 wff (φ ψ)
54wn 3 . 2 wff ¬ (φ ψ)
63, 5wb 176 1 wff ((φ ψ) ↔ ¬ (φ ψ))
Colors of variables: wff setvar class
This definition is referenced by:  nanan  1289  nancom  1290  nannan  1291  nannot  1293  nanbi  1294  nanbi1  1295  trunanfal  1355  nic-mpALT  1437  nic-ax  1438  nic-axALT  1439  nfnan  1825  elcomplg  3218  elin  3219  elun  3220  nincompl  4072
  Copyright terms: Public domain W3C validator