Primitive symbol. Logical negation.
If phi is a wff, so is [not] phi or "not phi". In classical logic (which is our logic), a wff is interpreted as either true or false. So if phi is true, then not phi is false; if phi is false, then not phi 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 extent the basic wff definition by including atomic wffs.
pr
(pr),