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.
Titolo: | Formative processes with applications to the decision problem in set theory: II. Powerset and singleton operators, finiteness predicate | |
Autori interni: | ||
Data di pubblicazione: | 2014 | |
Rivista: | ||
Handle: | http://hdl.handle.net/20.500.11769/16602 | |
Appare nelle tipologie: | 1.1 Articolo in rivista |