Metamath Proof Explorer


Syntax definition wn

Description: If ph is a wff, so is -. ph or "not ph ". 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 ph is true, then -. ph is false; if ph is false, then -. ph 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 and wel ).

Ref Expression
Assertion wn wff ¬ 𝜑