{'fraction_non_alphanumeric': 0.06135531135531135, 'fraction_numerical': 0.007312735573605139, 'mean_word_length': 3.6728062015503875, 'pattern_counts': {'":': 0, '<': 0, '<?xml version=': 0, '>': 0, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 53, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
An Abstract Approach to Consequence Relations

We generalise the Blok-J\'onsson account of structural consequence relations, later developed by Galatos, Tsinakis and other authors, in such a way as to naturally accommodate multiset consequence. While Blok and J\'onsson admit, in place of sheer formulas, a wider range of syntactic units to be manipulated in deductions (including sequents or equations), these objects are invariably aggregated via set-theoretical union. Our approach is more general in that non-idempotent forms of premiss and conclusion aggregation, including multiset sum and fuzzy set union, are considered. In their abstract form, thus, deductive relations are defined as additional compatible preorderings over certain partially ordered monoids. We investigate these relations using categorical methods, and provide analogues of the main results obtained in the general theory of consequence relations. Then we focus on the driving example of multiset deductive relations, providing variations of the methods of matrix semantics and Hilbert systems in Abstract Algebraic Logic.


Logical consequence: The Blok-Jónsson approach
Let L be a propositional language (or, which is the same, an algebraic language). According to the standard textbook definition, a Tarskian consequence relation (tcr) on L is a relation ⊢ ⊆ ℘(Fm L ) × Fm L obeying the following conditions for all X, Y ⊆ Fm L and ϕ ∈ Fm L : • X ⊢ ϕ whenever ϕ ∈ X. (Reflexivity) • If X ⊢ ϕ and X ⊆ Y , then Y ⊢ ϕ. (Monotonicity) • If Y ⊢ ϕ and X ⊢ ψ for every ψ ∈ Y , then X ⊢ ϕ.
Tarskian consequence relations are the primary object of study of Abstract Algebraic Logic (AAL: see e.g. [7,11,12,14,15]), a discipline that aims at providing general tools for the investigation and comparison of the different brands of propositional logics on the market. Among the reasons why AAL has established itself as a mainstream approach there is its success in effectively accommodating all the main extensions of, and alternatives to, classical propositional logic: intuitionistic logic, modal logics, relevant logics, quantum logics, and whatnot.
Although tcr's are perfectly adequate for the needs of a wide spectrum of such abstract metalogical enquiries, it gradually emerged that they fail to capture a range of situations where we are still reasoning from given premisses to certain conclusions according to the same three principles of Reflexivity, Monotonicity, and Cut, yet we are not manipulating formulas of a given language, but perhaps sequents (as in Gentzen calculi) or equations (as in equational consequence relations associated with classes of algebras). Actually, it is not unusual for a logic to be given alternative presentations as a "consequence relation" of sorts over different sets of syntactic units. For example, classical logic can be presented not only as a (syntactically or semantically defined) tcr, but also as the derivability relation of the classical sequent calculus, or as the equational consequence relation of the 2-element Boolean algebra. In order to subsume these generalisations of the concept of propositional logic, core AAL was extended to k-dimensional systems [8] and, subsequently, to Gentzen systems [29,30,31,32,28,36]. The proliferation of these extensions of the classical AAL theory suggests that the idea of abstracing away from the specifics of these presentations to pinpoint what is essential to a logic is not without its allure.
In their groundbreaking paper [6] (see also the lecture notes [5] of the course "Algebraic structures for logic" that inspired the paper), Wim Blok and Bjarni Jónsson take their cue from such reflections and suggest to replace the set Fm L in the definition of tcr by an arbitrary set A: Definition 1. An abstract consequence relation (acr) on the set A is a relation ⊢ ⊆ ℘ (A) × A obeying the following conditions for all X, Y ⊆ A and for all a ∈ A: • X ⊢ a whenever a ∈ X. (Reflexivity) • If X ⊢ a and X ⊆ Y , then Y ⊢ a. (Monotonicity) • If Y ⊢ a and X ⊢ b for every b ∈ Y , then X ⊢ a. (Cut) The first conceptual hurdle for this general approach is providing a suitable account of logical consequence. It is generally agreed that logical consequence, as opposed to consequence in general, is a matter of logical form. In the standard AAL framework, this requirement is rendered precise by adding to the three Tarskian postulates the further condition of substitution-invariance. Accordingly, a tcr ⊢ on L is said to substitution-invariant if for all X ∪ {ϕ} ⊆ Fm L , whenever X ⊢ ϕ we also have that σ (X) ⊢ σ (ϕ), where σ is an arbitrary Lsubstitution (namely, an endomorphism of the formula algebra Fm L ) and σ (X) is defined pointwise. It is clear enough that replacing the algebra Fm L by the unstructured set A, which behaves as a sort of "black box" in so far as no notion of endomorphism is applicable to it, calls for a completely different account of substitution-invariance. Blok and Jónsson's response to this problem is insightful. They observe that the application of substitutions to propositional formulas (or, for that matter, to equations or sequents) is reminiscent of an operation of multiplication by a scalar. In fact, if L is a language, ϕ is an L-formula and σ 1 , σ 2 are L-substitutions, then (σ 1 • σ 2 ) (ϕ) = σ 1 (σ 2 (ϕ)), and if ι is the identity L-substitution, ι (ϕ) = ϕ. Generalising this example, we are led to the following abstract counterpart of substitution-invariance. We say that a monoid M = M, ·, 1 acts on a set A if there is a map ⋆ : M × A → A s.t. for all m 1 , m 2 ∈ M and all a ∈ A, (m 1 · m 2 ) ⋆ a = m 1 ⋆ (m 2 ⋆ a) and 1 ⋆ a = a. Thus, an acr ⊢ is said to be M-action-invariant if for all X ∪ {a} ⊆ A and m ∈ M , whenever X ⊢ a we also have that {m ⋆ x : x ∈ X} ⊢ m ⋆ a.
For future reference, we need to observe that if M acts on A, then ℘ (M) = ℘ (M ) , · ′ , {1} (where · ′ is complex product) acts on ℘ (A) via the induced map One striking feature of Blok and Jónsson's suggestion is that it allows to reformulate, at a very general level, the classical notion of algebraisability [7], in a way that provides a uniform perspective on the algebraisation of logics and Gentzen systems. We remind the reader that a logic ⊢ (i.e., a substitutioninvariant tcr) is algebraisable [7] if there exist a generalized quasi-variety K and two maps τ : ℘(Fm L ) ←→ ℘(Eq L ) : ρ which commute with unions and substitutions, such that for every X ∪ {ϕ} ⊆ Fm L . In the displays above, Eq L is the set of L-equations (formally cast as ordered pairs of L-formulas), and |= K the equational consequence relation of K. When the above conditions hold, K is unique and is said to be the equivalent algebraic semantics of ⊢. Given a logic ⊢ and a generalized quasi-variety K, we denote by C ⊢ and C K the closure operators associated to the relations ⊢ and |= K respectively. It is well-known (see e.g. [12, p. 149]) that the notion of algebraisability is captured by the existence of a particular isomorphism: Theorem 2 (Syntactic Isomorphism Theorem). Let ⊢ be a logic and K a generalised quasi-variety. Moreover, let T h(⊢) and T h(|= K ) be the complete lattices of theories (i.e., such sets that ϕ ∈ T whenever T ⊢ ϕ; analogously for |= K ) of ⊢ and |= K , respectively. Then ⊢ is algebraisable with equivalent algebraic semantics K if and only if there is a lattice isomorphism Φ : T h(⊢) → T h(|= K ) such that Φ • C ⊢ • σ = C K • σ • Φ for every substitution σ.
Blok and Jónsson introduced the following natural generalisation of the concept of algebraisability, based on the criterion provided by the Syntactic Isomorphism Theorem. Let M be a monoid acting on two sets A 1 and A 2 , respectively through the actions ⋆ 1 and ⋆ 2 . Moreover, let ⊢ 1 and ⊢ 2 be two M-action invariant acr's, respectively on A 1 and A 2 . The acr's ⊢ 1 and ⊢ 2 are said to be equivalent if their lattices of closed sets, when suitably enriched with the actions of the monoid M, are isomorphic (see [5,Definition 4.5]). Observe that, in the light of the Syntactic Isomorphism Theorem, a logic ⊢ is algebraisable with equivalent algebraic semantics K if and only if the substitution-invariant acr's ⊢ and |= K are equivalent according to this definition (where M is the monoid of substitutions, acting in the natural way on formulas and equations).

A categorical perspective
Nikolaos Galatos and Constantine Tsinakis [18] follow in Blok and Jónsson's footsteps and take their approach to the next level of generality. In particular, they aim at applying categorical and order-theoretic methods to the study of acr's. One major hindrance to this accomplishment is the intrinsic asymmetry of acr's, whose relata are, respectively, a subset of the base set and an element thereof. With an eye to mending this flaw, they go on to define symmetric versions of acr's on a given set A as preorder relations ⊢ ⊆ ℘ (A) × ℘ (A) such that X ⊢ Y iff X ⊢ y for all y ∈ Y ; equivalently, preorder relations containing the supersethood relation such that X ⊢ {Z : X ⊢ Z}. Although these symmetric acr's are shown to be in bijective correspondence with standard acr's, their advantage is that their premiss-sets and conclusion-sets are points in a complete lattice of sets, a circumstance that suggests the following generalisation.
Definition 3. A Galatos-Tsinakis consequence relation (gtcr) on a complete lattice L = L, ∧, ∨ , with induced order ≤, is a preorder ⊢ of L that contains ≥ and is such that for all x ∈ L, x ⊢ {y ∈ L : x ⊢ y}.
Can action-invariance be accommodated in this broader setting? To do so, we must first enrich our monoids of actions with additional structure, in such a way as to turn them into complete residuated lattices [17,23]. Now, let M = M, ∧ M , ∨ M , ·, \, /, 1 be a complete residuated lattice, 1 L = L, ∧ L , ∨ L be a complete lattice and ⋆ : M × L → L be a map. We say that M acts on L, or also that L = L, ∧ L , ∨ L , ⋆ is an M-module, 2 if the monoid reduct of M acts on L and, moreover, there are maps / ⋆ : L × L → M and \ ⋆ : M × L → L such that, for all m ∈ M and x, y ∈ L, From this point onwards, Galatos and Tsinakis continue their investigation in the category M−Mod whose objects are M-modules and whose arrows are residuated maps τ : L → L ′ (called translators) such that, if M acts on L and L ′ via ⋆ 1 and ⋆ 2 respectively, we have that for all x ∈ L and m ∈ M , τ (m ⋆ 1 x) = m ⋆ 2 τ (x). A noteworthy feature of M−Mod is the fact that gtcr's on its objects can be viewed as bona fide objects in the same category. In fact: • The gtcr's on an M-module L correspond bijectively to closure operators on its lattice reduct L via the maps ⊢ () and γ () defined by • If L is an M-module (via ⋆) and ⊢ is a gtcr on its lattice reduct L, then the lattice L γ ⊢ of γ ⊢ -closed elements of L is the lattice reduct of an If ⊢ is a gtcr on L, then L γ ⊢ is nothing but the lattice of ⊢-theories -viz., It turns out that algebraisability can be generalised to the setting of modules over residuated lattices, again thanks to the criterion provided by the Syntactic Isomorphism Theorem of algebraisable logics (see Theorem 2). More precisely, two gtcr's ⊢ 1 and ⊢ 2 , respectively on the M-modules L and L ′ , are said to be equivalent if there is a module isomorphism f : . Moreover, we say that an isomorphism f : is induced by the translators τ : L → L ′ and ρ : L ′ → L if f γ ⊢1 = γ ⊢2 τ and f −1 γ ⊢2 = γ ⊢1 ρ. In this case, the classical definition of algebraisability can be restored, in the sense that for every x, y ∈ L and z ∈ L ′ we have that (x ⊢ 1 y ⇐⇒ τ (x) ⊢ 2 τ (y)) and z ⊣⊢ 2 τ (ρ (z)) .
In this parlance, the Syntactic Isomorphism Theorem states that every equivalence between a logic ⊢ and the equational consequence |= K relative to a generalized quasi-variety K is induced by a pair of translators. It is natural to ask whether this is true for arbitrary equivalences between gtcr's on M-modules. Unfortunately, it turns out that this is false in general, as shown in [19]. Nevertheless, Galatos and Tsinakis find sufficient and necessary conditions for it to be the case. Recall, that an object R in a category C, whose arrows are set-theoretic functions, is onto-projective if for any C-morphisms f : S → T and g : R → T between objects in C with f onto, there is a C-morphism h : R → S such that f • h = g. Here is the main result in the paper by Galatos and Tsinakis: Theorem 4. An M-module L is onto-projective in M−Mod iff for any Mmodule L ′ and gtcr's ⊢ 1 and ⊢ 2 , respectively on L and L ′ , every residuated order embedding f of L γ⊢1 into L ′ γ⊢2 is such that f γ ⊢1 = γ ⊢2 τ for some translator τ : L → L ′ . In particular, if both L and L ′ are onto-projective, then every equivalence between ⊢ 1 and ⊢ 2 is induced by translators.
Generalizations of the above criterion have been obtained in [16] (see also [34]) and [26], while the structure of onto-projective objects in the Blok-Jónsson framework was described in [13]. Note that in [16] the authors have also proved that all epimorphisms in M−Mod are onto, so the specification "onto" in the previous theorem is redundant.
Given a propositional language L, the lattice of sets ℘ (Fm L ) -that corresponds to the plain old module of L-formulas -is indeed onto-projective in ℘ (End (Fm L )) −Mod, and so are the modules of L-equations and L-sequents. Thus, Theorem 4 gives an elegant abstract characterisation of those modules that are just as "well-behaved" as these standard examples in terms of admitting a general version of the Syntactic Isomorphism Theorem.

The substructural challenge
Substructural logics [27,17,23], usually introduced by means of sequent calculi where some or all of the standard structural rules (Weakening, Contraction, Exchange, Cut) are restricted or even deleted, provide an interesting challenge for the Blok-Jónsson approach to consequence, as further developed by Galatos and Tsinakis. By this we do not mean that they lie outside its scope -on the contrary, they can be handled even in traditional AAL. There is, in fact, a canonical way to obtain a tcr out of a given substructural sequent calculus. By way of example, consider the sequent calculus FL e for full Lambek calculus with exchange and the variety F L e of pointed commutative residuated lattices. Define: • X ⊢ FL e ϕ iff the sequent ⇒ ϕ is provable in the calculus obtained by adding to FL e as axioms the sequents in {⇒ ψ : ψ ∈ X} (this is sometimes called [2] the external consequence relation of a sequent calculus).
It is well-known [17, Ch. 2] that for any set of formulas X ∪ {ϕ}, X ⊢ FL e ϕ holds if and only if X ⊢ ′ FLe ϕ. The relation defined by any of these two equivalent conditions is a tcr to all intents and purposes.
This approach, however, seems to fly in the face of the motivation underlying substructural logics. tcr's are relations between sets of formulas and single formulas, whence they are insensitive to the number of occurrences a formula may have in some collection of premisses. In other words, they automatically validate the Contraction and the Anticontraction rules: if X, ϕ, ϕ ⊢ ψ, then X, ϕ ⊢ ψ, and conversely if X, ϕ ⊢ ψ, then X, ϕ, ϕ ⊢ ψ. Yet, some substructural logics (like linear logic, [20]) are commonly employed to formalise a "resourceconscious" notion of inference, according to which sentences are information tokens of a given type and for which the Contraction rule is utterly suspect. Other substructural logics in the relevant family [24,25] aim at capturing a concept of deduction according to which premisses in an argument should be actually used to get the conclusion, something which seems to disqualify Anticontraction (and, even more, Weakening). In other words: AAL can certainly accommodate substructural logics into its framework (in the format of propositional logics or of Gentzen systems), and bestow on them the imposing bulk of general results it has to offer, but only at the cost of tweaking the substructural proof systems in such a way as to produce consequence relations that weaken and contract by fiat. AAL, in sum, does not stay true to the spirit of substructural logics. Now return, for a while, to the sequent calculus FL e . A more plausible candidate for a formalisation of substructural consequence is its so-called internal consequence relation [2], namely, that relation that holds between a finite multiset of formulas Γ and a formula ϕ just in case Γ ⇒ ϕ is a provable sequent of FL e . Investigating relations of this kind, however, means overstepping the Tarskian framework under at least two respects: 1. A consequence relation should be conceived of as a relation between a finite multiset of formulas and a formula; 2. The Monotonicity postulate should be dropped and the Reflexivity postulate should be restricted.
This approach, indeed, has been followed by Arnon Avron [3] and, sporadically, by a few others [24,25,37,27], who laid down the fundamentals of a theory of multiset consequence. However, to help the theory to get started and make it easier to reconstruct some of the basic AAL theorems, it also seems wise to follow a middle-of-the-road perspective that shortens the gap with the Tarskian paradigm, adopting finite multisets as collections of premisses but leaving the Monotonicity and Reflexivity postulates untouched. The resulting relations have a built-in Weakening condition, although they do not necessarily contract. This policy, as a matter of fact, faces an insurmountable problem. David Ripley [33] has shown that it is not possible to obtain a bijective correspondence between these "naive" multiset consequence relations and closure operators on finite multisets of formulas -any such relation that arises from a closure operator has to obey Contraction.
In the paper [10], two of us developed a strategy to avoid this problem. They adopted a multiple-conclusion format, studying relations between finite multisets of formulas of a given propositional language. They also suitably modified the notions of closure operator and closure system on finite multisets of formulas so as to recover the traditional lattice isomorphism results that characterise the standard set-theoretical framework. These correspondences were laid down as the embryo of a theory that aimed at eventually obtaining appropriate analogues of the main results available in AAL for Tarskian consequence.
It is worth asking whether something like these multiset consequence relations, which have no direct counterpart in AAL, can still ensconce in some more flexible apparatus based on (not necessarily complete) lattices. After all, finite multisets over a set still form a lattice under the operations (X ∨ Y)(a) = sup{X(a), Y(a)} and (X ∧ Y)(a) = inf{X(a), Y(a)} (see below), out of which we could define an M-module of sorts that would land us in known territory. However, it is not hard to see that the crucial operation on multisets is not any of these, but rather multiset sum: It is via multiset sum that we aggregate multisets of premisses in substructural logics and formulate sequent rules in substructural sequent calculi. Being a non-idempotent operation, though, it is scarcely pliant to the methods reviewed so far. The gtcr's on complete lattices, therefore, need to be replaced by appropriate relations on dually integral partially ordered Abelian monoids, the prime motivating example being the po-monoid where Fm ♭ L is the set of finite multisets of formulas of the propositional language L, ⊎ is multiset sum, ∅ is the empty multiset and is the sub-multisethood relation (all these notions will be rehearsed in Section 2).

Overview of the paper
This paper is structured as follows. In Section 2 we provide a short primer on multisets. In Section 3, we introduce the concept of a deductive relation (dr) on a dually integral Abelian po-monoid. This is a modification of the notion of gtcr on a complete lattice, so as to encompass deductive relations on multisets and other examples that are not directly covered by Galatos and Tsinakis' theory. Since, as we have seen, gtcr's on a lattice are in bijective correspondence with closure operators on the same lattice, it is to be expectedif we are on the right track -that an analogous result holds with respect to dr's and some sort of "operational companions" of such. The fact that aggregation of premisses and conclusions is abstractly represented by a monoidal operation which, unlike set union, is not necessarily idempotent, implies that it won't do to define these operators in the standard way. Thus, deductive operators (do's) on a dually integral Abelian po-monoid R = R, ≤, +, 0 are introduced as certain maps δ : R → ℘ (R). Similarly, we propose a notion of deductive system (ds) that appropriately generalises closure systems associated with closure operators. The main result of the section is: Theorem A (see Theorem 23) If R is a dually integral Abelian po-monoid, then the posets Re l(R), ⊆ , Op(R), and Sys(R), ⊇ are isomorphic.
In Section 4, the problem of action-invariance is under scrutiny. We define a category A−Mod of modules over dually integral po-semirings (called A-modules) that is closely related to the category of Galatos and Tsinakis' M-modules and includes as new examples the modules M ult L whose underlying po-monoids have the form Fm ♭ L , , ⊎, ∅ for some language L, and whose scalars are finite multisets of L-substitutions. In this wider framework, we obtain analogues of the main theorems proved by Galatos and Tsinakis. Here is an example: Theorem B (see Theorem 43) An A-module R is onto-projective in A−Mod iff, for any other A-module S and action-invariant do's δ and γ on R and S respectively, every injective and order-reflecting morphism Φ : R δ → S γ is induced by some morphism.
In Theorem B, R δ , S γ are A-modules of sets whose universes are, respectively, the union of all δ-images (resp., γ-images) of elements of R (resp. S). We also show that our motivating multiset-theoretical example is just as wellbehaved as the standard examples in Galatos and Tsinakis' theory: Theorem C (see Theorem 48) Modules arising from multisets are onto-projective in the appropriate categories.
In Section 5, we zoom in on multiset deductive relations (mdr's). We introduce two types of matrix semantics for such relations. If ⊢ is an mdr on a language L, an L-hypermatrix is a pair A, F , where A is an L-algebra and F is a -downward closed set of finite multisets over A. We show that the L-hypermatrix models of an mdr ⊢ correspond bijectively to the models of a Gentzen relation uniquely associated to ⊢. This opens the way for importing into our theory all sorts of tools and results from the abstract theory of Gentzen systems [29,31,32], including a workable definition of Leibniz congruence of an L-hypermatrix and a completeness theorem for any substitution-invariant mdr: Theorem D (see Theorem 64) Any substitution-invariant mdr is complete with respect to the class of its reduced L-hypermatrix models.
An alternative type of matrix semantics for mdr's, on the other hand, involves certain structures made up by an algebra A, a dually integral Abelian po-monoid D, ≤, +, 0 , and a po-monoid homomorphism from A ♭ , , ⊎, ∅ to D, ≤, +, 0 . These structures subsume ordinary logical matrices, which arise when D is the 2-element join semilattice. We clarify the relationship between these monoidal matrices and L-hypermatrices. We also show that, in the most favourable cases, the structure of the former can be simplified to a pair constituted by an algebra and a fuzzy subset of its universe. We use these simplified matrices to provide a completeness theorem for a multiset-theoretic companion of infinite-valued Lukasiewicz logic.
Finally, we introduce Hilbert systems suited for multiset consequence and prove that their derivability relations are substitution-invariant mdr's; conversely, every substitution-invariant mdr is shown to arise as the derivability relation of some such Hilbert system. As an example, we provide a Hilbertstyle axiomatisation of the above-mentioned multiset-theoretic companion of infinite-valued Lukasiewicz logic. The main result is: Theorem E (see Theorem 78) Every substitution-invariant mdr coincides with the derivability relation of some axiomatic system AS.

Preliminaries on multisets
In this short section we review some basic notions about multisets only to such an extent as it is needed for the purposes of the present paper. For a more comprehensive account, the reader can consult e.g. [4,35].
By a multiset over a set A we mean a function X from A to the set N of natural numbers. 3 By ℘ M (A) we denote the set of all multisets over A.
The root set of the multiset X is the set If a ∈ |X|, we say that a is an element of X of multiplicity X(a). A multiset X is finite if |X| is finite. By A ♭ we denote the set of all finite multisets over A.
The empty multiset, i.e. the constant function 0, will be denoted by the same symbol ∅ used for the empty set -the context will always be sufficient to resolve ambiguities.
The set of all multisets over a set A inherits the ordering of N in the following way: and, with respect to this ordering, it forms a lattice with joins and meets defined as for all a ∈ A. The operation ∨ is a kind of "union", and, true to form, if we consider the subsets of A as multisets whose elements have multiplicity 1, and X and Y are subsets of A, then X ∨ Y = X ∪ Y. There is another "union-like" operation of sum between multisets, defined as follows: The next proposition shows that the set of finite multisets over a set A can be seen as the universe of a dually integral Abelian po-monoid which we will denote as A ♭ . Proposition 6. For any set A the structure is a dually integral Abelian po-monoid, i.e., a structure where: 3. ∅ is the bottom element of .
We will also have occasion to use the operation X\Y defined by relying on the context to disambiguate between this operation and standard set-theoretic subtraction.
As it is customary to do, we use square brackets for multiset abstraction; so, for example, [a, a, b, c] will denote the multiset X s.t. X(a) = 2, X(b) = X(c) = 1, and X(d) = 0 for any d / ∈ {a, b, c}. Every map f : A → B can be extended to a morphism from A ♭ to B ♭ (for which we retain the same symbol) via for every X = [x 1 , . . . , x n ]. We will use this notation without special mention.

Deductive relations 3.1 Basic definitions and facts
We emphasised in our introduction that we need to consider more general relations than Galatos and Tsinakis' gtcr's if we want to properly account for multiset consequence relations introduced in Definition 5. By Proposition 6, the set of finite multisets of formulas of a given language can be equipped with the structure of a dually integral Abelian po-monoid. This leads us to the next definition.

Definition 7.
A deductive relation (dr) on a dually integral Abelian po-monoid R = R, ≤, +, 0 is a relation ⊢ on R such that for every a, b, c ∈ R: (Generalised Reflexivity) Observe that ⊢ is a compatible preordering of R and 0 is a ⊢-maximum. Also observe that, using properties of compatible preorderings on Abelian monoids and the dual integrality of R, we have: Some examples of dr's follow hereafter. Our prime motivating example, the multiset deductive relations, will be thoroughly studied in Section 5, where appropriate particular examples will be given. It is easy to observe that: Example 9. Let L be a propositional language. Multiset deductive relations on L are exactly the dr's on Fm ♭ L . Of course, standard acr's (hence, in particular, tcr's) give rise to instances of deductive relations: Example 10. Let ⊢ be an acr on the set A (see Definition 1) and let In view of the previous example, the reader will be curious to figure out whether dr's also generalise gtcr's (see Definition 3). The answer, here, is less straightforward.
Proposition 11. Let L = L, ∧, ∨ be a complete lattice with induced order ≤ and bottom element 0. Then the structure is a dually integral Abelian po-monoid and any (finitary) gtcr on L is a (finitary) dr on L ′ .
Proof. The only non-trivial part is Compatibility. Assume that a ⊢ b. Thus, a ∨ c ⊢ b and a ∨ c ⊢ c and so {x : a ∨ c ⊢ x} ⊢ b ∨ c. By the defining condition on gtcr's, it follows that a ∨ c ⊢ b ∨ c. The finitarity part is obvious.
The converse direction does not hold in general. The next proposition provides a class of explicit counterexamples, indeed, a very wide one, because any substitution-invariant tcr ⊢ with a theorem (i.e., an element a such ∅ ⊢ a) containing a variable has infinitely many theorems.
Proposition 12. Let ⊢ be a finitary acr with infinitely many theorems 5 and R ℘(A) and let ⊢ ′ be defined as in Example 10. Then the relation defined by: Proof. For our first claim, the only nontrivial condition to check is Transitivity. Assume that X Y and Y Z, and let Y ′ and Z ′ be finite sets with the required properties. We claim that the finite setZ = Z ′ ∪ (Y ′ ∩ Z) witnesses X Z. In fact: • ClearlyZ is a finite subset of Z.
• The final condition is obtained by the following chain: To conclude the proof, it is easy to observe that for each theorem a we have ∅ a, yet clearly ∅ ⊢ {a : ∅ a}.
The above result is not that surprising, as our definition of dr only employs finitary operations, as opposed to the use of infinite suprema in gtcr's. Our approach has the advantage that our background structure could be much smaller, as the following proposition shows.
Proposition 13. Let L = L, ∧, ∨ be a complete algebraic lattice with induced order ≤ and bottom element 0. Then the structure where K(L) is the set of compact elements of L, is a dually integral Abelian po-monoid. Moreover, there is bijective correspondence between finitary gtcr's on L and dr's on K(L). 6 Proof. For a start, note that finitary gtcr's on complete algebraic lattices are fully determined by their subrelations between compact elements. In fact, for As in Example 11, it is possible to show that the restriction of any gtcr on L is a dr on K(L), and the previous observation entails that if two gtcr's differ they also differ on compact elements.
Conversely, assume that ⊢ is a dr and define: The only condition in need of a proof is that For the nontrivial inclusion, assume that c ∈ K(L) and c ≤ p. Then there are c 1 , . . . , c n such that c ≤ c 1 ∨ . . . ∨ c n and x ⊢ ′ c j for all j ≤ n. This means that for all j ≤ n there is x j ≤ x such that x j ⊢ c j . Using properties of dr's we obtain This mapping is clearly one-one and an inverse to the previous one.
The next example identifies a deductive relation on fuzzy sets. It is introduced to underscore the generality of our framework, but it will not be further discussed in the remainder of this paper.
Among the basic notions of algebraic logic that need to be redefined in our new framework, one certainly finds the concepts of theory and theorem. Here, we must stray away to a certain extent from the received orthodoxy. In view of Example 10, given a dr ⊢ on R = R, ≤, +, 0 , one would expect a ⊢-theory to be an element of R with certain properties. In AAL, in fact, a theory is a deductively closed set of formulas. In particular, the theory generated by a set of formulas X is the smallest deductively closed set of formulas that includes X -or else, the largest Y such that X ⊢ Y -and has the property that its subsets are exactly the consequences of X. However, in the case of mdr's (Definition 5), this would not work. Such a "largest consequence" need not always exist, because it could happen, for instance, that Γ ⊢ ∆ and Γ ⊢ Π but Γ ⊢ ∆ ∨ Π. Nevertheless, it makes sense to collect all the consequences of a given multiset Γ of formulas into a set and view the set itself as the deductive closure of Γ. Abstracting away from this particular example, we are led to the following definition (recall that every dr is a preorder on R).

Definition 15.
Let ⊢ be a dr on R. A ⊢-theory (or simply a theory, when ⊢ is understood) is a ⊢-upset T of R. By Th(⊢) we denote the family of all ⊢-theories.
Observe that the ⊢-theory generated by a ∈ R is just the principal ⊢-upset generated by a. We denote it by Th ⊢ (a), and we denote by Th p (⊢) the set of all principal members of Th(⊢), i.e. theories that are generated by a single element. The subscripts in Th ⊢ will be dropped when the preordering is clear from the context.
Let us note the each ⊢-theory is a union of principal theories, a quite unusual feature from the point of view of the general theory of closure systems. Actually we can prove even more: Proof. Clearly if x ∈ X then Th ⊢ (x) ⊆ Th ⊢ (X) and so one inclusion follows.
To prove the converse one it suffices to show that T = {Th ⊢ (x) : x ∈ X} is a ⊢-theory. Assume that a ∈ T and a ⊢ b. Thus we know that a ∈ Th ⊢ (x) for some x ∈ X and so Transitivity completes the proof.
Observe that 0 is always a theorem 7 and the theorems are exactly the ⊢maximal elements of R, since for any a ∈ R we have a ⊢ 0. Note that ≥, which can be seen as the least dr on R, has 0 as the only theorem.
The reader will recall that one of the main advantages of the notion of gtcr is the fact that the collection of theories of a given gtcr ⊢ over a complete lattice is itself a complete lattice, which is furthermore determined by ⊢. We prove an analogous results for dr's and principal theories. Then is a dually integral po-monoid and the mapping Th ⊢ : R → Th p (⊢) is a surjective morphism.
Proof. The relation ⊆ is clearly a partial order on Th p (⊢) with Th(0) as a bottom element. Moreover, Th is order preserving: in fact, by Generalised Reflexivity a ∈ Th(a) and so, by Transitivity, We now sketch the proof of the fact that the operation + ⊢ is well-defined. To this end, consider a, b, c, d ∈ R such that Th(a) = Th(b) and Th(c) = Th(d). In particular, b ⊢ a and d ⊢ c and so by Compatibility and Transitivity d+b ⊢ a+c, whence Th(a + c) ⊆ Th(b + d). The other inclusion is proved analogously. The fact that Th p (⊢), + ⊢ , Th(0) is an Abelian monoid is obvious, so we only need to check that + ⊢ is compatible with the order. Let a, b, c ∈ R be such that Th(a) ⊆ Th(b). Thus b ⊢ a and so b + c ⊢ a + c. As a consequence, The fact that Th is a surjective morphism is again obvious.

Deductive operators and systems
In AAL, propositional logics can be introduced in three different but equivalent ways: via consequence relations, via closure operators, and via closure systems. The same is true of the approach we have taken. While deductive relations are abstract counterparts of tcr's, our next goal is to define suitable abstract notions of deductive operator and deductive system, in such a way as to generalise the lattice isomorphisms between the lattices of consequence relations, of closure operators, and of closure systems that are available in the traditional theory of AAL. Analogues of the classical concepts of closure operator and closure system can be defined as follows.
Definition 20. A deductive operator (do) on a dually integral Abelian pomonoid R = R, ≤, +, 0 is a map δ : R → ℘(R) such that for every a, b, c ∈ R: • a ∈ δ(a). (Enlargement) Observe that, in full analogy with Definition 15, a do is a map from elements of R to subsets of R.
Next we define the notion of a deductive system; recall that closure systems are systems of theories of some acr, but as we have seen in the previous subsection the principal theories are the crucial ones in our framework (as they can be seen as universes of dually integral Abelian po-monoids). This leads to the following definition: The subscript, or superscript, C will be omitted whenever it is not needed to clarify potential confusions.
Proposition 22. Let C be a ds on a dually integral Abelian po-monoid R. Then the mapping δ C is a do on R.
Proof. Enlargement is obvious. For Idempotency, assume that a ∈ δ(b), c ∈ δ(a) and we have X ∈ C such that b ∈ X. Then a ∈ X (due to the first assumption) and so c ∈ X (due to the second assumption), i.e., c ∈ δ(b). If a ≤ b, then (as each X is ≤-downset) a ∈ δ(b) and so by Idempotency δ(a) ⊆ δ(b), which takes care of Order Preservation. Finally, we prove Compatibility: using the conditions we already established, if a ∈ δ(b), then δ(a) ⊆ δ(b) and so δ(a + c) Given a dually integral Abelian po-monoid R = R, ≤, +, 0 , we respectively denote by Re l(R), Op(R) and Sys(R) the sets of deductive relations, deductive operators and deductive systems on R. We next define partial orders on these sets. Re l(R) will be viewed as partially ordered by set inclusion, and Sys(R) by supersethood. We define an order on Op(R) as follows: given δ, γ ∈ Op(R), we set δ γ iff δ(a) ⊆ γ(a) for every a ∈ R.
It is easy to show that they are well-defined and monotone. We now prove they are mutually inverse. Consider ⊢ ∈ Rel(R) and observe that x ⊢ y iff y ∈ δ ⊢ (x) iff x ⊢ δ ⊢ y. On the other hand, for any δ ∈ Op(R): Next, we handle the slightly more complex case of dr's and ds's. We define maps C () : Rel(R) → Sys(R) and ⊢ () : Sys(R) → Rel(R) as follows: Using Theorem 19, we conclude that C ⊢ is indeed a ds, while Proposition 22 guarantees that δ C is a do. Monotonicity of both functions is obvious and so is the fact that they are mutually inverse. For the sake of completeness, we observe that C δ = {δ(a) : a ∈ R} maps Op(R) to Sys(R), and that such a mapping is inverted by the mapping that sends any ds C to the already defined deductive operator δ C .
Proof. By Theorem 23, it will suffice to prove our claim for any one of these posets, say Op(R), . It is obvious that δ 1 , defined by is a do and that it is the top element w.r.t. . In order to see that do's on R form a complete lattice, it is enough to see that for every family of do's {δ i : i ∈ I}, the map i∈I δ i defined by

Blok-Jónsson companions of deductive relations
Deductive relations, deductive operators and deductive systems respectively give rise to special kinds of acr's (Definition 1), closure operators and closure systems. In the present subsection, we point out the fact that there is a significant transfer of information from the original relations, operators and systems to these "Blok-Jónsson companions", which we now proceed to define. Given a dr ⊢ on R = R, ≤, +, 0 , its Blok-Jónsson companion is the relation ⊢ BJ ⊆ ℘ (R) × R defined as follows for every X ⊆ R and every a ∈ R: Lemma 25. If ⊢ is a dr on R = R, ≤, +, 0 , then ⊢ BJ is an acr on R.
Proof. For Reflexivity, suppose x ∈ X; we want to show that X ⊢ BJ x, i.e. that there is y ∈ X s.t. y ⊢ x. However, by the reflexivity of ⊢, x itself fits the bill.
Monotonicity is straightforward from the definition of ⊢ BJ . For Cut, we want to show that X ⊢ BJ y and Z ⊢ BJ x for all x ∈ X imply that Z ⊢ BJ y. In fact, suppose there is x ∈ X s.t. x ⊢ y. This implies that there is z ∈ Z s.t. z ⊢ x, whence by transitivity of ⊢, z ⊢ y, which in turns entails that Z ⊢ BJ y.
Along the same lines, deductive operators and deductive systems on R can be lifted to closure operators and closure systems, respectively, on the base set R.

Lemma 27.
Given a ds C on R = R, ≤, +, 0 , the family To conclude the proof just observe that In full analogy with the above, we call δ BJ and C BJ the Blok-Jónsson companions of δ and C, respectively. Observe that: Lemma 28. Let ⊢ be a dr on R = R, ≤, +, 0 . The ⊢-theories are the theories (in the sense of Blok-Jónsson) of ⊢ BJ . Namely, for T ⊆ R, t.f.a.e.: 1. T is a ⊢-upset of R.
Proof. (1) implies (2). Suppose T is a ⊢-upset of R and there is y ∈ T s.t. y ⊢ x. Then x ∈ T .
(2) implies (1). Suppose that for any x, T ⊢ BJ x implies x ∈ T , that y ∈ T , and that y ⊢ z. So T ⊢ BJ z, whence z ∈ T .
Let us continue to use the notations ⊢ δ , ⊢ C , C ⊢ , C δ , δ ⊢ , and δ C for the correspondences between dr's, do's and ds's on R spelt out in Theorem 23. With an innocent notational abuse, we employ the same symbols for the standard correspondences between the sets Acr(R) of acr's, closure operators Clop(R) and closure systems Clos(R), all on R. We now prove that the relation of "taking the Blok-Jónsson companion" commutes with these functions.
Theorem 29. The following diagrams as well as the ones we obtain by reversing the above correspondences, are all commutative.
Proof. The correspondences are well-defined by Theorem 23 and Lemmas 25, 26, and 27. We now take care of some of the commutations. We show that (⊢ δ ) BJ = ⊢ δ BJ ; the other commutations are established similarly. In fact, X, a ∈ (⊢ δ ) This theorem implies, in particular, the following corollary: Corollary 30. Let R = R, ≤, +, 0 be a dually integral Abelian po-monoid. The complete lattices of Blok-Jónsson companions of dr's, do's, and ds's on R are isomorphic.

Action-invariance
One of the remarkable achievements of Blok and Jónsson's treatment of logical consequence is its purely abstract account of substitution-invariance. Resorting to appropriate monoidal actions, Blok and Jónsson effectively sidestep the problem brought about by their use of sets with no structure whatsoever to be preserved. As we have seen, Galatos and Tsinakis turn this insight into the starting point for their categorical foundation of the whole subject. It would be highly desirable, then, to lay down a comparable treatment of action-invariance in our framework. This will be done by equipping our Abelian po-monoids with appropriate monoidal actions.
Our chief example of dually integral po-semiring will be the semiring of finite multisets of substitutions on formulas of a propositional language L. The role it will play here is analogous to the role played in Galatos and Tsinakis' theory by the complete residuated lattice of sets of L-substitutions.
Example 32. Let L be a propositional language, and let End(Fm L ) be the set of substitutions of Fm L . The structure is a dually integral po-semiring.
With this notion in our quiver, in order to get going we only need to endow our dually integral Abelian po-monoids from the previous section with a suitable operation of multiplication by a scalar.

Definition 33. Let
is a dually integral Abelian po-monoid and * R : A × R → R is an action of A, · A , 1 A on R that is order-preserving in both coordinates and distributes over + R . In symbols: we set, resorting to our usual notational conventions, X * Γ = σ 1 (Γ) ⊎ · · · ⊎ σ n (Γ).
Then M ult L is a Σ L -module.
Modules over a dually integral po-semiring can be naturally equipped with arrows as follows: Definition 35. Let A be a dually integral po-semiring, and R and S be a pair of A-modules. A morphism τ : R → S is a po-monoid homomorphism (i.e., an order-preserving monoid homomorphism) such that τ (σ * R a) = σ * S τ (a) for every σ ∈ A and a ∈ R.
Given a dually integral po-semiring A, the collection of A-modules with morphisms between them forms a category in which composition and identity arrows are, respectively, standard composition of functions and identity functions. We denote this category by A−Mod. Isomorphisms in the category A−Mod are precisely bijective morphisms.
From now on we will assume that A is a fixed, but otherwise arbitrary, dually integral po-semiring. We are now ready to give an abstract formulation of action-invariant dr's. Against the backdrop of Theorem 23, these deductive relations can be presented equivalently as deductive operators or as deductive systems. As a matter of fact, it turns out that working with do's is more convenient, although similar definitions and results can be obtained by putting the other two concepts to the forefront.
Definition 37. An action-invariant do on an A-module R is a do δ on its po-monoid reduct R, ≤, +, 0 such that for every σ ∈ A and a, b ∈ R: To exemplify this concept, we point out that substitution-invariant mdr's give rise to deductive operators that are action-invariant according to the definition just given.
Proposition 38. Let L be a propositional language. Then an mdr ⊢ on L is substitution-invariant iff δ ⊢ is an action-invariant do on the Σ L -module M ult L . Similarly, δ is an action-invariant do on the Σ L -module M ult L iff ⊢ δ is a substitution-invariant mdr on L.
The second claim follows from the first one, together with the fact that δ ⊢ δ = δ (Theorem 23).
Lemma 39. Let δ be an action-invariant do on the A-module R. Then R δ is a well-defined A-module and the map δ : R → R δ is a morphism.
Proof. Using Theorems 23 and 19, we know that is a well-defined dually integral po-monoid. Now we show that the action * δ is well-defined too. Consider σ ∈ A and a, b ∈ R such that δ(a) = δ(b). In particular, we have that a ∈ δ(b). By the action-invariance of δ, we obtain that σ * a ∈ δ(σ * b). Thus we conclude that δ(σ * a) ⊆ δ(σ * b). The other inclusion is proved analogously.
Next, we turn to prove that R δ is an A-module. It only remains to establish the conditions regarding the action * δ . It is clear that * δ is order-preserving on the first coordinate. We prove that the same holds for the second one. Consider σ ∈ A and a, b ∈ R such that δ(a) ≤ δ δ(b). From the action-invariance of δ it follows that σ * a ∈ δ(σ * b) and, therefore, that δ(σ * a) ≤ δ δ(σ * b). We conclude that The fact that * δ is a monoidal action and the distributivity conditions are easy exercises. Finaly, we prove that the map δ : R → R δ is a morphism. Due to Theorem 19, it remains to show that δ respects the monoidal action, which follows directly from the definition of * δ .
We conclude this subsection be defining two maps which will play an important role in the next subsection.
Lemma 40. Let f : R → S be a morphism between A-modules.
1. The map f * : R → ℘(R) defined as: is an action-invariant do on R.

The mapf
is a well-defined isomorphism.
Proof. 1. The only condition in Definition 20 that stands in need of a check is Compatibility. Let a, b, c ∈ R and suppose that a ∈ f * (b). This means that f (a) ≤ f (b). In particular, we have that Hence we conclude that a + c ∈ f * (b + c). This shows that f * is a do. It remains to be shown that it is action-invariant. Consider σ ∈ A and suppose that a ∈ f * (b). Then Thus σ * R a ∈ f * (σ * R b), whence our conclusion follows.
2. Observe that the mapf is well-defined, since ≤ S is antisymmetric. It is clear thatf is a bijection. Since isomorphisms in A−Mod are bijective morphisms, it suffices to prove thatf is a morphism. But this is an exercise, using the definition of R f and the fact that f is a morphism.

Action-invariant representations
The main result in [18], reproduced above as Theorem 4, is an elegant and purely categorical characterisation of the modules over a complete residuated lattice for which an analogue of the Syntactic Isomorphism Theorem (Theorem 2) for algebraisable logics holds. The aim of this subsection is to obtain a similar result in the setting of modules over a dually integral po-semiring.
Definition 41. Let δ and γ be action-invariant do's on the A-modules R and S, respectively.
1. An action-invariant representation of δ into γ is an injective morphism Φ : R δ → S γ that reflects the order.

2.
A representation Φ of δ into γ is induced if there is a morphism τ : R → S that makes the following diagram commute: δ and γ are equivalent if the A-modules R δ and S γ are isomorphic.
Definition 42. An A-module R has the representation property (REP) if for any other A-module S and action-invariant do's δ and γ on R and S respectively, every action-invariant representation of δ into γ is induced.
We are now ready to provide a characterisation of A-modules with the REP in the spirit of Theorem 4.
Theorem 43. An A-module has the REP iff it is onto-projective in A−Mod.
Proof. The backbone of our argument is essentially the same as in [18,Lemma 8.1]. It is clear that every projective A-module has the REP. Now, let R be an Amodule with the REP, and consider two morphisms f : S → T and g : R → T with f onto. By Lemma 40, the derived maps f * and g * are action-invariant do's on R and S, respectively. Observe that g(R) is the universe of a submodule g(R) of T . By Lemma 40 the following maps are isomorphisms: f : S f * → T and g : R g * → g(R).
Let i : g(R) → T be the morphism given by the inclusion relation. Clearly the compositionf Thus we can apply the fact that R has the REP, obtaining a morphism h : R → S such that Hence for every a ∈ R, we have that Hence we conclude that f • h = g. Therefore R is onto-projective.
In order to show that our abstract framework is well-behaved, we are committed to proving that every equivalence between two substitution-invariant mdr's is induced by a pair of endomoprhisms on the Σ L -module M ult L (note that this claim can bee seen as a variant of Isomorphism Theorem in the setting of mdr's). In other words, we want to show that M ult L has the REP (that is, it is onto-projective) in the category of Σ L -modules. Instead of proving this directly, we will take a brief detour and prove some more general results. First, we make a note of the following definition.
Observe that every dually integral po-semiring A = A, ≤, +, ·, 0, 1 can be seen as a degenerate instance of A-module if we drop · and 1 from the signature and set * = ·. Keeping this in mind, we obtain the following: Lemma 45. Any dually integral po-semiring A, viewed as an A-module, is cyclic and onto-projective.
Proof. Clearly A is cyclic, since A = {σ · 1 : σ ∈ A}. Let f : R → S and g : A → S be two morphisms, where f is onto. Then fix any a ∈ R such that f (a) = g(1). We define a map h : A → R via h (σ) = σ * R a. It is easy to see that h : A → R is a morphism. Moreover, given σ ∈ A, we have that Hence we conclude that A is onto-projective. Cyclic modules can be described in an arrow-theoretic way as follows: Lemma 46. An A-module R is cyclic if and only if there is an onto morphism f : A → R.
Proof. If there is an onto morphism f : A → R and x ∈ R, then for some σ ∈ A we have that x = f (σ) = σ * f (1). To prove the converse, it is enough to check We are now ready to prove the following characterisation of cyclic and ontoprojective objects in A−Mod.
Theorem 47. Let R be an A-module. The following conditions are equivalent: 1. R is cyclic and onto-projective.

2.
There is a retraction f : A → R.
Proof. (1)⇒(2): From Lemma 46 we know that there is a surjective morphism f : A → R. Applying the projectivity of R to the diagram given by f and the identity map id R , we conclude that f is a retraction.
(2)⇒(1): From Lemma 46 we know that R is cyclic. Moreover, R is a retract of an onto-projective object by Lemma 45. Thus we conclude that R is onto-projective too.
(2)⇒(3): By assumption, there is an injective morphism g : R → A such that 1 R = f • g. Then we define v = f (1) and µ = g(v). Since f is onto, we have that A * {v} = R. Moreover: (3)⇒(2): Since A * {v} = R, we know that the map f : A → R defined as f (σ) = σ * v is an onto morphism. Then let g : R → A be defined via g (σ * v) = σ · µ. Using the assumption, it is not difficult to see that g is well-defined and order-preserving. Also, it can be routinely established that g preserves the action and is a monoid homomorphism. Thus, g is a morphism. In order to prove that f • g = 1 R we consider a generic element σ * v ∈ R and show that:

Multiset deductive relations
Recall that what prompted us to extend Blok and Jónsson's theory was the motivating example of multiset deductive relations (mdr's), defined in Definition 5. It turns out that our general theory has interesting offshoots once we focus on this special case -and the whole of the present section will be devoted to buttressing this claim.
For a start, we list some prototypical instances of mdr's.
Example 49. Recall that an algebra A = A, ∧, ∨, ·, →, 1 of language L 0 = 2, 2, 2, 2, 0 is a commutative and integral residuated lattice (see e.g. [23]) if A, ∧, ∨ is a lattice, A, ·, 1 is a commutative monoid, 1 is the top element w.r.t. the induced order ≤ of A, ∧, ∨ , and the following residuation law holds for every a, b, c ∈ A: Given a class K of commutative and integral residuated lattices, let the relation ⊢ K be defined as follows for all It can be checked that ⊢ K is indeed a substitution-invariant mdr in the sense of Definition 5.
Example 49 identifies, for every substructural logic whose equivalent algebraic semantics is a quasi-variety of commutative and integral residuated lattices, a "multiset-theoretic" companion of such that best suits the resource interpretation at which we hinted in our introduction. One particular such logic will play some role in what follows. The multiset companion ⊢ MV of infinitevalued Lukasiewicz logic ⊢ L is obtained when the class K is the variety MV of MV-algebras [9], formulated in the language L 0 .
Also, observe that Example 49 encompasses the so-called internal consequence relations of algebraisable substructural sequent calculi with exchange and weakening [2,3]. In fact, let S be such a calculus and Q its equivalent algebraic semantics. Upon defining, for finite multisets of L 0 -formulas Γ and ∆ = [ψ 1 , . . . , ψ m ], then it follows from well-known results about substructural logics that ⊢ S = ⊢ Q . If the above examples look a bit contrived, this is due, in part, to the fact that the multiple-conclusion format is unfamiliar to many. As a consequence, it would seem expedient to extract from these examples appropriate singleconclusion relations that can be more easily compared, say, to the usual, external, consequence relations of substructural sequent calculi. It turns out that single-conclusion relations can be recovered as fragments of mdr's [10]: Definition 50. Let L be a propositional language. A single-conclusion mdr on L is a relation ⊢ u ⊆ Fm ♭ L × Fm L such that, for some mdr ⊢, It should be observed, though, that we are not claiming that single-conclusion mdr's be themselves instances of mdr's, for they need not be closed w.r.t. all the conditions that define them (see [10] for further discussion). Clearly, for each single-conclusion mdr ⊢ u there exists the least mdr ⊢ that has ⊢ u as fragment: namely, the intersection of all such mdr's. In Subsection 5.4 we present an example of two mdr's with the same single-conclusion fragment.
Multiset deductive relations can be taken to subsume tcr's, as the next example shows.
Example 51. Every finitary substitution-invariant tcr can be encoded into a finitary substitution-invariant mdr. Indeed, consider such tcr on language L. Then we define a substitution-invariant mdr ⊢ on L by setting, for all It is a purely computational matter to check that ⊢ is indeed a substitutioninvariant mdr. Moreover, it is clear that ⊢ encodes in the sense that, whenever ϕ j = ϕ k for all j, k ≤ n, ϕ 1 , . . . , ϕ n ψ ⇐⇒ [ϕ 1 , . . . , ϕ n ] ⊢ [ψ] .

Hypermatrices and the first completeness theorem
In this subsection we describe a matrix-based semantics for arbitrary substitutioninvariant mdr's. To this end, we work in a fixed (but otherwise arbitrary) language L. Logical matrices are part and parcel of every algebraic logician's toolbox [12,Ch. 4]. As a consequence, when we are dealing with mdr's over a language L, it seems desirable to be in a position to help ourselves to concepts that inherit at least some of the effectiveness and power of matrix semantics in AAL. Whatever notion of matrix we are bound to adopt, it appears natural that its attendant notion of "Lindenbaum-Tarski matrix" be in keeping with Definition 15: we expect such matrices to have the form Fm L , F where F is a certain set of finite multisets of L-formulas. Therefore, it is all too plausible to focus on "matrices" constituted by an algebra and a certain family of finite submultisets of its universe. The next definitions spell out in detail this basic insight.
Definition 52. An L-hypermatrix is a pair A, F , where A is an L-algebra and F a -downset in A ♭ .
Definition 53. For a class H of L-hypermatrices we define a relation |= H on Fm ♭ L as Γ |= H ∆, if for every A = A, F ∈ H, each context C ∈ A ♭ and each homomorphism f : Fm L → A: For Compatibility, assume that Γ |= A ∆ and consider a homomorphism e : Fm L → A and context C ∈ A ♭ . If C ⊎ e(Γ) ⊎ e(Π) = C ⊎ e(Γ ⊎ Π) ∈ F , then by our hypothesis C ⊎ e(∆) ⊎ e(Π) ∈ F , and thus Γ ⊎ Π |= A ∆⊎Π.
For Generalized Reflexivity, assume that Γ ∆ and consider a homomorphism e : Fm L → A and context C ∈ A ♭ . Clearly, e (Γ) e (∆), and by com- Note that the fact that F a -downset in A ♭ , and the reference to arbitrary contexts C, play a crucial role in the previous proof. Lifting both restrictions at once leads to the following definition of a relation |= ′ A on Fm ♭ L for an arbitrary pair A = A, F , where A is an L-algebra and F ⊆ A ♭ : Lemma 55. Consider a pair A = A, F , where A is an L-algebra and F ⊆ A ♭ . Then |= A ⊆ |= ′ A . Assume further that for some mdr ⊢ we have ⊢ ⊆ |= ′ A . Then A is an L-hypermatrix and ⊢ ⊆ |= A .
To complete the proof we need to show that ⊢ ⊆ |= A . Assume that Γ ⊢ ∆, C = [x 1 , . . . , x n ] ∈ A ♭ and f : Fm L → A are such that C⊎f (Γ) ∈ F and we need to prove that C ⊎ f (∆) ∈ F . Let Π be a multiset of mutually different atoms [p 1 , . . . , p n ] not occurring in Γ ⊎ ∆; we know that Γ ⊎ Π ⊢ ∆ ⊎ Π. Next consider the homomorphism e ′ defined as e ′ (p i ) = x i and e ′ (p) = e(p) for other atoms and note that e ′ (Γ ⊎ Π) = X ⊎ e(Γ) ∈ F and so X ⊎ e(Γ) = e ′ (∆ ⊎ Π) ∈ F . Next, we provide an example showing that |= A and |= ′ A are in general different relations.
Example 56. Consider a two-element set A = {0, 1}. Then let F ⊆ A ♭ be defined as follows: Now, equip A with the structure of an algebra A = A, 0, 1 , whose only operations are constant symbols 0 and 1 for 0 and 1, respectively. Clearly, F is a -downset and it is easy to see that for A = A, F we have we denote the set of all models of ⊢ and by F i ⊢ (A) the set of all ⊢-filters on A.
It is straightforward to show that F i ⊢ (A) is a closure system. Given a closure system C on a set X, let us denote by C p the set of its principal members: Proposition 59. Let ⊢ be a substitution-invariant mdr on L.
1. For every L-algebra A, the collection (F i ⊢ (A)) p is a ds on A ♭ and Proof. Consider an arbitrary L-algebra B. Recall that F i ⊢ (B) is a closure system. Then let Fg B ⊢ : ℘(B ♭ ) → ℘(B ♭ ) be its corresponding closure operator. It is easy to see that for every X ⊆ B ♭ , For the other statement, consider an L-algebra A. We begin by proving that (F i ⊢ (A)) p is a ds on A ♭ , ≤, ⊎, ∅ . To this end, we claim that for every X, Y, C ∈ A ♭ . To prove this claim, fix X, Y, C = [c 1 , . . . , c k ] ∈ A ♭ and consider decomposi- defined at the beginning of this proof. We show, by induction on n ∈ ω, that The case where n = 0 is direct. Then we consider the case n = s + 1. Suppose that X ∈ F s+1 . Then there are Γ, ∆ and a homomorphism f : Consider the multiset Π = [x 1 , . . . , x k ] consisting of fresh pair-wise different variables. By compatibility of ⊢, we have that By inductive hypothesis we know that Let f ′ : Fm L → A be any homomorphism which coincides with f on the variables appearing in the formulas Γ and ∆, and such that f ′ (x i ) = c i . By (5) we have that Together with (4), this implies that This concludes the proof of (3) and, therefore, establishes (2). Now we turn back to the main argument. First observe that Hence we conclude that (F i ⊢ (A)) p is a ds on A ♭ as desired.
Then we turn to prove that F i ⊢ (A) = ((F i ⊢ (A)) p ) BJ . The inclusion from left to right is clear. To prove the other one, consider a family {F i : i ∈ I} ⊆ (F i ⊢ (A)) p . Then suppose that Γ ⊢ ∆, and consider a homomorphism f : The notions introduced so far are enough to obtain a first completeness theorem for any substitution-invariant mdr.
Theorem 60 (1st completeness theorem). Let ⊢ be a substitution-invariant mdr on L. Then . Proof. From left to right, our claim is obvious. For the reverse direction, assume that Γ ⊢ ∆ and define T = Th ⊢ (Γ). By Proposition 59, Fm L , T ∈ Mod(⊢) and then the identity mapping is the homomorphism we need to show that Γ |= Mod(⊢) ∆.

A bridge to Gentzen systems and the second completeness theorem
We will now establish a connection with the algebraic theory of Gentzen systems, i.e. substitution-invariant acr's on sequents, a well-trodden research stream in AAL [29,30,31,32,28,36], that will serve as a touchstone for our approach based on hypermatrices. Let ⊢ be a substitution-invariant mdr on L. We will associate with it a consequence relation ⊢ g between sequents. To this end, consider the set Seq L of L-sequents of the form where ϕ 1 , . . . , ϕ n is a finite sequence of formulas. We consider the relation ⊢ g ⊆ ℘(Seq L ) × Seq L defined as follows: Clearly, ⊢ g is a substitution-invariant acr on Seq L : for every substitution σ, if X ⊢ g ∅ ⊲ ϕ 1 , . . . , ϕ n , then As we remarked above, substitution-invariant acr's on sequents are the object of study of numerous papers that have appeared under the heading of algebraisation of Gentzen systems. Within this theory, a model of a Gentzen system on Seq L is a pair A, F where A is an L-algebra and F is a set of finite sequences of elements of A such that for every set X ∪ {∅ ⊲ ϕ 1 , . . . , ϕ n } ⊆ Seq L , if X ∅ ⊲ ϕ 1 , . . . , ϕ n , then for every homomorphism f : We denote by Mod( ) the class of all models of . A quick comparison between Definition 58 (see also the comments before the definition) and (6) suggests that the models of ⊢ and ⊢ g must be interdefinable. To make this idea precise, we define two maps as follows: where (·) s stands for sequents and (·) m stands for multisets. Given A, F ∈ Mod(⊢ g ) and B, G ∈ Mod(⊢), we set: . . , a n ] : n ≥ 0, a 1 , . . . , a n ∈ F } The proof of the following result is straightforward (note that we need to use Lemma 55): Lemma 61. The transformations (·) s : Mod(⊢) ←→ Mod(⊢ g ) : (·) m are welldefined and mutually inverse bijections.
As a consequence, we can apply the algebraic constructions developed for Gentzen systems in the above-mentioned literature, to the study of substitutioninvariant mdr's. We devote the remaining part of this subsection to give a flavour of the resulting theory.
Let A, F be a pair consisting of an L-algebra A and a set F of finite sequences of elements of A. A congruence θ of A is compatible with F if for every a 1 , b 1 , . . . , a n , b n ∈ A, if a 1 , . . . , a n ∈ F and a 1 , b 1 , . . . , a n , b n ∈ θ, then b 1 , . . . , b n ∈ F.
It turns out that there exists the largest congruence of A compatible with F . This congruence is called the Leibniz congruence of F over A, and is denoted by Ω A F . The reduced models of are the following class: A general result [12,Proposition 5.111] shows that the Gentzen system is complete with respect to the semantics Mod * ( ): the pairs in Mod * ( ) are models of and, moreover, if X ∅ ⊲ ϕ 1 , . . . , ϕ n , then there is A, F ∈ Mod * ( ) and a homomorphism f : Fm L → A such that f (γ 1 ), . . . , f (γ m ) ∈ F for every ∅ ⊲ γ 1 , . . . , γ m ∈ X, and f (ϕ 1 ), . . . , f (ϕ n ) / ∈ F.
Lemma 62. There exists the largest congruence of A compatible with F .
Proof. We will denote by G the set of finite sequences of elements of A such that A, G = A, F s . We know that Ω A G is the largest congruence of A compatible with G. In order to conclude the proof, it will be enough to show that Ω A G is also the largest congruence of A compatible with F . However, it is easily proved that a congruence of A is compatible with F if and only if it is compatible with G, whence our claim follows.
Given the above result, we denote the largest congruence of A compatible with F by Ω A F , and call it the the Leibniz congruence of F over A. We define the reduced models of an mdr ⊢ as follows: Corollary 63. The transformations (·) s : Mod * (⊢) ←→ Mod * (⊢ g ) : (·) m are well-defined and mutually inverse bijections.
Proof. Pick a model A, F ∈ Mod * (⊢). Let G be the set of finite sequences of elements of A such that A, F s = A, G . From Lemma 61 we know that A, G ∈ Mod(⊢ g ). Moreover, since A, F ∈ Mod * (⊢), the congruence Ω A F is the identity relation Id A . Now, in the proof of Lemma 62 we showed that Ω A F = Ω A G. Thus we conclude that Ω A G = Id A . Since A, G ∼ = A/Id A , G/Id A and Mod * (⊢ g ) is closed under isomorphisms, we conclude that A, F s = A, G ∈ Mod * (⊢ g ). A similar argument shows that if B, G ∈ Mod * (⊢ g ), then B, G m ∈ Mod * (⊢). This means that the maps (·) s : Mod * (⊢) ←→ Mod * (⊢ g ) : (·) m are well-defined. The fact that they are inverse bijections follows from Lemma 61.
Theorem 64 (2nd completeness theorem). Let ⊢ be a substitution-invariant mdr on L. Then ⊢ = |= Mod * (⊢) = |= ′ Mod * (⊢) . Proof. From the general theory of the algebraisation of Gentzen systems we know that Mod * (⊢ g ) is a class of models of ⊢ g . By Lemma 61 this implies that the image of the class Mod * (⊢ g ) under the transformation (·) m is a class of models of ⊢. But by the previous corollary we know that this image coincides with Mod * (⊢). Thus Mod * (⊢) is a class of models of ⊢. Then suppose that X Y. From the very definition of ⊢ g it follows that for any sequence ϕ 1 , . . . , ϕ n and ψ 1 , . . . , ψ m such that X = [ϕ 1 , . . . , ϕ n ] and Y = [ψ 1 , . . . , ψ m ] we have: From the general completeness result of ⊢ g with respect to Mod * (⊢ g ) it follows that there is A, F ∈ Mod * (⊢ g ) and a homomorphism f : Due to the previous corollary we know that A, G ∈ Mod * (⊢). Moreover, it is straightforward to check that

