The Logic of Multisets Continued: The Case of Disjunction

We continue our work [5] on the logic of multisets (or on the multiset semantics of linear logic), by interpreting further the additive disjunction ⊔. To this purpose we employ a more general class of processes, called free, the axiomatization of which requires a new rule (not compatible with the full LL), the cancellation rule. Disjunctive multisets are modeled as finite sets of multisets. The ⊔-Horn fragment of linear logic, with the cut rule slightly restricted, is sound with respect to this semantics. Another rule, which is a slight modification of cancellation, added to HF⊔ makes the system sound and complete.