Formative processes with applications to the decision problem in set theory: II. Powerset and singleton operators, finiteness predicate

In this paper we solve the satisfiability problem for the quantifier-free fragment of set theory MLSSPF involving in addition to the basic Boolean set operators of union, intersection, and difference, also the powerset and singleton operators, and a finiteness predicate.
The more restricted fragment obtained by dropping the finiteness predicate has been shown to have a solvable satisfiability problem in a previous paper, by establishing for it a small model property.
We exploit the latter decision result for dealing also with the finiteness predicate (and therefore with the infiniteness predicate too) and prove a small witness-model property for MLSSPF, asserting that any model for a satisfiable formula Phi with m distinct variables of the fragment of our interest admits a finite representation bounded by c(m), where c is a suitable computable function. Since such candidate representations are finitely many, their number does not exceed a known bound, and it can be recognized algorithmically whether they indeed represent a(n infinite) model for the input formula, the decidability of the satisfiability problem for MLSSPF follows.