Monoid matrices and t-norm semantics
It is possible to give hypermatrices a (nearly) equivalent formulation in such a way as to shed further light on the direction in which they generalise ordinary logical matrices. The rough idea is replacing the unstructured set of designated values in a logical matrix by a richer structure. If A, D is an ordinary logical matrix (i.e., an algebra with a subset), D can be identified with a function in {0, 1} A ; in other words, being designated is an all-or-nothing matter. The set {0, 1} can also be viewed as the universe of the 2-element join semilattice 2. If we replace 2 by any dually integral Abelian po-monoid D, however, we can at the same time express an ordering of "degrees of designation", and evaluate the degree of designation of whole submultisets of A, with the monoidal operation in D ensuring that evaluations behave well with respect to multiset union. This leads to the following: Proof. D ′ is a dually integral Abelian po-monoid by assumption, and likewise (g (G)] is a ≤-downset in D ′ . The map g•f is a composition of monoid homomorphisms, and if X Y, then f (X) ≤ D f (Y) and so g (f (X)) ≤ D ′ g (f (Y)).
Of course, each axiomatic system can also be seen as a collection of schemata, i.e. a collection of consecutions and all their substitution instances. Observe that our single-conclusion axiomatic systems are essentially Avron's multiset Hilbert systems [3]; however, the upcoming notion of tree-proof is different, as our single-conclusion mdr's (unlike Avron's "simple consequence relations") enjoy the Monotonicity condition.
Definition 74 (Tree-proof). Let L be a propositional language and let AS be a single-conclusion axiomatic system in L. A tree-proof of a formula ϕ from a multiset of formulas Γ in AS is a finite tree t labelled by formulas such that: • The root of t is labelled by ϕ.
• If a leaf of t is labelled by ψ, then either ψ is an axiom or ψ is an element of Γ and it labels at most Γ(ψ) leaves in t.
• If a node of t is labelled by ψ and ∆ = ∅ is the multiset of labels of its predecessor nodes, then ∆ ⊲ [ψ] ∈ AS.
We write Γ ⊢ t AS ϕ whenever there is a tree-proof of ϕ from Γ in AS. Our next goal is to define a notion of derivation for arbitrary axiomatic systems.
Definition 75. Let L be a propositional language and let AS be an axiomatic system in L. A derivation of a finite multiset of formulas ∆ from a finite multiset of formulas Γ in AS is a finite sequence Γ 1 , . . . , Γ n of finite multisets of formulas such that: We say that ∆ is derivable from Γ in AS, and write Γ ⊢ AS ∆, if there is a derivation of ∆ from Γ in AS.
Observe that, if Ψ = ∅, the second clause above says that in a derivation we are allowed to beef up with finitely many axioms any multiset that has already been derived. The next lemma supports the adequacy of the given definition.
Lemma 76. Let L be a propositional language and let AS be an axiomatic system in L. Then ⊢ AS is the least substitution-invariant mdr containing AS.
Proof. Generalized Reflexivity being trivial, we prove the remaining conditions one by one.
• (Compatibility). Given a derivation P = Γ 1 , . . . , Γ n of ∆ from Γ in AS, it is easy to observe that the sequence P ′ = Γ 1 ⊎ Π, . . . , Γ n ⊎ Π is a derivation of ∆ ⊎ Π from Γ ⊎ Π (thanks to the fact that in our notion of proof we can apply rules in an arbitrary context).
Now for the proof that ⊢ AS is the least substitution-invariant mdr containing AS. Obviously AS ⊆ ⊢ AS . What remains to prove is that for each substitutioninvariant mdr ⊢, if AS ⊆⊢, then ⊢ AS ⊆ ⊢. Assume that Γ ⊢ AS ∆, i.e. there is a derivation P of ∆ from Γ in AS. By induction on the length of P , we can show that for each multiset of formulas Π in P we have Γ ⊢ Π, and hence in particular Γ ⊢ ∆. The base case is settled with an appeal to Reflexivity. As to the induction step: let Π and Π ′ be labels of successive elements of P and Γ ⊢ Π. We know that there is a rule Ψ ⊲ Ψ ′ such that Π ′ = (Π \ Ψ) ⊎ Ψ ′ . Thus Ψ ⊢ Ψ ′ , and so by Compatibility Ψ ⊎ (Π \ Ψ) ⊢ Ψ ′ ⊎ (Π \ Ψ), i.e. Π ⊢ Π ′ . An application of Transitivity completes the proof.
Definition 77. Let L be a propositional language, AS an axiomatic system in L, and let ⊢ be a substitution-invariant mdr on L. We say that AS is an axiomatic system for (or a presentation of ) ⊢ if ⊢ = ⊢ AS .
Clearly, due to the previous lemma, each mdr can be seen as its own presentation, and so we obtain: Corollary 78 ( Los-Suszko). Every substitution-invariant mdr ⊢ coincides with the derivability relation ⊢ AS of some axiomatic system AS.
The next lemma spells out the relationship between derivations and treeproofs.
Lemma 79. Let AS be a single-conclusion axiomatic system on L, Γ ⊢ AS ∆, and ϕ ∈ |∆|. Then there are multisets of L-formulas Γ ϕ and Γ r such that Γ ϕ ⊎ Γ r = Γ, Γ ϕ ⊢ t AS ϕ and Γ r ⊢ AS ∆ \ [ϕ]. Proof. Let P = Γ 1 , . . . , Γ n be the assumed derivation of ∆ from Γ in AS. For each i ≤ n, let Γ i = [ψ i 1 , . . . , ψ i ki ] and note that without loss of generality we can assume that the rule used in the i-th step of P is [ψ i 1 , . . . , ψ i pi ] ⊲ ψ i+1 ci for some p i ≤ k i and c i ≤ k i+1 . Also note that k i+1 − 1 = k i+1 − p i and there is a bijection f between Γ i+1 \ [ψ i+1 ci ] and Γ i \ [ψ i 1 , . . . , ψ i pi ] such that ψ i+1 j = ψ i f (j) whenever c i = j ≤ k i+1 . We construct the labelled graph G with nodes N = { i, j | i ≤ n and j ≤ k i }, where ψ i j is the label of i, j , and edges only between the following nodes: • rule edges: i, k and i + 1, c i for each k ≤ p i ; • non-rule edges: i, f (j) and i + 1, j for j = c i .
It is easy to see that G is a forest (a disjoint union of trees). Let t be the subtree of G with root ψ 1 n , and let Γ ϕ be the multiset of all labels of leaves in t which are not axioms. Then clearly Γ ϕ Γ and t is almost a tree-proof of ϕ from Γ ϕ ; all we have to do is to collapse nodes connected by non-rule edges.
Finally, let Γ t i denote the multiset resulting from Γ i by removing formulas labeling the nodes of t (as many times as it labels some node) and observe that Γ t 1 , . . . , Γ t n is almost a proof of Γ t n = Γ n \ [ψ n 1 ] from Γ t 1 : we only need to remove each Γ t i which equals its predecessor. Defining Γ r = Γ t 1 and observing that Γ r = Γ \ Γ ϕ and ∆ \ [ψ n 1 ] Γ t n completes the proof.
Lemma 80. Let AS be a single-conclusion axiomatic system. Then Proof. One direction follows directly from the previous lemma. To prove the converse one, assume that there is a tree-proof t of ϕ from Γ in AS. Let n be a node of t, ψ n its label, P n the set of its predecessors, ∆ n the multiset of labels of nodes in P n , and Γ n the multiset of labels of elements of Γ which are not axioms and occur in leaves of the subtree of t with root n. If we show that Γ n ⊢ AS [ψ n ], the proof is done: indeed for the root r of t we obtain Γ r ⊢ AS [ϕ] and given that Γ r Γ and ⊢ is an mdr, we obtain the claim by Monotonicity. Let us prove the claim: if n is a leaf, the proof is trivial. Otherwise, there is a rule ∆ n ⊲ [ψ n ] and for each m ∈ P n we have Γ m ⊢ [ψ m ]. Thus m∈Pn Γ m ⊢ ∆ n and so m∈Pn Γ m ⊢ [ψ n ]. The proof is completed by observing that m∈Pn Γ m = Γ n .
Recall that single-conclusion mdr's were introduced in Definition 50 as fragments of mdr's. We now observe that the tree-provability relations of singleconclusion axiomatic systems, in a sense, "generate" the corresponding derivability relations.
Corollary 81. Let AS be a single-conclusion axiomatic system. Then ⊢ t AS is a single-conclusion mdr and ⊢ AS is the least mdr ⊢ such that Proof. The former claim is immediate from the previous lemma. To prove the latter, assume that ⊢ is an mdr such that We need to show that if Γ ⊢ AS ∆, then Γ ⊢ ∆. We prove it by induction on n = ψ∈|∆| ∆ (ψ). If n = 0 the claim is trivial. Assume now that ∆ = ∆ 0 ⊎ [ϕ].
We close this subsection by providing an axiomatic system for ⊢ MV , the multiset companion of infinite-valued Lukasiewicz logic ⊢ L . Although we show that it has no single-conclusion axiomatisation, we also axiomatise its singleconclusion fragment. In this way, we incidentally provide an example of two different mdr's with the same single-conclusion fragment.
Proposition 82. There is no single-conclusion presentation of ⊢ MV .
Proof. Assume that there is such a system Ax and note that we have [p ⊗ q] ⊢ Ax [p, q]. Then, due to Lemma 79, either ⊢ Ax p or ⊢ Ax q, a contradiction. Observe that MV s is a single-conclusion axiomatic system. Proof. Recall, that given a multiset of L 0 -formulas Γ = [γ 1 , . . . , γ n ], we write Γ for γ 1 ⊗ · · · ⊗ γ n . Note that due to the standard completeness of ⊢ L we obtain: For the left-to-right direction of the former claim, it suffices to prove the latter. Assume that Γ = Γ 1 , . . . , Γ n ≥ ∆ is a derivation of ∆ from Γ. If we show that MV |= Γ i ≤ Γ i+1 the claim follows as MV |= Γ n ≤ ∆. We distinguish three cases: • The case when Γ i+1 = Γ i ⊎ [ϕ], where ϕ is an axiom, is simple, as in this case we have MV |= ϕ ≈ 1.
For the converse direction, we first prove the first claim by induction on the length of Γ. Note that thanks to Lemma 79 we can work with tree-proofs. If Γ = ∅, then by the assumption we know that ϕ is a theorem of Lukasiewicz logic, i.e., there is a proof of ϕ in the usual Hilbert calculus of Lukasiewicz logic. This proof can be easily transformed into a tree-proof of ϕ in ⊢ MV s . For the induction step, observe that if Γ ⊎ [ψ] ⊢ MV [ϕ], then Γ ⊢ MV [ψ → ϕ] and so by induction there is a tree-proof of ψ → ϕ from Γ from which it is trivial to get a tree-proof of ϕ from Γ ⊎ [ψ]. Finally, we prove the right-to-left direction of the latter claim. First notice that Γ ⊢ MV ∆ entails Γ ⊢ MV ∆ and so by the first claim Γ ⊢ MV s ∆ and thus also Γ ⊢ MV ∆. Repeated use of the rule (⊗-Elim) completes the proof.