 The example above used an interpreted language with atomic sentences Sat and Sun. The inset equivalence presented involving them would not be reasonable for all sentences. Modulating back to the issue of a formal propositional logic involving the envisaged new connective, such an equivalence would not be reasonable for arbitrary φ and ψ in place of them, since we would expect the new connective to be congruential according to the desired consequence relation, and any unrestricted such equivalence would then deliver from φ1 ∧ ψ ⊣⊢ φ2 ∧ ψ—by “subtracting ψ from both sides” (in view of congruentiality)—the conclusion that φ1 ⊣⊢ φ2, and it easy to find counterexamples to such cancellation inferences for even quite weak initial logics. Since the counterexamples arise for φ1, φ2, in the language unexpanded by “−”, the sense in which a generalized version of the earlier equivalence would not be reasonable is that it would not be conservative over the initial logic. Here we say no more about how to constrain the equivalence in question, or, more generally, about whether there really is any such logical subtraction connective as we have been  envisaging.[45]