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 (weq1733 and wel1819).

Hypothesis

Ref

Expression

wph

Assertion

Ref

Expression

wn

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