 We saw earlier that combining the intuitionistic and classical rules in a single proof system did not work well, and another suggestion that comes to mind is that we could perhaps extend intuitionistic logic with a new connective, 1-ary #, say, which does what according to the intuitionist, negation (¬) itself cannot do: serve as a left inverse for ¬ in the sense of rendering equivalent #¬φ and φ for all  φ.[35]  This again represents an offer the intuitionist cannot afford to accept, assuming that any (the rules for any) proposed new connectives should conserve synonymy, as suggested above. (The even stronger demand that the consequence relation associated with the extended proof systems should be congruential does not seem unreasonable.) The reason is that ¬p and ¬¬¬p are intuitionistically equivalent (and thus synonymous according to ⊢I L) so the conservation of synonymy requires that #¬p and #¬¬¬p should be equivalent—since we have this ‘Law of Triple Negation’ equivalence in intuitionistic logic—from which the left inverse condition above delivers, taking φ as ¬p in the former case and as ¬¬¬p in the latter, the equivalence of p with ¬¬p—a straightforwardly non-conservative extension, then. (A similar argument shows that adding binary # with φ # (φ ↔ ψ) equivalent to ψ—a possibility suggesting itself since, by contrast with the classical case, ↔ itself cannot serve as # here—is also non-conservative.) Nor, incidentally, could the intuitionist acknowledge the existence of a right inverse for negation, a # with arbitrary φ equivalent to ¬ # φ, as this makes every formula equivalent to a negated formula and hence to its own double negation. This argument, which is well known (see, e.g., Koslow (1992), p. 97), does not even require the ‘conservation of synonymies’ constraint.