The linear logic of multisets
Athanassios Tzouvaras · Logic Journal of IGPL · 1998
We consider finite multisets over some set of urelements equipped only with additive union [uplus ] and show that the {[otimes], -0}-Horn fragment of Intuitionistic Linear Logic (ILL) has a sound and complete interpretation in them by interpreting [otimes] as [uplus ]. The linear implication is interpreted by ordered pairs of multisets expressing replacement. The operator ! is also defined in an asymptotic way. Soundness, completeness and partial completeness results are proved for the {×, -0, !}-Horn fragment as well. Key words: linear logic, multisets, additive union, replacement.