Formative processes with applications to the decision problem in set theory: I. Powerset and singleton operators

This paper introduces formative processes, composed by transitive partitions. Given a family F of sets, a formative process ending in the Venn partition Sigma of F is shown to exist. Sufficient criteria are also singled out for a transitive partition to model (via a function from set variables to unions of sets in the partition) all set-literals modeled by Sigma . On the basis of such criteria a procedure is designed that mimics a given formative process by another where sets have finite rank bounded by C(|Sigma|), with C a specific computable function. As a by-product, one of the core results on decidability in computable set theory is rediscovered, namely the one that regards the satisfiability of unquantified set-theoretic formulae involving Boolean operators, the singleton-former, and the powerset operator. The method described (which is able to exhibit a set-solution when the answer is affirmative) can be extended to solve the satisfiability problem for broader fragments of set theory.