In an effort to marry set theory and theoretical computer science, in 1970 the Computable Set Theory project was launched to study decidable fragments of set theory. A challenging question for researchers has been finding a way to overcome the impossibility of finding finite models that do not exceed a fixed size and to solve advanced decidability problems when the list of nontrivial set constructors is lengthened. The unquantified multi-level syllogistic with singleton and powerset operators (MLSSP) is a result from this research movement. MLSSPF, the subject of this paper, extends MLSSP with the predicate Finite(x), asserting the finite cardinality of the argument.

The focus of Cantone and Ursino’s paper is solving the satisfiability problem for a fragment of MLSSPF that exhibits powerset and fitness operators and a finiteness predicate. The paper proves that this context has a decidable satisfiability problem. In other words, an interpretation that makes the formula true is presented. A “small-witness model property” is proven, asserting that “any satisfiable MLSSPF formulas have a model admitting a small representation through a suitably annotated formative process.”

This research is contributing to efforts to design and implement a set-theoretically based proof verifier. Being able to carry out the elementary deduction steps is critical to any practical application, including program verification and automated deduction. Still far away from a general solution to the challenge, research contributions like the one in the paper bring us closer by providing solutions to subproblems.