In this note we report on an on-going research concerning new decidability results in computable set theory both in a multi-level syllogistic setting and in a stratified setting. Both deal with free uninterpreted set-to-set function symbols and unary predicates stating monotone properties of set functions. While the syllogistic case is important from a theoretical point of view, the stratified case is significant for the design and implementation of practical decision procedures which can support tools for automated verification when setreasoning is decisive. 1 Introduction In this paper we show the decidability of the unquantified language MLSmf (multi- level syllogistic with monotone functions) which extends MLS (multi-level syllogistic, cf. [3]) with free uninterpreted function symbols and the following predicates stating monotone properties of functions ffl increasing(f), which holds iff s ` t ! f(s) ` f(t), for any two sets s; t; ffl decreasing(f), which holds iff s ` t ! f(t...