Formative Processes with Applications to the Decision Problem in Set Theory

This paper introduces formative processes, composed by transitive partitions. Given a family F of sets, a formative process ending in the Venn partition Σ 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 Σ. 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(|Σ|), 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.

Authors

• Domenico Cantone
• Pietro Ursino
• Eugenio G. Omodeo

Keywords

No keywords are indexed for this paper.