 This expresses the convention that an atomic formula cannot be true unless its terms refer. Second, because all empty-termed identity statements are false on a negative semantics, (A7) is invalid and must be replaced by (A7-). Third, since (A2), (A3), (A-) and (A7-) together imply (A5), (A5) may be omitted. The resulting logic is known as NFL (Negative Free Logic). For languages with function symbols, negative free logic requires in addition this axiom of strictness: