2LS is a decidable many-sorted set-theoretic language involving one sort for elements and one sort for sets of elements. In this paper we extend
2LS with constructs for expressing monotonicity, additivity, and multiplicativity properties of set-to-set functions. We call the resulting language
2LSmf. We prove that
2LSmf is decidable by reducing the problem of determining the satisfiability of its sentences to the problem of determining the satisfiability of sentences of
2LS. Furthermore, we prove that the language
2LSmf is stably infinite with respect to the sort of elements. Therefore, by using a many-sorted version of the Nelson–Oppen combination method,
2LSmf can be combined with other languages modeling the sort of elements.
Keywords set theory - decision procedure - Nelson–Oppen procedure