A decision procedure for a sublanguage of set theory involving monotone additive and multiplicative functions, II. The multi-level case

Abstract

MLSS is a decidable sublanguage of set theory involving the predicates membership, set equality, set inclusion, and the operators union, intersection, set difference, and singleton.
In this paper we extend MLSS with constructs for expressing monotonicity, additivity, and multiplicativity properties of set-to-set functions. We prove that the resulting language is decidable by reducing the problem of determining the satisfiability of its sentences to the problem of determining the satisfiability of sentences of MLSS.
In addition, we show an interesting model theoretic property of MLSS, the singleton model property, upon which our decidability proof is based. Intuitively, the singleton model property states that if a formula is satisfiable, then it is satisfiable in a model whose non-empty Venn regions are singleton sets.