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.
File in questo prodotto:
Non ci sono file associati a questo prodotto.