Non-null implication
David B. Nelson · Journal of Symbolic Logic · 1997
An implication A ⊃ B is said to be null in case A is false in all instances. This note describes several formal systems for first-order predicate logic and arithmetic in which null implications do not occur. In fact, the most restrictive systems avoid the occurrences of any formulas which represent null predicates. The precise sense of this avoidance is explained below. An intuitionistic negation is a statement of the form A ⊃ F where F is a contradiction. The absence of null implications among true statements entails the absence of intuitionistic negations, and hence systems described here might be called negationless intuitionistic systems.