 If we were doing classical logic with multisets, we would need the structural rules (Id), (Weakening) and (Cut) from Section  2,  set-variables now reinterpreted as multiset variables, and the further rule of Contraction to allow double occurrences of formulas on the left or right of the ≻ to be replaced by single occurrences. For linear logic we retain only (Id) and (Cut), disallowing weakenings and contractions, which has the effect that there are now also two versions of conjunction and of disjunction, multiplicative and additive—into which distinction we cannot go further here, except to say that for binary connectives it lines up with the intensional/extensional distinction in the relevance  tradition.[26]  A sequent calculus presentation of the favoured logic from this tradition, R, can be obtained from that for Classical Linear Logic (without two of its characteristic 1-ary connectives, called exponentials, which are there to mark formulas for which weakening and contraction are permitted) by allowing contraction (while still banning  weakening).[27]  We return to R in Example 6 of Section  4;  it is for the sake of that return that the rules governing t and T have been given here alongside those for f and F, the latter pair being of current interest. Notice that even though there is only one rule for F, namely a left insertion rule (with no premiss sequents), this rule suffices to characterize F uniquely, since in the combined language with F′ governed by a like rule we can prove—just by appealing to the appropriate instance of the rule F ≻ F′ and F′ ≻ F. The weaker system of Intuitionistic Linear Logic is cast in the framework Mset-Fmla0 disallowing the appearance of more than one formula on the right, and this application of the left rule for F is available there, as also in Mset-Fmla, requiring exactly one formula on the right (since we have exactly one formula—F or F′—there in the present case). When we turn to f, again we find that the rules uniquely characterize this connective, since (f Left) provides the premiss for an application of (f′ Right) with Γ consisting of (one occurrence of) f and Δ empty, yielding f ≻ f′, with the converse proved similarly. (Note that while F ≻ f is a special case of the (left) rule for F, there is no proof of the converse sequent. One cannot begin with f ≻ and then weaken in an F on the right, since we do not have  Weakening.[28])  Again, these derivations go through in Mset-Fmla0, but this time we note that they do not go through in Mset-Fmla, since the left insertion rule has no applications in that framework. When attention is restricted to Mset-Fmla, there is no set of pure rules available which uniquely characterize f. The Mset-Mset (or Mset-Fmla0) sequent calculus rules for ¬, which can be taken to be those given in Section  2  with the set-variables taken as multiset-variables (suitably restricted for Mset-Fmla0), uniquely characterize ¬, but have no direct application in Mset-Fmla or any other framework with a fixed multiset cardinality on the right (or the left, for that matter). We can say in this framework that the rules governing ¬ uniquely characterize this connective in terms of → and f—on the basis of which it would indeed be explicitly definable (¬ φ as φ → f), but since here f is not uniquely characterized (even though → is), this still leaves ¬ without its (perhaps) expected uniqueness, as is even more evident in Fmla. These considerations continue to apply in the presence of contraction (and ∧/∨) distribution, accounting for the complaint sometimes made that relevant logic does not operate with a uniquely characterized negation. The point here has not been either to press or to reply to such complaints, but to note their framework sensitivity: they do not arise for Mset-Mset or Mset-Fmla0.