Algebraic Properties of Generalized Multisets

We present generalized multisets in the Zermelo-Fraenkel framework, in Reverse Mathematics, and in the Fraenkel-Mostowski framework. In the Zermelo-Fraenkel framework, we prove that the set of all generalized multisets over a certain finite set is a finitely-generated, lattice-ordered, free abelian group. Similar properties are then discussed in Reverse Mathematics. Finally, we study the generalized multisets in the Fraenkel-Mostowski framework, and present their nominal properties. Several Zermelo-Fraenkel algebraic properties of generalized multisets are translated into the Fraenkel-Mostowski framework by using the finite support axiom of the Fraenkel-Mostowski set theory.

I. Introduction

Multisets are used more and more in computer science for quantitative analysis and models of resources. The concept of multiset was introduced in order to capture the idea of multiplicity of appearance, or resource. Multisets are defined by assuming that for a given set an element occurs a finite number of times. For example the prime factorization of a natural number is a multiset whose elements are primes. The invariants of a finite abelian group also form a multiset. Even processes in an operating system can be seen as a multiset, and the examples can continue.