The requirement that falsity of (A → B) implies that if A is true then B is not true cannot be expressed in a language with only one negation expressing falsity

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 tha