Syntax Definition wn 3

Description: If 𝜑 is a wff, so is ¬ 𝜑 or "not 𝜑". Part of the recursive definition of a wff (well-formed formula). 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 1503 and wel 2149).

Hypothesis

Ref	Expression
wph	wff 𝜑

Assertion

Ref	Expression
wn	wff ¬ 𝜑

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