 These two connexive logics arise from the idea of negation as cancellation in a straightforward way. They are neither monotonic nor closed under uniform substitution. Proof systems and decision procedures for them can be obtained from a straightforward faithful translation τ into the modal logic S5, cf. the entry  logic: modal.  For implications A → B the translation is defined as follows, where ⊃ is material implication and ¬ is classical negation: