![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > df-nan | Structured version Visualization version GIF version |
Description: Define incompatibility, or alternative denial ("not-and" or "nand"). See dfnan2 1493 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 1545) and the constant false ⊥ (df-fal 1555), we will be able to prove these truth table values: ((⊤ ⊼ ⊤) ↔ ⊥) (trunantru 1583), ((⊤ ⊼ ⊥) ↔ ⊤) (trunanfal 1584), ((⊥ ⊼ ⊤) ↔ ⊤) (falnantru 1585), and ((⊥ ⊼ ⊥) ↔ ⊤) (falnanfal 1586). Contrast with ∧ (df-an 398), ∨ (df-or 847), → (wi 4), and ⊻ (df-xor 1511). (Contributed by Jeff Hoffman, 19-Nov-2007.) |
Ref | Expression |
---|---|
df-nan | ⊢ ((𝜑 ⊼ 𝜓) ↔ ¬ (𝜑 ∧ 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | wph | . . 3 wff 𝜑 | |
2 | wps | . . 3 wff 𝜓 | |
3 | 1, 2 | wnan 1490 | . 2 wff (𝜑 ⊼ 𝜓) |
4 | 1, 2 | wa 397 | . . 3 wff (𝜑 ∧ 𝜓) |
5 | 4 | wn 3 | . 2 wff ¬ (𝜑 ∧ 𝜓) |
6 | 3, 5 | wb 205 | 1 wff ((𝜑 ⊼ 𝜓) ↔ ¬ (𝜑 ∧ 𝜓)) |
Colors of variables: wff setvar class |
This definition is referenced by: nanan 1492 dfnan2 1493 nanor 1494 nanbi 1499 xornan2 1520 trunanfal 1584 nic-mpALT 1675 nic-ax 1676 nic-axALT 1677 nfnan 1904 elnanel 9544 naim1 34864 naim2 34865 df3nandALT1 34874 imnand2 34877 waj-ax 34889 lukshef-ax2 34890 arg-ax 34891 nandsym1 34897 tsna1 36606 tsna2 36607 tsna3 36608 ifpdfnan 41765 ifpnannanb 41786 nanorxor 42592 undisjrab 42593 |
Copyright terms: Public domain | W3C validator |