MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  wn Structured version   Visualization version   GIF version

Syntax Definition wn 3
Description: If 𝜑 is a wff, so is ¬ 𝜑 or "not 𝜑". Part of the recursive definition of a wff (well-formed formula). In classical logic (which is our logic), a wff is interpreted as either true or false. So if 𝜑 is true, then ¬ 𝜑 is false; if 𝜑 is false, then ¬ 𝜑 is true. Traditionally, Greek letters are used to represent wffs, and we follow this convention. In propositional calculus, we define only wffs built up from other wffs, i.e. there is no starting or "atomic" wff. Later, in predicate calculus, we will extend the basic wff definition by including atomic wffs (weq 1967 and wel 2109).
Hypothesis
Ref Expression
wph wff 𝜑
Assertion
Ref Expression
wn wff ¬ 𝜑

This syntax is primitive. The first axiom using it is ax-3 8.

Colors of variables: wff setvar class
  Copyright terms: Public domain W3C validator