 Whereas the direction from right to left of Axiom a5 can be justified by rejecting the view that if A implies B and A is inconsistent, A implies any formula, in particular B, the direction from left to right seems rather strong. If the verification conditions of implications are dynamic (in the sense of referring to other states in addition to the state of evaluation), then a5 indicates that the falsification conditions of implications are dynamic as well. The falsity of (A → B) thus implies that if A is true, B is false. Yet, one might wonder why it is not required that the falsity of (A→ B) implies that if A is true, B is not true. This cannot be expressed in a language with just one negation, ~, expressing falsity instead of absence of truth (classically at the state of evaluation or intuitionistically at all related states). If one adds to C the further axiom ~A → (A → B) to obtain a connexive variant of Nelson’s three-valued logic N3, intuitionistic negation ¬ is definable by setting: ¬A := A → ~A. Then a5 might be replaced by